Metamath Proof Explorer

Theorem mulcand

Description: Cancellation law for multiplication. Theorem I.7 of Apostol p. 18. (Contributed by NM, 26-Jan-1995) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 mulcand.1 
 |-  ( ph -> A e. CC )
2 mulcand.2 
 |-  ( ph -> B e. CC )
3 mulcand.3 
 |-  ( ph -> C e. CC )
4 mulcand.4 
 |-  ( ph -> C =/= 0 )
5 recex 
 |-  ( ( C e. CC /\ C =/= 0 ) -> E. x e. CC ( C x. x ) = 1 )
6 3 4 5 syl2anc 
 |-  ( ph -> E. x e. CC ( C x. x ) = 1 )
7 oveq2 
 |-  ( ( C x. A ) = ( C x. B ) -> ( x x. ( C x. A ) ) = ( x x. ( C x. B ) ) )
8 simprl 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> x e. CC )
9 3 adantr 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> C e. CC )
10 8 9 mulcomd 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( x x. C ) = ( C x. x ) )
11 simprr 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( C x. x ) = 1 )
12 10 11 eqtrd 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( x x. C ) = 1 )
13 12 oveq1d 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( ( x x. C ) x. A ) = ( 1 x. A ) )
14 1 adantr 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> A e. CC )
15 8 9 14 mulassd 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( ( x x. C ) x. A ) = ( x x. ( C x. A ) ) )
16 14 mullidd 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( 1 x. A ) = A )
17 13 15 16 3eqtr3d 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( x x. ( C x. A ) ) = A )
18 12 oveq1d 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( ( x x. C ) x. B ) = ( 1 x. B ) )
19 2 adantr 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> B e. CC )
20 8 9 19 mulassd 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( ( x x. C ) x. B ) = ( x x. ( C x. B ) ) )
21 19 mullidd 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( 1 x. B ) = B )
22 18 20 21 3eqtr3d 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( x x. ( C x. B ) ) = B )
23 17 22 eqeq12d 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( ( x x. ( C x. A ) ) = ( x x. ( C x. B ) ) <-> A = B ) )
24 7 23 imbitrid 
 |-  ( ( ph /\ ( x e. CC /\ ( C x. x ) = 1 ) ) -> ( ( C x. A ) = ( C x. B ) -> A = B ) )
25 6 24 rexlimddv 
 |-  ( ph -> ( ( C x. A ) = ( C x. B ) -> A = B ) )
26 oveq2 
 |-  ( A = B -> ( C x. A ) = ( C x. B ) )
27 25 26 impbid1 
 |-  ( ph -> ( ( C x. A ) = ( C x. B ) <-> A = B ) )