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 ⊢ φ → A ∈ ℝ
remulcan2d.2 ⊢ φ → B ∈ ℝ
remulcan2d.3 ⊢ φ → C ∈ ℝ
remulcan2d.4 ⊢ φ → C ≠ 0
Assertion remulcan2d ⊢ φ → A ⁢ C = B ⁢ C ↔ A = B

Proof

Step Hyp Ref Expression
1 remulcan2d.1 ⊢ φ → A ∈ ℝ
2 remulcan2d.2 ⊢ φ → B ∈ ℝ
3 remulcan2d.3 ⊢ φ → C ∈ ℝ
4 remulcan2d.4 ⊢ φ → C ≠ 0
5 ax-rrecex ⊢ C ∈ ℝ ∧ C ≠ 0 → ∃ x ∈ ℝ C ⁢ x = 1
6 3 4 5 syl2anc ⊢ φ → ∃ x ∈ ℝ C ⁢ x = 1
7 oveq1 ⊢ A ⁢ C = B ⁢ C → A ⁢ C ⁢ x = B ⁢ C ⁢ x
8 1 adantr ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → A ∈ ℝ
9 8 recnd ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → A ∈ ℂ
10 3 adantr ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → C ∈ ℝ
11 10 recnd ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → C ∈ ℂ
12 simprl ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → x ∈ ℝ
13 12 recnd ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → x ∈ ℂ
14 9 11 13 mulassd ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → A ⁢ C ⁢ x = A ⁢ C ⁢ x
15 simprr ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → C ⁢ x = 1
16 15 oveq2d ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → A ⁢ C ⁢ x = A ⋅ 1
17 ax-1rid ⊢ A ∈ ℝ → A ⋅ 1 = A
18 8 17 syl ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → A ⋅ 1 = A
19 14 16 18 3eqtrd ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → A ⁢ C ⁢ x = A
20 2 adantr ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → B ∈ ℝ
21 20 recnd ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → B ∈ ℂ
22 21 11 13 mulassd ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → B ⁢ C ⁢ x = B ⁢ C ⁢ x
23 15 oveq2d ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → B ⁢ C ⁢ x = B ⋅ 1
24 ax-1rid ⊢ B ∈ ℝ → B ⋅ 1 = B
25 20 24 syl ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → B ⋅ 1 = B
26 22 23 25 3eqtrd ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → B ⁢ C ⁢ x = B
27 19 26 eqeq12d ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → A ⁢ C ⁢ x = B ⁢ C ⁢ x ↔ A = B
28 7 27 syl5ib ⊢ φ ∧ x ∈ ℝ ∧ C ⁢ x = 1 → A ⁢ C = B ⁢ C → A = B
29 6 28 rexlimddv ⊢ φ → A ⁢ C = B ⁢ C → A = B
30 oveq1 ⊢ A = B → A ⁢ C = B ⁢ C
31 29 30 impbid1 ⊢ φ → A ⁢ C = B ⁢ C ↔ A = B