This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulcan1g

Description: A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013)

Ref Expression
Assertion mulcan1g 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) = ( A x. C ) <-> ( A = 0 \/ B = C ) ) )

Proof

Step Hyp Ref Expression
1 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
2 1 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. B ) e. CC )
3 mulcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) e. CC )
4 3 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. C ) e. CC )
5 2 4 subeq0ad 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A x. B ) - ( A x. C ) ) = 0 <-> ( A x. B ) = ( A x. C ) ) )
6 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
7 subcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
8 7 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
9 6 8 mul0ord 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. ( B - C ) ) = 0 <-> ( A = 0 \/ ( B - C ) = 0 ) ) )
10 subdi 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )
11 10 eqeq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. ( B - C ) ) = 0 <-> ( ( A x. B ) - ( A x. C ) ) = 0 ) )
12 subeq0 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( B - C ) = 0 <-> B = C ) )
13 12 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B - C ) = 0 <-> B = C ) )
14 13 orbi2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A = 0 \/ ( B - C ) = 0 ) <-> ( A = 0 \/ B = C ) ) )
15 9 11 14 3bitr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A x. B ) - ( A x. C ) ) = 0 <-> ( A = 0 \/ B = C ) ) )
16 5 15 bitr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) = ( A x. C ) <-> ( A = 0 \/ B = C ) ) )