Metamath Proof Explorer


Theorem lspsnel6

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014) (Revised by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses lspsnel5.v 𝑉 = ( Base ‘ 𝑊 )
lspsnel5.s 𝑆 = ( LSubSp ‘ 𝑊 )
lspsnel5.n 𝑁 = ( LSpan ‘ 𝑊 )
lspsnel5.w ( 𝜑𝑊 ∈ LMod )
lspsnel5.a ( 𝜑𝑈𝑆 )
Assertion lspsnel6 ( 𝜑 → ( 𝑋𝑈 ↔ ( 𝑋𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lspsnel5.v 𝑉 = ( Base ‘ 𝑊 )
2 lspsnel5.s 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspsnel5.n 𝑁 = ( LSpan ‘ 𝑊 )
4 lspsnel5.w ( 𝜑𝑊 ∈ LMod )
5 lspsnel5.a ( 𝜑𝑈𝑆 )
6 1 2 lssel ( ( 𝑈𝑆𝑋𝑈 ) → 𝑋𝑉 )
7 5 6 sylan ( ( 𝜑𝑋𝑈 ) → 𝑋𝑉 )
8 4 adantr ( ( 𝜑𝑋𝑈 ) → 𝑊 ∈ LMod )
9 5 adantr ( ( 𝜑𝑋𝑈 ) → 𝑈𝑆 )
10 simpr ( ( 𝜑𝑋𝑈 ) → 𝑋𝑈 )
11 2 3 lspsnss ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆𝑋𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
12 8 9 10 11 syl3anc ( ( 𝜑𝑋𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
13 7 12 jca ( ( 𝜑𝑋𝑈 ) → ( 𝑋𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
14 1 3 lspsnid ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
15 4 14 sylan ( ( 𝜑𝑋𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
16 ssel ( ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) → 𝑋𝑈 ) )
17 15 16 syl5com ( ( 𝜑𝑋𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈𝑋𝑈 ) )
18 17 impr ( ( 𝜑 ∧ ( 𝑋𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) → 𝑋𝑈 )
19 13 18 impbida ( 𝜑 → ( 𝑋𝑈 ↔ ( 𝑋𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )