Metamath Proof Explorer


Theorem lspindp2

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

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