Metamath Proof Explorer

Theorem xmulcand

Description: Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 xmulcand.1 
 |-  ( ph -> A e. RR* )
2 xmulcand.2 
 |-  ( ph -> B e. RR* )
3 xmulcand.3 
 |-  ( ph -> C e. RR )
4 xmulcand.4 
 |-  ( ph -> C =/= 0 )
5 xrecex 
 |-  ( ( C e. RR /\ C =/= 0 ) -> E. x e. RR ( C *e x ) = 1 )
6 3 4 5 syl2anc 
 |-  ( ph -> E. x e. RR ( C *e x ) = 1 )
7 oveq2 
 |-  ( ( C *e A ) = ( C *e B ) -> ( x *e ( C *e A ) ) = ( x *e ( C *e B ) ) )
8 simprl 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> x e. RR )
9 8 rexrd 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> x e. RR* )
10 3 adantr 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> C e. RR )
11 10 rexrd 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> C e. RR* )
12 xmulcom 
 |-  ( ( x e. RR* /\ C e. RR* ) -> ( x *e C ) = ( C *e x ) )
13 9 11 12 syl2anc 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( x *e C ) = ( C *e x ) )
14 simprr 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( C *e x ) = 1 )
15 13 14 eqtrd 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( x *e C ) = 1 )
16 15 oveq1d 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( ( x *e C ) *e A ) = ( 1 *e A ) )
17 1 adantr 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> A e. RR* )
18 xmulass 
 |-  ( ( x e. RR* /\ C e. RR* /\ A e. RR* ) -> ( ( x *e C ) *e A ) = ( x *e ( C *e A ) ) )
19 9 11 17 18 syl3anc 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( ( x *e C ) *e A ) = ( x *e ( C *e A ) ) )
20 xmulid2 
 |-  ( A e. RR* -> ( 1 *e A ) = A )
21 17 20 syl 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( 1 *e A ) = A )
22 16 19 21 3eqtr3d 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( x *e ( C *e A ) ) = A )
23 15 oveq1d 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( ( x *e C ) *e B ) = ( 1 *e B ) )
24 2 adantr 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> B e. RR* )
25 xmulass 
 |-  ( ( x e. RR* /\ C e. RR* /\ B e. RR* ) -> ( ( x *e C ) *e B ) = ( x *e ( C *e B ) ) )
26 9 11 24 25 syl3anc 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( ( x *e C ) *e B ) = ( x *e ( C *e B ) ) )
27 xmulid2 
 |-  ( B e. RR* -> ( 1 *e B ) = B )
28 24 27 syl 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( 1 *e B ) = B )
29 23 26 28 3eqtr3d 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( x *e ( C *e B ) ) = B )
30 22 29 eqeq12d 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( ( x *e ( C *e A ) ) = ( x *e ( C *e B ) ) <-> A = B ) )
31 7 30 syl5ib 
 |-  ( ( ph /\ ( x e. RR /\ ( C *e x ) = 1 ) ) -> ( ( C *e A ) = ( C *e B ) -> A = B ) )
32 6 31 rexlimddv 
 |-  ( ph -> ( ( C *e A ) = ( C *e B ) -> A = B ) )
33 oveq2 
 |-  ( A = B -> ( C *e A ) = ( C *e B ) )
34 32 33 impbid1 
 |-  ( ph -> ( ( C *e A ) = ( C *e B ) <-> A = B ) )