Metamath Proof Explorer


Theorem lspsneq0

Description: Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspsneq0.v 𝑉 = ( Base ‘ 𝑊 )
lspsneq0.z 0 = ( 0g𝑊 )
lspsneq0.n 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspsneq0 ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )

Proof

Step Hyp Ref Expression
1 lspsneq0.v 𝑉 = ( Base ‘ 𝑊 )
2 lspsneq0.z 0 = ( 0g𝑊 )
3 lspsneq0.n 𝑁 = ( LSpan ‘ 𝑊 )
4 1 3 lspsnid ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
5 eleq2 ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ 𝑋 ∈ { 0 } ) )
6 4 5 syl5ibcom ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } → 𝑋 ∈ { 0 } ) )
7 elsni ( 𝑋 ∈ { 0 } → 𝑋 = 0 )
8 6 7 syl6 ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } → 𝑋 = 0 ) )
9 2 3 lspsn0 ( 𝑊 ∈ LMod → ( 𝑁 ‘ { 0 } ) = { 0 } )
10 9 adantr ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { 0 } ) = { 0 } )
11 sneq ( 𝑋 = 0 → { 𝑋 } = { 0 } )
12 11 fveqeq2d ( 𝑋 = 0 → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ ( 𝑁 ‘ { 0 } ) = { 0 } ) )
13 10 12 syl5ibrcom ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑋 = 0 → ( 𝑁 ‘ { 𝑋 } ) = { 0 } ) )
14 8 13 impbid ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )