Theorem lspsnsubn0

Description: Unequal singleton spans imply nonzero vector subtraction. (Contributed by NM, 19-Mar-2015)

	Ref	Expression
Hypotheses	lspsnsubn0.v	|- V = ( Base ` W )
	lspsnsubn0.o	|- .0. = ( 0g ` W )
	lspsnsubn0.m	|- .- = ( -g ` W )
	lspsnsubn0.w	|- ( ph -> W e. LMod )
	lspsnsubn0.x	|- ( ph -> X e. V )
	lspsnsubn0.y	|- ( ph -> Y e. V )
	lspsnsubn0.e	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion	lspsnsubn0	|- ( ph -> ( X .- Y ) =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		lspsnsubn0.v	|- V = ( Base ` W )
2		lspsnsubn0.o	|- .0. = ( 0g ` W )
3		lspsnsubn0.m	|- .- = ( -g ` W )
4		lspsnsubn0.w	|- ( ph -> W e. LMod )
5		lspsnsubn0.x	|- ( ph -> X e. V )
6		lspsnsubn0.y	|- ( ph -> Y e. V )
7		lspsnsubn0.e	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
8	1 2 3	lmodsubeq0	|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( ( X .- Y ) = .0. <-> X = Y ) )
9	4 5 6 8	syl3anc	|- ( ph -> ( ( X .- Y ) = .0. <-> X = Y ) )
10		sneq	|- ( X = Y -> { X } = { Y } )
11	10	fveq2d	|- ( X = Y -> ( N ` { X } ) = ( N ` { Y } ) )
12	9 11	syl6bi	|- ( ph -> ( ( X .- Y ) = .0. -> ( N ` { X } ) = ( N ` { Y } ) ) )
13	12	necon3d	|- ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) -> ( X .- Y ) =/= .0. ) )
14	7 13	mpd	|- ( ph -> ( X .- Y ) =/= .0. )