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	mullidd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 · 𝑥 ) = 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	mullidd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 1 · 𝐵 ) = 𝐵 )
22	18 20 21	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝑥 · ( 𝐶 · 𝐵 ) ) = 𝐵 )
23	17 22	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝑥 · ( 𝐶 · 𝐴 ) ) = ( 𝑥 · ( 𝐶 · 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )
24	7 23	imbitrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) → 𝐴 = 𝐵 ) )
25	6 24	rexlimddv	⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) → 𝐴 = 𝐵 ) )
26		oveq2	⊢ ( 𝐴 = 𝐵 → ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) )
27	25 26	impbid1	⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ↔ 𝐴 = 𝐵 ) )