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	⊢ ( 𝜑 → 𝑋 = 𝑌 )