Metamath Proof Explorer


Theorem xmulasslem

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

Ref Expression
Hypotheses xmulasslem.1 x = D ψ X = Y
xmulasslem.2 x = D ψ E = F
xmulasslem.x φ X *
xmulasslem.y φ Y *
xmulasslem.d φ D *
xmulasslem.ps φ x * 0 < x ψ
xmulasslem.0 φ x = 0 ψ
xmulasslem.e φ E = X
xmulasslem.f φ F = Y
Assertion xmulasslem φ X = Y

Proof

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