This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xmulasslem

Description: Lemma for xmulass . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses xmulasslem.1 ⊢ ( 𝑥 = 𝐷 → ( 𝜓 ↔ 𝑋 = 𝑌 ) )
xmulasslem.2 ⊢ ( 𝑥 = -𝑒 𝐷 → ( 𝜓 ↔ 𝐸 = 𝐹 ) )
xmulasslem.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
xmulasslem.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
xmulasslem.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
xmulasslem.ps ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 0 < 𝑥 ) ) → 𝜓 )
xmulasslem.0 ⊢ ( 𝜑 → ( 𝑥 = 0 → 𝜓 ) )
xmulasslem.e ⊢ ( 𝜑 → 𝐸 = -𝑒 𝑋 )
xmulasslem.f ⊢ ( 𝜑 → 𝐹 = -𝑒 𝑌 )
Assertion xmulasslem ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 xmulasslem.1 ⊢ ( 𝑥 = 𝐷 → ( 𝜓 ↔ 𝑋 = 𝑌 ) )
2 xmulasslem.2 ⊢ ( 𝑥 = -𝑒 𝐷 → ( 𝜓 ↔ 𝐸 = 𝐹 ) )
3 xmulasslem.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
4 xmulasslem.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
5 xmulasslem.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
6 xmulasslem.ps ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 0 < 𝑥 ) ) → 𝜓 )
7 xmulasslem.0 ⊢ ( 𝜑 → ( 𝑥 = 0 → 𝜓 ) )
8 xmulasslem.e ⊢ ( 𝜑 → 𝐸 = -𝑒 𝑋 )
9 xmulasslem.f ⊢ ( 𝜑 → 𝐹 = -𝑒 𝑌 )
10 0xr ⊢ 0 ∈ ℝ*
11 xrltso ⊢ < Or ℝ*
12 solin ⊢ ( ( < Or ℝ* ∧ ( 𝐷 ∈ ℝ* ∧ 0 ∈ ℝ* ) ) → ( 𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷 ) )
13 11 12 mpan ⊢ ( ( 𝐷 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷 ) )
14 5 10 13 sylancl ⊢ ( 𝜑 → ( 𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷 ) )
15 xlt0neg1 ⊢ ( 𝐷 ∈ ℝ* → ( 𝐷 < 0 ↔ 0 < -𝑒 𝐷 ) )
16 5 15 syl ⊢ ( 𝜑 → ( 𝐷 < 0 ↔ 0 < -𝑒 𝐷 ) )
17 xnegcl ⊢ ( 𝐷 ∈ ℝ* → -𝑒 𝐷 ∈ ℝ* )
18 5 17 syl ⊢ ( 𝜑 → -𝑒 𝐷 ∈ ℝ* )
19 breq2 ⊢ ( 𝑥 = -𝑒 𝐷 → ( 0 < 𝑥 ↔ 0 < -𝑒 𝐷 ) )
20 19 2 imbi12d ⊢ ( 𝑥 = -𝑒 𝐷 → ( ( 0 < 𝑥 → 𝜓 ) ↔ ( 0 < -𝑒 𝐷 → 𝐸 = 𝐹 ) ) )
21 20 imbi2d ⊢ ( 𝑥 = -𝑒 𝐷 → ( ( 𝜑 → ( 0 < 𝑥 → 𝜓 ) ) ↔ ( 𝜑 → ( 0 < -𝑒 𝐷 → 𝐸 = 𝐹 ) ) ) )
22 6 exp32 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ* → ( 0 < 𝑥 → 𝜓 ) ) )
23 22 com12 ⊢ ( 𝑥 ∈ ℝ* → ( 𝜑 → ( 0 < 𝑥 → 𝜓 ) ) )
24 21 23 vtoclga ⊢ ( -𝑒 𝐷 ∈ ℝ* → ( 𝜑 → ( 0 < -𝑒 𝐷 → 𝐸 = 𝐹 ) ) )
25 18 24 mpcom ⊢ ( 𝜑 → ( 0 < -𝑒 𝐷 → 𝐸 = 𝐹 ) )
26 16 25 sylbid ⊢ ( 𝜑 → ( 𝐷 < 0 → 𝐸 = 𝐹 ) )
27 8 9 eqeq12d ⊢ ( 𝜑 → ( 𝐸 = 𝐹 ↔ -𝑒 𝑋 = -𝑒 𝑌 ) )
28 xneg11 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ) → ( -𝑒 𝑋 = -𝑒 𝑌 ↔ 𝑋 = 𝑌 ) )
29 3 4 28 syl2anc ⊢ ( 𝜑 → ( -𝑒 𝑋 = -𝑒 𝑌 ↔ 𝑋 = 𝑌 ) )
30 27 29 bitrd ⊢ ( 𝜑 → ( 𝐸 = 𝐹 ↔ 𝑋 = 𝑌 ) )
31 26 30 sylibd ⊢ ( 𝜑 → ( 𝐷 < 0 → 𝑋 = 𝑌 ) )
32 eqeq1 ⊢ ( 𝑥 = 𝐷 → ( 𝑥 = 0 ↔ 𝐷 = 0 ) )
33 32 1 imbi12d ⊢ ( 𝑥 = 𝐷 → ( ( 𝑥 = 0 → 𝜓 ) ↔ ( 𝐷 = 0 → 𝑋 = 𝑌 ) ) )
34 33 imbi2d ⊢ ( 𝑥 = 𝐷 → ( ( 𝜑 → ( 𝑥 = 0 → 𝜓 ) ) ↔ ( 𝜑 → ( 𝐷 = 0 → 𝑋 = 𝑌 ) ) ) )
35 34 7 vtoclg ⊢ ( 𝐷 ∈ ℝ* → ( 𝜑 → ( 𝐷 = 0 → 𝑋 = 𝑌 ) ) )
36 5 35 mpcom ⊢ ( 𝜑 → ( 𝐷 = 0 → 𝑋 = 𝑌 ) )
37 breq2 ⊢ ( 𝑥 = 𝐷 → ( 0 < 𝑥 ↔ 0 < 𝐷 ) )
38 37 1 imbi12d ⊢ ( 𝑥 = 𝐷 → ( ( 0 < 𝑥 → 𝜓 ) ↔ ( 0 < 𝐷 → 𝑋 = 𝑌 ) ) )
39 38 imbi2d ⊢ ( 𝑥 = 𝐷 → ( ( 𝜑 → ( 0 < 𝑥 → 𝜓 ) ) ↔ ( 𝜑 → ( 0 < 𝐷 → 𝑋 = 𝑌 ) ) ) )
40 39 23 vtoclga ⊢ ( 𝐷 ∈ ℝ* → ( 𝜑 → ( 0 < 𝐷 → 𝑋 = 𝑌 ) ) )
41 5 40 mpcom ⊢ ( 𝜑 → ( 0 < 𝐷 → 𝑋 = 𝑌 ) )
42 31 36 41 3jaod ⊢ ( 𝜑 → ( ( 𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷 ) → 𝑋 = 𝑌 ) )
43 14 42 mpd ⊢ ( 𝜑 → 𝑋 = 𝑌 )