Metamath Proof Explorer

Theorem remulcand

Description: Commuted version of remulcan2d without ax-mulcom . (Contributed by SN, 21-Feb-2024)

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

Proof

Step Hyp Ref Expression
1 remulcand.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 remulcand.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 remulcand.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 remulcand.4 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
5 ax-rrecex ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 1 )
6 3 4 5 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 1 )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐶 ∈ ℝ )
8 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐶 · 𝑥 ) = 1 ) → 𝐶 ∈ ℝ )
9 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐶 · 𝑥 ) = 1 ) → 𝑥 ∈ ℝ )
10 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐶 · 𝑥 ) = 1 ) → ( 𝐶 · 𝑥 ) = 1 )
11 8 9 10 remulinvcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐶 · 𝑥 ) = 1 ) → ( 𝑥 · 𝐶 ) = 1 )
12 11 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐶 · 𝑥 ) = 1 → ( 𝑥 · 𝐶 ) = 1 ) )
13 oveq2 ⊢ ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) → ( 𝑥 · ( 𝐶 · 𝐴 ) ) = ( 𝑥 · ( 𝐶 · 𝐵 ) ) )
14 13 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( 𝑥 · ( 𝐶 · 𝐴 ) ) = ( 𝑥 · ( 𝐶 · 𝐵 ) ) )
15 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( 𝑥 · 𝐶 ) = 1 )
16 15 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( ( 𝑥 · 𝐶 ) · 𝐴 ) = ( 1 · 𝐴 ) )
17 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝑥 ∈ ℝ )
18 17 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝑥 ∈ ℂ )
19 7 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝐶 ∈ ℝ )
20 19 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝐶 ∈ ℂ )
21 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝜑 )
22 21 1 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝐴 ∈ ℝ )
23 22 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝐴 ∈ ℂ )
24 18 20 23 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( ( 𝑥 · 𝐶 ) · 𝐴 ) = ( 𝑥 · ( 𝐶 · 𝐴 ) ) )
25 remulid2 ⊢ ( 𝐴 ∈ ℝ → ( 1 · 𝐴 ) = 𝐴 )
26 22 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( 1 · 𝐴 ) = 𝐴 )
27 16 24 26 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( 𝑥 · ( 𝐶 · 𝐴 ) ) = 𝐴 )
28 15 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( ( 𝑥 · 𝐶 ) · 𝐵 ) = ( 1 · 𝐵 ) )
29 21 2 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝐵 ∈ ℝ )
30 29 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝐵 ∈ ℂ )
31 18 20 30 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( ( 𝑥 · 𝐶 ) · 𝐵 ) = ( 𝑥 · ( 𝐶 · 𝐵 ) ) )
32 remulid2 ⊢ ( 𝐵 ∈ ℝ → ( 1 · 𝐵 ) = 𝐵 )
33 29 32 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( 1 · 𝐵 ) = 𝐵 )
34 28 31 33 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → ( 𝑥 · ( 𝐶 · 𝐵 ) ) = 𝐵 )
35 14 27 34 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 · 𝐶 ) = 1 ∧ ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ) → 𝐴 = 𝐵 )
36 35 3exp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 · 𝐶 ) = 1 → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) → 𝐴 = 𝐵 ) ) )
37 12 36 syld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐶 · 𝑥 ) = 1 → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) → 𝐴 = 𝐵 ) ) )
38 37 impr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) → 𝐴 = 𝐵 ) )
39 6 38 rexlimddv ⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) → 𝐴 = 𝐵 ) )
40 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) )
41 39 40 impbid1 ⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ↔ 𝐴 = 𝐵 ) )