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