Theorem mulcan2g

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

	Ref	Expression
Assertion	mulcan2g	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐶 = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
2	1	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
3		mulcom	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
4	3	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
5	2 4	eqeq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) )
6		mulcan1g	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ↔ ( 𝐶 = 0 ∨ 𝐴 = 𝐵 ) ) )
7	6	3coml	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ↔ ( 𝐶 = 0 ∨ 𝐴 = 𝐵 ) ) )
8		orcom	⊢ ( ( 𝐶 = 0 ∨ 𝐴 = 𝐵 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐶 = 0 ) )
9	7 8	bitrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐶 = 0 ) ) )
10	5 9	bitrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐶 = 0 ) ) )