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 imbitrid ⊢φ∧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