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 ∨ 𝐵 = 𝐶 ) ) )