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 𝑉 = ( Base ‘ 𝑊 )
lspprat.s 𝑆 = ( LSubSp ‘ 𝑊 )
lspprat.n 𝑁 = ( LSpan ‘ 𝑊 )
lspprat.w ( 𝜑𝑊 ∈ LVec )
lspprat.u ( 𝜑𝑈𝑆 )
lspprat.x ( 𝜑𝑋𝑉 )
lspprat.y ( 𝜑𝑌𝑉 )
lspprat.p ( 𝜑𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
lsppratlem1.o 0 = ( 0g𝑊 )
lsppratlem1.x2 ( 𝜑𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
lsppratlem1.y2 ( 𝜑𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
lsppratlem4.x3 ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
Assertion lsppratlem4 ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) )

Proof

Step Hyp Ref Expression
1 lspprat.v 𝑉 = ( Base ‘ 𝑊 )
2 lspprat.s 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspprat.n 𝑁 = ( LSpan ‘ 𝑊 )
4 lspprat.w ( 𝜑𝑊 ∈ LVec )
5 lspprat.u ( 𝜑𝑈𝑆 )
6 lspprat.x ( 𝜑𝑋𝑉 )
7 lspprat.y ( 𝜑𝑌𝑉 )
8 lspprat.p ( 𝜑𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
9 lsppratlem1.o 0 = ( 0g𝑊 )
10 lsppratlem1.x2 ( 𝜑𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
11 lsppratlem1.y2 ( 𝜑𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
12 lsppratlem4.x3 ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
13 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
14 4 13 syl ( 𝜑𝑊 ∈ LMod )
15 1 2 lssss ( 𝑈𝑆𝑈𝑉 )
16 5 15 syl ( 𝜑𝑈𝑉 )
17 16 ssdifssd ( 𝜑 → ( 𝑈 ∖ { 0 } ) ⊆ 𝑉 )
18 17 10 sseldd ( 𝜑𝑥𝑉 )
19 16 ssdifssd ( 𝜑 → ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ⊆ 𝑉 )
20 19 11 sseldd ( 𝜑𝑦𝑉 )
21 1 2 3 14 18 20 lspprcl ( 𝜑 → ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∈ 𝑆 )
22 df-pr { 𝑥 , 𝑌 } = ( { 𝑥 } ∪ { 𝑌 } )
23 snsspr1 { 𝑥 } ⊆ { 𝑥 , 𝑦 }
24 18 20 prssd ( 𝜑 → { 𝑥 , 𝑦 } ⊆ 𝑉 )
25 1 3 lspssid ( ( 𝑊 ∈ LMod ∧ { 𝑥 , 𝑦 } ⊆ 𝑉 ) → { 𝑥 , 𝑦 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
26 14 24 25 syl2anc ( 𝜑 → { 𝑥 , 𝑦 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
27 23 26 sstrid ( 𝜑 → { 𝑥 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
28 18 snssd ( 𝜑 → { 𝑥 } ⊆ 𝑉 )
29 8 pssssd ( 𝜑𝑈 ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
30 1 2 3 14 18 7 lspprcl ( 𝜑 → ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ∈ 𝑆 )
31 df-pr { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
32 12 snssd ( 𝜑 → { 𝑋 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
33 snsspr2 { 𝑌 } ⊆ { 𝑥 , 𝑌 }
34 18 7 prssd ( 𝜑 → { 𝑥 , 𝑌 } ⊆ 𝑉 )
35 1 3 lspssid ( ( 𝑊 ∈ LMod ∧ { 𝑥 , 𝑌 } ⊆ 𝑉 ) → { 𝑥 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
36 14 34 35 syl2anc ( 𝜑 → { 𝑥 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
37 33 36 sstrid ( 𝜑 → { 𝑌 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
38 32 37 unssd ( 𝜑 → ( { 𝑋 } ∪ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
39 31 38 eqsstrid ( 𝜑 → { 𝑋 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
40 2 3 lspssp ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ∈ 𝑆 ∧ { 𝑋 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
41 14 30 39 40 syl3anc ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
42 29 41 sstrd ( 𝜑𝑈 ⊆ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
43 22 fveq2i ( 𝑁 ‘ { 𝑥 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑌 } ) )
44 42 43 sseqtrdi ( 𝜑𝑈 ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑌 } ) ) )
45 44 ssdifd ( 𝜑 → ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ⊆ ( ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
46 45 11 sseldd ( 𝜑𝑦 ∈ ( ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
47 1 2 3 lspsolv ( ( 𝑊 ∈ LVec ∧ ( { 𝑥 } ⊆ 𝑉𝑌𝑉𝑦 ∈ ( ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑦 } ) ) )
48 4 28 7 46 47 syl13anc ( 𝜑𝑌 ∈ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑦 } ) ) )
49 df-pr { 𝑥 , 𝑦 } = ( { 𝑥 } ∪ { 𝑦 } )
50 49 fveq2i ( 𝑁 ‘ { 𝑥 , 𝑦 } ) = ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑦 } ) )
51 48 50 eleqtrrdi ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
52 51 snssd ( 𝜑 → { 𝑌 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
53 27 52 unssd ( 𝜑 → ( { 𝑥 } ∪ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
54 22 53 eqsstrid ( 𝜑 → { 𝑥 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
55 2 3 lspssp ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∈ 𝑆 ∧ { 𝑥 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) → ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
56 14 21 54 55 syl3anc ( 𝜑 → ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
57 56 12 sseldd ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
58 57 51 jca ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) )