Theorem lspindp2l

Description: Alternate way to say 3 vectors are mutually independent (rotate left). (Contributed by NM, 10-May-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 )
	lspindp1.y	|- ( ph -> X e. ( V \ { .0. } ) )
	lspindp1.z	|- ( ph -> Y e. V )
	lspindp1.x	|- ( ph -> Z e. V )
	lspindp1.q	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
	lspindp1.e	|- ( ph -> -. Z e. ( N ` { X , Y } ) )
Assertion	lspindp2l	|- ( ph -> ( ( N ` { Y } ) =/= ( N ` { Z } ) /\ -. X e. ( N ` { Y , Z } ) ) )

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		lspindp1.y	|- ( ph -> X e. ( V \ { .0. } ) )
6		lspindp1.z	|- ( ph -> Y e. V )
7		lspindp1.x	|- ( ph -> Z e. V )
8		lspindp1.q	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
9		lspindp1.e	|- ( ph -> -. Z e. ( N ` { X , Y } ) )
10	1 2 3 4 5 6 7 8 9	lspindp1	|- ( ph -> ( ( N ` { Z } ) =/= ( N ` { Y } ) /\ -. X e. ( N ` { Z , Y } ) ) )
11	10	simpld	|- ( ph -> ( N ` { Z } ) =/= ( N ` { Y } ) )
12	11	necomd	|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )
13	10	simprd	|- ( ph -> -. X e. ( N ` { Z , Y } ) )
14		prcom	|- { Z , Y } = { Y , Z }
15	14	fveq2i	|- ( N ` { Z , Y } ) = ( N ` { Y , Z } )
16	15	eleq2i	|- ( X e. ( N ` { Z , Y } ) <-> X e. ( N ` { Y , Z } ) )
17	13 16	sylnib	|- ( ph -> -. X e. ( N ` { Y , Z } ) )
18	12 17	jca	|- ( ph -> ( ( N ` { Y } ) =/= ( N ` { Z } ) /\ -. X e. ( N ` { Y , Z } ) ) )