This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ) )