Metamath Proof Explorer

Theorem remulcand

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

Ref Expression
Hypotheses remulcand.1 
|- ( ph -> A e. RR )
remulcand.2 
|- ( ph -> B e. RR )
remulcand.3 
|- ( ph -> C e. RR )
remulcand.4 
|- ( ph -> C =/= 0 )
Assertion remulcand 
|- ( ph -> ( ( C x. A ) = ( C x. B ) <-> A = B ) )

Proof

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