Theorem lspsnne2

Description: Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015)

	Ref	Expression
Hypotheses	lspsnne2.v	|- V = ( Base ` W )
	lspsnne2.n	|- N = ( LSpan ` W )
	lspsnne2.w	|- ( ph -> W e. LMod )
	lspsnne2.x	|- ( ph -> X e. V )
	lspsnne2.y	|- ( ph -> Y e. V )
	lspsnne2.e	|- ( ph -> -. X e. ( N ` { Y } ) )
Assertion	lspsnne2	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )

Proof

Step	Hyp	Ref	Expression
1		lspsnne2.v	|- V = ( Base ` W )
2		lspsnne2.n	|- N = ( LSpan ` W )
3		lspsnne2.w	|- ( ph -> W e. LMod )
4		lspsnne2.x	|- ( ph -> X e. V )
5		lspsnne2.y	|- ( ph -> Y e. V )
6		lspsnne2.e	|- ( ph -> -. X e. ( N ` { Y } ) )
7		eqimss	|- ( ( N ` { X } ) = ( N ` { Y } ) -> ( N ` { X } ) C_ ( N ` { Y } ) )
8		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
9	1 8 2	lspsncl	|- ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
10	3 5 9	syl2anc	|- ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
11	1 8 2 3 10 4	lspsnel5	|- ( ph -> ( X e. ( N ` { Y } ) <-> ( N ` { X } ) C_ ( N ` { Y } ) ) )
12	7 11	syl5ibr	|- ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> X e. ( N ` { Y } ) ) )
13	12	necon3bd	|- ( ph -> ( -. X e. ( N ` { Y } ) -> ( N ` { X } ) =/= ( N ` { Y } ) ) )
14	6 13	mpd	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )