Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lspsnel5a.s | ⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) | |
lspsnel5a.n | ⊢ 𝑁 = ( LSpan ‘ 𝑊 ) | ||
lspsnel5a.w | ⊢ ( 𝜑 → 𝑊 ∈ LMod ) | ||
lspsnel5a.a | ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 ) | ||
lspsnel5a.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 ) | ||
Assertion | lspsnel5a | ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspsnel5a.s | ⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) | |
2 | lspsnel5a.n | ⊢ 𝑁 = ( LSpan ‘ 𝑊 ) | |
3 | lspsnel5a.w | ⊢ ( 𝜑 → 𝑊 ∈ LMod ) | |
4 | lspsnel5a.a | ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 ) | |
5 | lspsnel5a.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 ) | |
6 | eqid | ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) | |
7 | 6 1 | lssel | ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) ) |
8 | 4 5 7 | syl2anc | ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) ) |
9 | 6 1 2 3 4 8 | lspsnel5 | ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) |
10 | 5 9 | mpbid | ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) |