Theorem lspindp2

Description: Alternate way to say 3 vectors are mutually independent (rotate right). (Contributed by NM, 12-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspindp1.v	|- V = ( Base ` W )
2		lspindp1.o	|- .0. = ( 0g ` W )
3		lspindp1.n	|- N = ( LSpan ` W )
4		lspindp1.w	|- ( ph -> W e. LVec )
5		lspindp2.x	|- ( ph -> X e. V )
6		lspindp2.y	|- ( ph -> Y e. ( V \ { .0. } ) )
7		lspindp2.z	|- ( ph -> Z e. V )
8		lspindp2.q	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
9		lspindp2.e	|- ( ph -> -. Z e. ( N ` { X , Y } ) )
10	8	necomd	|- ( ph -> ( N ` { Y } ) =/= ( N ` { X } ) )
11		prcom	|- { X , Y } = { Y , X }
12	11	fveq2i	|- ( N ` { X , Y } ) = ( N ` { Y , X } )
13	12	eleq2i	|- ( Z e. ( N ` { X , Y } ) <-> Z e. ( N ` { Y , X } ) )
14	9 13	sylnib	|- ( ph -> -. Z e. ( N ` { Y , X } ) )
15	1 2 3 4 6 5 7 10 14	lspindp1	|- ( ph -> ( ( N ` { Z } ) =/= ( N ` { X } ) /\ -. Y e. ( N ` { Z , X } ) ) )