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

Metamath Proof Explorer

Theorem lsppratlem4

Proof