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	|- V = ( Base ` W )
	lspsneq0.z	|- .0. = ( 0g ` W )
	lspsneq0.n	|- N = ( LSpan ` W )
Assertion	lspsneq0	|- ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		lspsneq0.v	|- V = ( Base ` W )
2		lspsneq0.z	|- .0. = ( 0g ` W )
3		lspsneq0.n	|- N = ( LSpan ` W )
4	1 3	lspsnid	|- ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
5		eleq2	|- ( ( N ` { X } ) = { .0. } -> ( X e. ( N ` { X } ) <-> X e. { .0. } ) )
6	4 5	syl5ibcom	|- ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } -> X e. { .0. } ) )
7		elsni	|- ( X e. { .0. } -> X = .0. )
8	6 7	syl6	|- ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } -> X = .0. ) )
9	2 3	lspsn0	|- ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
10	9	adantr	|- ( ( W e. LMod /\ X e. V ) -> ( N ` { .0. } ) = { .0. } )
11		sneq	|- ( X = .0. -> { X } = { .0. } )
12	11	fveqeq2d	|- ( X = .0. -> ( ( N ` { X } ) = { .0. } <-> ( N ` { .0. } ) = { .0. } ) )
13	10 12	syl5ibrcom	|- ( ( W e. LMod /\ X e. V ) -> ( X = .0. -> ( N ` { X } ) = { .0. } ) )
14	8 13	impbid	|- ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )