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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) = ( 𝐴 · 𝐶 ) ↔ ( 𝐴 = 0 ∨ 𝐵 = 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
3 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
4 3 3adant2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
5 2 4 subeq0ad ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 𝐶 ) ) = 0 ↔ ( 𝐴 · 𝐵 ) = ( 𝐴 · 𝐶 ) ) )
6 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
7 subcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
8 7 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
9 6 8 mul0ord ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · ( 𝐵 − 𝐶 ) ) = 0 ↔ ( 𝐴 = 0 ∨ ( 𝐵 − 𝐶 ) = 0 ) ) )
10 subdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 𝐶 ) ) )
11 10 eqeq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · ( 𝐵 − 𝐶 ) ) = 0 ↔ ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 𝐶 ) ) = 0 ) )
12 subeq0 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) = 0 ↔ 𝐵 = 𝐶 ) )
13 12 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) = 0 ↔ 𝐵 = 𝐶 ) )
14 13 orbi2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 = 0 ∨ ( 𝐵 − 𝐶 ) = 0 ) ↔ ( 𝐴 = 0 ∨ 𝐵 = 𝐶 ) ) )
15 9 11 14 3bitr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 𝐶 ) ) = 0 ↔ ( 𝐴 = 0 ∨ 𝐵 = 𝐶 ) ) )
16 5 15 bitr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) = ( 𝐴 · 𝐶 ) ↔ ( 𝐴 = 0 ∨ 𝐵 = 𝐶 ) ) )