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 xmulid2 ⊢ 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 xmulid2 ⊢ 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 syl5ib ⊢ φ ∧ 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