Metamath Proof Explorer


Theorem remulcand

Description: Commuted version of remulcan2d without ax-mulcom . (Contributed by SN, 21-Feb-2024)

Ref Expression
Hypotheses remulcand.1 φ A
remulcand.2 φ B
remulcand.3 φ C
remulcand.4 φ C 0
Assertion remulcand φ C A = C B A = B

Proof

Step Hyp Ref Expression
1 remulcand.1 φ A
2 remulcand.2 φ B
3 remulcand.3 φ C
4 remulcand.4 φ C 0
5 ax-rrecex C C 0 x C x = 1
6 3 4 5 syl2anc φ x C x = 1
7 3 adantr φ x C
8 7 adantr φ x C x = 1 C
9 simplr φ x C x = 1 x
10 simpr φ x C x = 1 C x = 1
11 8 9 10 remulinvcom φ x C x = 1 x C = 1
12 11 ex φ x C x = 1 x C = 1
13 oveq2 C A = C B x C A = x C B
14 13 3ad2ant3 φ x x C = 1 C A = C B x C A = x C B
15 simp2 φ x x C = 1 C A = C B x C = 1
16 15 oveq1d φ x x C = 1 C A = C B x C A = 1 A
17 simp1r φ x x C = 1 C A = C B x
18 17 recnd φ x x C = 1 C A = C B x
19 7 3ad2ant1 φ x x C = 1 C A = C B C
20 19 recnd φ x x C = 1 C A = C B C
21 simp1l φ x x C = 1 C A = C B φ
22 21 1 syl φ x x C = 1 C A = C B A
23 22 recnd φ x x C = 1 C A = C B A
24 18 20 23 mulassd φ x x C = 1 C A = C B x C A = x C A
25 remulid2 A 1 A = A
26 22 25 syl φ x x C = 1 C A = C B 1 A = A
27 16 24 26 3eqtr3d φ x x C = 1 C A = C B x C A = A
28 15 oveq1d φ x x C = 1 C A = C B x C B = 1 B
29 21 2 syl φ x x C = 1 C A = C B B
30 29 recnd φ x x C = 1 C A = C B B
31 18 20 30 mulassd φ x x C = 1 C A = C B x C B = x C B
32 remulid2 B 1 B = B
33 29 32 syl φ x x C = 1 C A = C B 1 B = B
34 28 31 33 3eqtr3d φ x x C = 1 C A = C B x C B = B
35 14 27 34 3eqtr3d φ x x C = 1 C A = C B A = B
36 35 3exp φ x x C = 1 C A = C B A = B
37 12 36 syld φ x C x = 1 C A = C B A = B
38 37 impr φ x C x = 1 C A = C B A = B
39 6 38 rexlimddv φ C A = C B A = B
40 oveq2 A = B C A = C B
41 39 40 impbid1 φ C A = C B A = B