Metamath Proof Explorer


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 ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )