Metamath Proof Explorer

Theorem xmulasslem

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

Ref Expression
Hypotheses xmulasslem.1 ${⊢}{x}={D}\to \left({\psi }↔{X}={Y}\right)$
xmulasslem.2 ${⊢}{x}=-{D}\to \left({\psi }↔{E}={F}\right)$
xmulasslem.x ${⊢}{\phi }\to {X}\in {ℝ}^{*}$
xmulasslem.y ${⊢}{\phi }\to {Y}\in {ℝ}^{*}$
xmulasslem.d ${⊢}{\phi }\to {D}\in {ℝ}^{*}$
xmulasslem.ps ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge 0<{x}\right)\right)\to {\psi }$
xmulasslem.0 ${⊢}{\phi }\to \left({x}=0\to {\psi }\right)$
xmulasslem.e ${⊢}{\phi }\to {E}=-{X}$
xmulasslem.f ${⊢}{\phi }\to {F}=-{Y}$
Assertion xmulasslem ${⊢}{\phi }\to {X}={Y}$

Proof

Step Hyp Ref Expression
1 xmulasslem.1 ${⊢}{x}={D}\to \left({\psi }↔{X}={Y}\right)$
2 xmulasslem.2 ${⊢}{x}=-{D}\to \left({\psi }↔{E}={F}\right)$
3 xmulasslem.x ${⊢}{\phi }\to {X}\in {ℝ}^{*}$
4 xmulasslem.y ${⊢}{\phi }\to {Y}\in {ℝ}^{*}$
5 xmulasslem.d ${⊢}{\phi }\to {D}\in {ℝ}^{*}$
6 xmulasslem.ps ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge 0<{x}\right)\right)\to {\psi }$
7 xmulasslem.0 ${⊢}{\phi }\to \left({x}=0\to {\psi }\right)$
8 xmulasslem.e ${⊢}{\phi }\to {E}=-{X}$
9 xmulasslem.f ${⊢}{\phi }\to {F}=-{Y}$
10 0xr ${⊢}0\in {ℝ}^{*}$
11 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
12 solin ${⊢}\left(<\mathrm{Or}{ℝ}^{*}\wedge \left({D}\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\right)\to \left({D}<0\vee {D}=0\vee 0<{D}\right)$
13 11 12 mpan ${⊢}\left({D}\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to \left({D}<0\vee {D}=0\vee 0<{D}\right)$
14 5 10 13 sylancl ${⊢}{\phi }\to \left({D}<0\vee {D}=0\vee 0<{D}\right)$
15 xlt0neg1 ${⊢}{D}\in {ℝ}^{*}\to \left({D}<0↔0<-{D}\right)$
16 5 15 syl ${⊢}{\phi }\to \left({D}<0↔0<-{D}\right)$
17 xnegcl ${⊢}{D}\in {ℝ}^{*}\to -{D}\in {ℝ}^{*}$
18 5 17 syl ${⊢}{\phi }\to -{D}\in {ℝ}^{*}$
19 breq2 ${⊢}{x}=-{D}\to \left(0<{x}↔0<-{D}\right)$
20 19 2 imbi12d ${⊢}{x}=-{D}\to \left(\left(0<{x}\to {\psi }\right)↔\left(0<-{D}\to {E}={F}\right)\right)$
21 20 imbi2d ${⊢}{x}=-{D}\to \left(\left({\phi }\to \left(0<{x}\to {\psi }\right)\right)↔\left({\phi }\to \left(0<-{D}\to {E}={F}\right)\right)\right)$
22 6 exp32 ${⊢}{\phi }\to \left({x}\in {ℝ}^{*}\to \left(0<{x}\to {\psi }\right)\right)$
23 22 com12 ${⊢}{x}\in {ℝ}^{*}\to \left({\phi }\to \left(0<{x}\to {\psi }\right)\right)$
24 21 23 vtoclga ${⊢}-{D}\in {ℝ}^{*}\to \left({\phi }\to \left(0<-{D}\to {E}={F}\right)\right)$
25 18 24 mpcom ${⊢}{\phi }\to \left(0<-{D}\to {E}={F}\right)$
26 16 25 sylbid ${⊢}{\phi }\to \left({D}<0\to {E}={F}\right)$
27 8 9 eqeq12d ${⊢}{\phi }\to \left({E}={F}↔-{X}=-{Y}\right)$
28 xneg11 ${⊢}\left({X}\in {ℝ}^{*}\wedge {Y}\in {ℝ}^{*}\right)\to \left(-{X}=-{Y}↔{X}={Y}\right)$
29 3 4 28 syl2anc ${⊢}{\phi }\to \left(-{X}=-{Y}↔{X}={Y}\right)$
30 27 29 bitrd ${⊢}{\phi }\to \left({E}={F}↔{X}={Y}\right)$
31 26 30 sylibd ${⊢}{\phi }\to \left({D}<0\to {X}={Y}\right)$
32 eqeq1 ${⊢}{x}={D}\to \left({x}=0↔{D}=0\right)$
33 32 1 imbi12d ${⊢}{x}={D}\to \left(\left({x}=0\to {\psi }\right)↔\left({D}=0\to {X}={Y}\right)\right)$
34 33 imbi2d ${⊢}{x}={D}\to \left(\left({\phi }\to \left({x}=0\to {\psi }\right)\right)↔\left({\phi }\to \left({D}=0\to {X}={Y}\right)\right)\right)$
35 34 7 vtoclg ${⊢}{D}\in {ℝ}^{*}\to \left({\phi }\to \left({D}=0\to {X}={Y}\right)\right)$
36 5 35 mpcom ${⊢}{\phi }\to \left({D}=0\to {X}={Y}\right)$
37 breq2 ${⊢}{x}={D}\to \left(0<{x}↔0<{D}\right)$
38 37 1 imbi12d ${⊢}{x}={D}\to \left(\left(0<{x}\to {\psi }\right)↔\left(0<{D}\to {X}={Y}\right)\right)$
39 38 imbi2d ${⊢}{x}={D}\to \left(\left({\phi }\to \left(0<{x}\to {\psi }\right)\right)↔\left({\phi }\to \left(0<{D}\to {X}={Y}\right)\right)\right)$
40 39 23 vtoclga ${⊢}{D}\in {ℝ}^{*}\to \left({\phi }\to \left(0<{D}\to {X}={Y}\right)\right)$
41 5 40 mpcom ${⊢}{\phi }\to \left(0<{D}\to {X}={Y}\right)$
42 31 36 41 3jaod ${⊢}{\phi }\to \left(\left({D}<0\vee {D}=0\vee 0<{D}\right)\to {X}={Y}\right)$
43 14 42 mpd ${⊢}{\phi }\to {X}={Y}$