Theorem lspprss

Description: The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015)

	Ref	Expression
Hypotheses	lspprss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lspprss.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspprss.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lspprss.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lspprss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
	lspprss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion	lspprss	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lspprss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lspprss.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lspprss.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lspprss.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
5		lspprss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
6		lspprss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
7	5 6	prssd	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑈 )
8	1 2	lspssp	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ { 𝑋 , 𝑌 } ⊆ 𝑈 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )
9	3 4 7 8	syl3anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )