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