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

Metamath Proof Explorer

Theorem lsppratlem3

Proof