Metamath Proof Explorer


Theorem lspprid2

Description: A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015)

Ref Expression
Hypotheses lspprid.v 𝑉 = ( Base ‘ 𝑊 )
lspprid.n 𝑁 = ( LSpan ‘ 𝑊 )
lspprid.w ( 𝜑𝑊 ∈ LMod )
lspprid.x ( 𝜑𝑋𝑉 )
lspprid.y ( 𝜑𝑌𝑉 )
Assertion lspprid2 ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 lspprid.v 𝑉 = ( Base ‘ 𝑊 )
2 lspprid.n 𝑁 = ( LSpan ‘ 𝑊 )
3 lspprid.w ( 𝜑𝑊 ∈ LMod )
4 lspprid.x ( 𝜑𝑋𝑉 )
5 lspprid.y ( 𝜑𝑌𝑉 )
6 1 2 3 5 4 lspprid1 ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
7 prcom { 𝑌 , 𝑋 } = { 𝑋 , 𝑌 }
8 7 fveq2i ( 𝑁 ‘ { 𝑌 , 𝑋 } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } )
9 6 8 eleqtrdi ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )