Theorem lspindp1

Description: Alternate way to say 3 vectors are mutually independent (swap 1st and 2nd). (Contributed by NM, 11-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 )
	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	lspindp1	|- ( ph -> ( ( N ` { Z } ) =/= ( N ` { Y } ) /\ -. X e. ( N ` { Z , Y } ) ) )

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	5	eldifad	|- ( ph -> X e. V )
11	1 3 4 7 10 6 9	lspindpi	|- ( ph -> ( ( N ` { Z } ) =/= ( N ` { X } ) /\ ( N ` { Z } ) =/= ( N ` { Y } ) ) )
12	11	simprd	|- ( ph -> ( N ` { Z } ) =/= ( N ` { Y } ) )
13	4	adantr	|- ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> W e. LVec )
14	5	adantr	|- ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> X e. ( V \ { .0. } ) )
15	7	adantr	|- ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> Z e. V )
16	6	adantr	|- ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> Y e. V )
17	8	adantr	|- ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
18		simpr	|- ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> X e. ( N ` { Z , Y } ) )
19	1 2 3 13 14 15 16 17 18	lspexch	|- ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> Z e. ( N ` { X , Y } ) )
20	9 19	mtand	|- ( ph -> -. X e. ( N ` { Z , Y } ) )
21	12 20	jca	|- ( ph -> ( ( N ` { Z } ) =/= ( N ` { Y } ) /\ -. X e. ( N ` { Z , Y } ) ) )