Theorem remulcan2d

Description: mulcan2d for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023)

	Ref	Expression
Hypotheses	remulcan2d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	remulcan2d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	remulcan2d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	remulcan2d.4	⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion	remulcan2d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		remulcan2d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		remulcan2d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		remulcan2d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		remulcan2d.4	⊢ ( 𝜑 → 𝐶 ≠ 0 )
5		ax-rrecex	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 1 )
6	3 4 5	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 1 )
7		oveq1	⊢ ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) → ( ( 𝐴 · 𝐶 ) · 𝑥 ) = ( ( 𝐵 · 𝐶 ) · 𝑥 ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℝ )
9	8	recnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℂ )
10	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐶 ∈ ℝ )
11	10	recnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐶 ∈ ℂ )
12		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℝ )
13	12	recnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℂ )
14	9 11 13	mulassd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 𝐶 ) · 𝑥 ) = ( 𝐴 · ( 𝐶 · 𝑥 ) ) )
15		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐶 · 𝑥 ) = 1 )
16	15	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐴 · ( 𝐶 · 𝑥 ) ) = ( 𝐴 · 1 ) )
17		ax-1rid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
18	8 17	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐴 · 1 ) = 𝐴 )
19	14 16 18	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 𝐶 ) · 𝑥 ) = 𝐴 )
20	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐵 ∈ ℝ )
21	20	recnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐵 ∈ ℂ )
22	21 11 13	mulassd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐵 · 𝐶 ) · 𝑥 ) = ( 𝐵 · ( 𝐶 · 𝑥 ) ) )
23	15	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐵 · ( 𝐶 · 𝑥 ) ) = ( 𝐵 · 1 ) )
24		ax-1rid	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 1 ) = 𝐵 )
25	20 24	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐵 · 1 ) = 𝐵 )
26	22 23 25	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐵 · 𝐶 ) · 𝑥 ) = 𝐵 )
27	19 26	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( ( 𝐴 · 𝐶 ) · 𝑥 ) = ( ( 𝐵 · 𝐶 ) · 𝑥 ) ↔ 𝐴 = 𝐵 ) )
28	7 27	imbitrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) → 𝐴 = 𝐵 ) )
29	6 28	rexlimddv	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) → 𝐴 = 𝐵 ) )
30		oveq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) )
31	29 30	impbid1	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ 𝐴 = 𝐵 ) )