lsppratlem2

Description: Lemma for lspprat . Show that if X and Y are both in ( N{ x , y } ) (which will be our goal for each of the two cases above), then ( N{ X , Y } ) C_ U , contradicting the hypothesis for U . (Contributed by NM, 29-Aug-2014) (Revised by Mario Carneiro, 5-Sep-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	⊢ ( 𝜑 → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
	lsppratlem2.x1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
	lsppratlem2.y1	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
Assertion	lsppratlem2	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )

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		lsppratlem2.x1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
13		lsppratlem2.y1	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
14		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
15	4 14	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
16	10	eldifad	⊢ ( 𝜑 → 𝑥 ∈ 𝑈 )
17	11	eldifad	⊢ ( 𝜑 → 𝑦 ∈ 𝑈 )
18	16 17	prssd	⊢ ( 𝜑 → { 𝑥 , 𝑦 } ⊆ 𝑈 )
19	1 2	lssss	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )
20	5 19	syl	⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
21	18 20	sstrd	⊢ ( 𝜑 → { 𝑥 , 𝑦 } ⊆ 𝑉 )
22	1 2 3	lspcl	⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑥 , 𝑦 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∈ 𝑆 )
23	15 21 22	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∈ 𝑆 )
24	2 3 15 23 12 13	lspprss	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
25	2 3 15 5 16 17	lspprss	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ⊆ 𝑈 )
26	24 25	sstrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )

Metamath Proof Explorer

Theorem lsppratlem2

Proof