Theorem lspsnnecom

Description: Swap two vectors with different spans. (Contributed by NM, 20-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspsnnecom.v	|- V = ( Base ` W )
2		lspsnnecom.o	|- .0. = ( 0g ` W )
3		lspsnnecom.n	|- N = ( LSpan ` W )
4		lspsnnecom.w	|- ( ph -> W e. LVec )
5		lspsnnecom.x	|- ( ph -> X e. V )
6		lspsnnecom.y	|- ( ph -> Y e. ( V \ { .0. } ) )
7		lspsnnecom.e	|- ( ph -> -. X e. ( N ` { Y } ) )
8		lveclmod	|- ( W e. LVec -> W e. LMod )
9	4 8	syl	|- ( ph -> W e. LMod )
10	6	eldifad	|- ( ph -> Y e. V )
11	1 3 9 5 10 7	lspsnne2	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
12	11	necomd	|- ( ph -> ( N ` { Y } ) =/= ( N ` { X } ) )
13	1 2 3 4 6 5 12	lspsnne1	|- ( ph -> -. Y e. ( N ` { X } ) )