Metamath Proof Explorer


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 syl5ib ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) → 𝐴 = 𝐵 ) )
29 6 28 rexlimddv ( 𝜑 → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) → 𝐴 = 𝐵 ) )
30 oveq1 ( 𝐴 = 𝐵 → ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) )
31 29 30 impbid1 ( 𝜑 → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ 𝐴 = 𝐵 ) )