Metamath Proof Explorer

Theorem mulcand

Description: Cancellation law for multiplication. Theorem I.7 of Apostol p. 18. (Contributed by NM, 26-Jan-1995) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses mulcand.1 ⊢ φ → A ∈ ℂ
mulcand.2 ⊢ φ → B ∈ ℂ
mulcand.3 ⊢ φ → C ∈ ℂ
mulcand.4 ⊢ φ → C ≠ 0
Assertion mulcand ⊢ φ → C ⁢ A = C ⁢ B ↔ A = B

Proof

Step Hyp Ref Expression
1 mulcand.1 ⊢ φ → A ∈ ℂ
2 mulcand.2 ⊢ φ → B ∈ ℂ
3 mulcand.3 ⊢ φ → C ∈ ℂ
4 mulcand.4 ⊢ φ → C ≠ 0
5 recex ⊢ C ∈ ℂ ∧ C ≠ 0 → ∃ x ∈ ℂ C ⁢ x = 1
6 3 4 5 syl2anc ⊢ φ → ∃ x ∈ ℂ C ⁢ x = 1
7 oveq2 ⊢ C ⁢ A = C ⁢ B → x ⁢ C ⁢ A = x ⁢ C ⁢ B
8 simprl ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ∈ ℂ
9 3 adantr ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → C ∈ ℂ
10 8 9 mulcomd ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ⁢ C = C ⁢ x
11 simprr ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → C ⁢ x = 1
12 10 11 eqtrd ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ⁢ C = 1
13 12 oveq1d ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ⁢ C ⁢ A = 1 ⁢ A
14 1 adantr ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → A ∈ ℂ
15 8 9 14 mulassd ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ⁢ C ⁢ A = x ⁢ C ⁢ A
16 14 mulid2d ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → 1 ⁢ A = A
17 13 15 16 3eqtr3d ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ⁢ C ⁢ A = A
18 12 oveq1d ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ⁢ C ⁢ B = 1 ⁢ B
19 2 adantr ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → B ∈ ℂ
20 8 9 19 mulassd ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ⁢ C ⁢ B = x ⁢ C ⁢ B
21 19 mulid2d ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → 1 ⁢ B = B
22 18 20 21 3eqtr3d ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ⁢ C ⁢ B = B
23 17 22 eqeq12d ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → x ⁢ C ⁢ A = x ⁢ C ⁢ B ↔ A = B
24 7 23 syl5ib ⊢ φ ∧ x ∈ ℂ ∧ C ⁢ x = 1 → C ⁢ A = C ⁢ B → A = B
25 6 24 rexlimddv ⊢ φ → C ⁢ A = C ⁢ B → A = B
26 oveq2 ⊢ A = B → C ⁢ A = C ⁢ B
27 25 26 impbid1 ⊢ φ → C ⁢ A = C ⁢ B ↔ A = B