Metamath Proof Explorer

Theorem lsppratlem3

Description: Lemma for lspprat . In the first case of lsppratlem1 , since x e/ ( N(/) ) , also Y e. ( N{ x } ) , and since y e. ( N{ X , Y } ) C_ ( N{ X , x } ) and y e/ ( N{ x } ) , we have X e. ( N{ x , y } ) as desired. (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 ⊢ ( 𝜑 → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
lsppratlem3.x3 ⊢ ( 𝜑 → 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lsppratlem3 ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) )

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 lsppratlem3.x3 ⊢ ( 𝜑 → 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) )
13 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
14 4 13 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
15 7 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
16 1 3 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑌 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 )
17 14 15 16 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 )
18 17 12 sseldd ⊢ ( 𝜑 → 𝑥 ∈ 𝑉 )
19 18 snssd ⊢ ( 𝜑 → { 𝑥 } ⊆ 𝑉 )
20 8 pssssd ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
21 6 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
22 19 21 unssd ⊢ ( 𝜑 → ( { 𝑥 } ∪ { 𝑋 } ) ⊆ 𝑉 )
23 1 2 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( { 𝑥 } ∪ { 𝑋 } ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) ∈ 𝑆 )
24 14 22 23 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) ∈ 𝑆 )
25 df-pr ⊢ { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
26 1 3 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ ( { 𝑥 } ∪ { 𝑋 } ) ⊆ 𝑉 ) → ( { 𝑥 } ∪ { 𝑋 } ) ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
27 14 22 26 syl2anc ⊢ ( 𝜑 → ( { 𝑥 } ∪ { 𝑋 } ) ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
28 27 unssbd ⊢ ( 𝜑 → { 𝑋 } ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
29 ssun1 ⊢ { 𝑥 } ⊆ ( { 𝑥 } ∪ { 𝑋 } )
30 29 a1i ⊢ ( 𝜑 → { 𝑥 } ⊆ ( { 𝑥 } ∪ { 𝑋 } ) )
31 1 3 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( { 𝑥 } ∪ { 𝑋 } ) ⊆ 𝑉 ∧ { 𝑥 } ⊆ ( { 𝑥 } ∪ { 𝑋 } ) ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
32 14 22 30 31 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
33 0ss ⊢ ∅ ⊆ 𝑉
34 33 a1i ⊢ ( 𝜑 → ∅ ⊆ 𝑉 )
35 uncom ⊢ ( ∅ ∪ { 𝑌 } ) = ( { 𝑌 } ∪ ∅ )
36 un0 ⊢ ( { 𝑌 } ∪ ∅ ) = { 𝑌 }
37 35 36 eqtri ⊢ ( ∅ ∪ { 𝑌 } ) = { 𝑌 }
38 37 fveq2i ⊢ ( 𝑁 ‘ ( ∅ ∪ { 𝑌 } ) ) = ( 𝑁 ‘ { 𝑌 } )
39 12 38 eleqtrrdi ⊢ ( 𝜑 → 𝑥 ∈ ( 𝑁 ‘ ( ∅ ∪ { 𝑌 } ) ) )
40 10 eldifbd ⊢ ( 𝜑 → ¬ 𝑥 ∈ { 0 } )
41 9 3 lsp0 ⊢ ( 𝑊 ∈ LMod → ( 𝑁 ‘ ∅ ) = { 0 } )
42 14 41 syl ⊢ ( 𝜑 → ( 𝑁 ‘ ∅ ) = { 0 } )
43 40 42 neleqtrrd ⊢ ( 𝜑 → ¬ 𝑥 ∈ ( 𝑁 ‘ ∅ ) )
44 39 43 eldifd ⊢ ( 𝜑 → 𝑥 ∈ ( ( 𝑁 ‘ ( ∅ ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ ∅ ) ) )
45 1 2 3 lspsolv ⊢ ( ( 𝑊 ∈ LVec ∧ ( ∅ ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( ∅ ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ ∅ ) ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( ∅ ∪ { 𝑥 } ) ) )
46 4 34 7 44 45 syl13anc ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ ( ∅ ∪ { 𝑥 } ) ) )
47 uncom ⊢ ( ∅ ∪ { 𝑥 } ) = ( { 𝑥 } ∪ ∅ )
48 un0 ⊢ ( { 𝑥 } ∪ ∅ ) = { 𝑥 }
49 47 48 eqtri ⊢ ( ∅ ∪ { 𝑥 } ) = { 𝑥 }
50 49 fveq2i ⊢ ( 𝑁 ‘ ( ∅ ∪ { 𝑥 } ) ) = ( 𝑁 ‘ { 𝑥 } )
51 46 50 eleqtrdi ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑥 } ) )
52 32 51 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
53 52 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
54 28 53 unssd ⊢ ( 𝜑 → ( { 𝑋 } ∪ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
55 25 54 eqsstrid ⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
56 2 3 lspssp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) ∈ 𝑆 ∧ { 𝑋 , 𝑌 } ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
57 14 24 55 56 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
58 20 57 sstrd ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) )
59 58 ssdifd ⊢ ( 𝜑 → ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ⊆ ( ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
60 59 11 sseldd ⊢ ( 𝜑 → 𝑦 ∈ ( ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
61 1 2 3 lspsolv ⊢ ( ( 𝑊 ∈ LVec ∧ ( { 𝑥 } ⊆ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ ( ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑋 } ) ) ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑦 } ) ) )
62 4 19 6 60 61 syl13anc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑦 } ) ) )
63 df-pr ⊢ { 𝑥 , 𝑦 } = ( { 𝑥 } ∪ { 𝑦 } )
64 63 fveq2i ⊢ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) = ( 𝑁 ‘ ( { 𝑥 } ∪ { 𝑦 } ) )
65 62 64 eleqtrrdi ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
66 1 2 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )
67 5 66 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
68 67 ssdifssd ⊢ ( 𝜑 → ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ⊆ 𝑉 )
69 68 11 sseldd ⊢ ( 𝜑 → 𝑦 ∈ 𝑉 )
70 18 69 prssd ⊢ ( 𝜑 → { 𝑥 , 𝑦 } ⊆ 𝑉 )
71 snsspr1 ⊢ { 𝑥 } ⊆ { 𝑥 , 𝑦 }
72 71 a1i ⊢ ( 𝜑 → { 𝑥 } ⊆ { 𝑥 , 𝑦 } )
73 1 3 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑥 , 𝑦 } ⊆ 𝑉 ∧ { 𝑥 } ⊆ { 𝑥 , 𝑦 } ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
74 14 70 72 73 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
75 74 51 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
76 65 75 jca ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) )