Metamath Proof Explorer


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