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 ) ) )