# 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 } ) )`
` |-  ( 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 } ) )`
` |-  ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> W e. LVec )`
` |-  ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> X e. ( V \ { .0. } ) )`
` |-  ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> Z e. V )`
` |-  ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> Y e. V )`
` |-  ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> ( N ` { X } ) =/= ( N ` { Y } ) )`
` |-  ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> X e. ( N ` { Z , Y } ) )`
` |-  ( ( ph /\ X e. ( N ` { Z , Y } ) ) -> Z e. ( N ` { X , Y } ) )`
` |-  ( ph -> -. X e. ( N ` { Z , Y } ) )`
` |-  ( ph -> ( ( N ` { Z } ) =/= ( N ` { Y } ) /\ -. X e. ( N ` { Z , Y } ) ) )`