This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )