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