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

Metamath Proof Explorer

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