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