Theorem lspsnne1

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

	Ref	Expression
Hypotheses	lspsnne1.v	|- V = ( Base ` W )
	lspsnne1.o	|- .0. = ( 0g ` W )
	lspsnne1.n	|- N = ( LSpan ` W )
	lspsnne1.w	|- ( ph -> W e. LVec )
	lspsnne1.x	|- ( ph -> X e. ( V \ { .0. } ) )
	lspsnne1.y	|- ( ph -> Y e. V )
	lspsnne1.e	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion	lspsnne1	|- ( ph -> -. X e. ( N ` { Y } ) )

Proof

Step	Hyp	Ref	Expression
1		lspsnne1.v	|- V = ( Base ` W )
2		lspsnne1.o	|- .0. = ( 0g ` W )
3		lspsnne1.n	|- N = ( LSpan ` W )
4		lspsnne1.w	|- ( ph -> W e. LVec )
5		lspsnne1.x	|- ( ph -> X e. ( V \ { .0. } ) )
6		lspsnne1.y	|- ( ph -> Y e. V )
7		lspsnne1.e	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
8		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
9		lveclmod	|- ( W e. LVec -> W e. LMod )
10	4 9	syl	|- ( ph -> W e. LMod )
11	1 8 3	lspsncl	|- ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
12	10 6 11	syl2anc	|- ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
13	5	eldifad	|- ( ph -> X e. V )
14	1 8 3 10 12 13	ellspsn5b	|- ( ph -> ( X e. ( N ` { Y } ) <-> ( N ` { X } ) C_ ( N ` { Y } ) ) )
15	14	notbid	|- ( ph -> ( -. X e. ( N ` { Y } ) <-> -. ( N ` { X } ) C_ ( N ` { Y } ) ) )
16	1 2 3 4 5 6	lspsncmp	|- ( ph -> ( ( N ` { X } ) C_ ( N ` { Y } ) <-> ( N ` { X } ) = ( N ` { Y } ) ) )
17	16	necon3bbid	|- ( ph -> ( -. ( N ` { X } ) C_ ( N ` { Y } ) <-> ( N ` { X } ) =/= ( N ` { Y } ) ) )
18	15 17	bitrd	|- ( ph -> ( -. X e. ( N ` { Y } ) <-> ( N ` { X } ) =/= ( N ` { Y } ) ) )
19	7 18	mpbird	|- ( ph -> -. X e. ( N ` { Y } ) )