Metamath Proof Explorer

Theorem xmulcand

Description: Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016)

Ref Expression
Hypotheses xmulcand.1 ⊢φ→A∈ℝ*
xmulcand.2 ⊢φ→B∈ℝ*
xmulcand.3 ⊢φ→C∈ℝ
xmulcand.4 ⊢φ→C≠0
Assertion xmulcand ⊢φ→C⋅𝑒A=C⋅𝑒B↔A=B

Proof

Step Hyp Ref Expression
1 xmulcand.1 ⊢φ→A∈ℝ*
2 xmulcand.2 ⊢φ→B∈ℝ*
3 xmulcand.3 ⊢φ→C∈ℝ
4 xmulcand.4 ⊢φ→C≠0
5 xrecex ⊢C∈ℝ∧C≠0→∃x∈ℝC⋅𝑒x=1
6 3 4 5 syl2anc ⊢φ→∃x∈ℝC⋅𝑒x=1
7 oveq2 ⊢C⋅𝑒A=C⋅𝑒B→x⋅𝑒C⋅𝑒A=x⋅𝑒C⋅𝑒B
8 simprl ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x∈ℝ
9 8 rexrd ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x∈ℝ*
10 3 adantr ⊢φ∧x∈ℝ∧C⋅𝑒x=1→C∈ℝ
11 10 rexrd ⊢φ∧x∈ℝ∧C⋅𝑒x=1→C∈ℝ*
12 xmulcom ⊢x∈ℝ*∧C∈ℝ*→x⋅𝑒C=C⋅𝑒x
13 9 11 12 syl2anc ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x⋅𝑒C=C⋅𝑒x
14 simprr ⊢φ∧x∈ℝ∧C⋅𝑒x=1→C⋅𝑒x=1
15 13 14 eqtrd ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x⋅𝑒C=1
16 15 oveq1d ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x⋅𝑒C⋅𝑒A=1⋅𝑒A
17 1 adantr ⊢φ∧x∈ℝ∧C⋅𝑒x=1→A∈ℝ*
18 xmulass ⊢x∈ℝ*∧C∈ℝ*∧A∈ℝ*→x⋅𝑒C⋅𝑒A=x⋅𝑒C⋅𝑒A
19 9 11 17 18 syl3anc ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x⋅𝑒C⋅𝑒A=x⋅𝑒C⋅𝑒A
20 xmullid ⊢A∈ℝ*→1⋅𝑒A=A
21 17 20 syl ⊢φ∧x∈ℝ∧C⋅𝑒x=1→1⋅𝑒A=A
22 16 19 21 3eqtr3d ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x⋅𝑒C⋅𝑒A=A
23 15 oveq1d ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x⋅𝑒C⋅𝑒B=1⋅𝑒B
24 2 adantr ⊢φ∧x∈ℝ∧C⋅𝑒x=1→B∈ℝ*
25 xmulass ⊢x∈ℝ*∧C∈ℝ*∧B∈ℝ*→x⋅𝑒C⋅𝑒B=x⋅𝑒C⋅𝑒B
26 9 11 24 25 syl3anc ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x⋅𝑒C⋅𝑒B=x⋅𝑒C⋅𝑒B
27 xmullid ⊢B∈ℝ*→1⋅𝑒B=B
28 24 27 syl ⊢φ∧x∈ℝ∧C⋅𝑒x=1→1⋅𝑒B=B
29 23 26 28 3eqtr3d ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x⋅𝑒C⋅𝑒B=B
30 22 29 eqeq12d ⊢φ∧x∈ℝ∧C⋅𝑒x=1→x⋅𝑒C⋅𝑒A=x⋅𝑒C⋅𝑒B↔A=B
31 7 30 imbitrid ⊢φ∧x∈ℝ∧C⋅𝑒x=1→C⋅𝑒A=C⋅𝑒B→A=B
32 6 31 rexlimddv ⊢φ→C⋅𝑒A=C⋅𝑒B→A=B
33 oveq2 ⊢A=B→C⋅𝑒A=C⋅𝑒B
34 32 33 impbid1 ⊢φ→C⋅𝑒A=C⋅𝑒B↔A=B