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