Metamath Proof Explorer


Theorem lsppratlem4

Description: Lemma for lspprat . In the second case of lsppratlem1 , y e. ( N{ X , Y } ) C_ ( N{ x , Y } ) and y e/ ( N{ x } ) implies Y e. ( N{ x , y } ) and thus X e. ( N{ x , Y } ) C_ ( N{ x , y } ) as well. (Contributed by NM, 29-Aug-2014)

Ref Expression
Hypotheses lspprat.v V = Base W
lspprat.s S = LSubSp W
lspprat.n N = LSpan W
lspprat.w φ W LVec
lspprat.u φ U S
lspprat.x φ X V
lspprat.y φ Y V
lspprat.p φ U N X Y
lsppratlem1.o 0 ˙ = 0 W
lsppratlem1.x2 φ x U 0 ˙
lsppratlem1.y2 φ y U N x
lsppratlem4.x3 φ X N x Y
Assertion lsppratlem4 φ X N x y Y N x y

Proof

Step Hyp Ref Expression
1 lspprat.v V = Base W
2 lspprat.s S = LSubSp W
3 lspprat.n N = LSpan W
4 lspprat.w φ W LVec
5 lspprat.u φ U S
6 lspprat.x φ X V
7 lspprat.y φ Y V
8 lspprat.p φ U N X Y
9 lsppratlem1.o 0 ˙ = 0 W
10 lsppratlem1.x2 φ x U 0 ˙
11 lsppratlem1.y2 φ y U N x
12 lsppratlem4.x3 φ X N x Y
13 lveclmod W LVec W LMod
14 4 13 syl φ W LMod
15 1 2 lssss U S U V
16 5 15 syl φ U V
17 16 ssdifssd φ U 0 ˙ V
18 17 10 sseldd φ x V
19 16 ssdifssd φ U N x V
20 19 11 sseldd φ y V
21 1 2 3 14 18 20 lspprcl φ N x y S
22 df-pr x Y = x Y
23 snsspr1 x x y
24 18 20 prssd φ x y V
25 1 3 lspssid W LMod x y V x y N x y
26 14 24 25 syl2anc φ x y N x y
27 23 26 sstrid φ x N x y
28 18 snssd φ x V
29 8 pssssd φ U N X Y
30 1 2 3 14 18 7 lspprcl φ N x Y S
31 df-pr X Y = X Y
32 12 snssd φ X N x Y
33 snsspr2 Y x Y
34 18 7 prssd φ x Y V
35 1 3 lspssid W LMod x Y V x Y N x Y
36 14 34 35 syl2anc φ x Y N x Y
37 33 36 sstrid φ Y N x Y
38 32 37 unssd φ X Y N x Y
39 31 38 eqsstrid φ X Y N x Y
40 2 3 lspssp W LMod N x Y S X Y N x Y N X Y N x Y
41 14 30 39 40 syl3anc φ N X Y N x Y
42 29 41 sstrd φ U N x Y
43 22 fveq2i N x Y = N x Y
44 42 43 sseqtrdi φ U N x Y
45 44 ssdifd φ U N x N x Y N x
46 45 11 sseldd φ y N x Y N x
47 1 2 3 lspsolv W LVec x V Y V y N x Y N x Y N x y
48 4 28 7 46 47 syl13anc φ Y N x y
49 df-pr x y = x y
50 49 fveq2i N x y = N x y
51 48 50 eleqtrrdi φ Y N x y
52 51 snssd φ Y N x y
53 27 52 unssd φ x Y N x y
54 22 53 eqsstrid φ x Y N x y
55 2 3 lspssp W LMod N x y S x Y N x y N x Y N x y
56 14 21 54 55 syl3anc φ N x Y N x y
57 56 12 sseldd φ X N x y
58 57 51 jca φ X N x y Y N x y