Metamath Proof Explorer

Theorem xmulcand

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

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

Proof

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