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

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