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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
mulcand.2 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
mulcand.3 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
mulcand.4 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion mulcand ( 𝜑 → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

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