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 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) )