Theorem xmulasslem

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

	Ref	Expression
Hypotheses	xmulasslem.1	$$⊢x=D\to \left(\psi \leftrightarrow X=Y\right)$$
	xmulasslem.2	$$⊢x=-D\to \left(\psi \leftrightarrow 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 \leftrightarrow X=Y\right)$$
2		xmulasslem.2	$$⊢x=-D\to \left(\psi \leftrightarrow 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\leftrightarrow 0<-D\right)$$
16	5 15	syl	$$⊢\phi \to \left(D<0\leftrightarrow 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\leftrightarrow 0<-D\right)$$
20	19 2	imbi12d	$$⊢x=-D\to \left(\left(0<x\to \psi \right)\leftrightarrow \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)\leftrightarrow \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\leftrightarrow -X=-Y\right)$$
28		xneg11	$$⊢\left(X\in {ℝ}^{*}\wedge Y\in {ℝ}^{*}\right)\to \left(-X=-Y\leftrightarrow X=Y\right)$$
29	3 4 28	syl2anc	$$⊢\phi \to \left(-X=-Y\leftrightarrow X=Y\right)$$
30	27 29	bitrd	$$⊢\phi \to \left(E=F\leftrightarrow X=Y\right)$$
31	26 30	sylibd	$$⊢\phi \to \left(D<0\to X=Y\right)$$
32		eqeq1	$$⊢x=D\to \left(x=0\leftrightarrow D=0\right)$$
33	32 1	imbi12d	$$⊢x=D\to \left(\left(x=0\to \psi \right)\leftrightarrow \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)\leftrightarrow \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\leftrightarrow 0<D\right)$$
38	37 1	imbi12d	$$⊢x=D\to \left(\left(0<x\to \psi \right)\leftrightarrow \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)\leftrightarrow \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$$