# Metamath Proof Explorer

## Theorem dvh3dim

Description: There is a vector that is outside the span of 2 others. (Contributed by NM, 24-Apr-2015)

Ref Expression
Hypotheses dvh3dim.h
`|- H = ( LHyp ` K )`
dvh3dim.u
`|- U = ( ( DVecH ` K ) ` W )`
dvh3dim.v
`|- V = ( Base ` U )`
dvh3dim.n
`|- N = ( LSpan ` U )`
dvh3dim.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
dvh3dim.x
`|- ( ph -> X e. V )`
dvh3dim.y
`|- ( ph -> Y e. V )`
Assertion dvh3dim
`|- ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) )`

### Proof

Step Hyp Ref Expression
1 dvh3dim.h
` |-  H = ( LHyp ` K )`
2 dvh3dim.u
` |-  U = ( ( DVecH ` K ) ` W )`
3 dvh3dim.v
` |-  V = ( Base ` U )`
4 dvh3dim.n
` |-  N = ( LSpan ` U )`
5 dvh3dim.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
6 dvh3dim.x
` |-  ( ph -> X e. V )`
7 dvh3dim.y
` |-  ( ph -> Y e. V )`
8 1 2 3 4 5 7 dvh2dim
` |-  ( ph -> E. z e. V -. z e. ( N ` { Y } ) )`
` |-  ( ( ph /\ X = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { Y } ) )`
10 prcom
` |-  { X , Y } = { Y , X }`
11 preq2
` |-  ( X = ( 0g ` U ) -> { Y , X } = { Y , ( 0g ` U ) } )`
12 10 11 syl5eq
` |-  ( X = ( 0g ` U ) -> { X , Y } = { Y , ( 0g ` U ) } )`
13 12 fveq2d
` |-  ( X = ( 0g ` U ) -> ( N ` { X , Y } ) = ( N ` { Y , ( 0g ` U ) } ) )`
14 eqid
` |-  ( 0g ` U ) = ( 0g ` U )`
15 1 2 5 dvhlmod
` |-  ( ph -> U e. LMod )`
16 3 14 4 15 7 lsppr0
` |-  ( ph -> ( N ` { Y , ( 0g ` U ) } ) = ( N ` { Y } ) )`
17 13 16 sylan9eqr
` |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( N ` { X , Y } ) = ( N ` { Y } ) )`
18 17 eleq2d
` |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( z e. ( N ` { X , Y } ) <-> z e. ( N ` { Y } ) ) )`
19 18 notbid
` |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( -. z e. ( N ` { X , Y } ) <-> -. z e. ( N ` { Y } ) ) )`
20 19 rexbidv
` |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( E. z e. V -. z e. ( N ` { X , Y } ) <-> E. z e. V -. z e. ( N ` { Y } ) ) )`
21 9 20 mpbird
` |-  ( ( ph /\ X = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , Y } ) )`
22 1 2 3 4 5 6 dvh2dim
` |-  ( ph -> E. z e. V -. z e. ( N ` { X } ) )`
` |-  ( ( ph /\ Y = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X } ) )`
24 preq2
` |-  ( Y = ( 0g ` U ) -> { X , Y } = { X , ( 0g ` U ) } )`
25 24 fveq2d
` |-  ( Y = ( 0g ` U ) -> ( N ` { X , Y } ) = ( N ` { X , ( 0g ` U ) } ) )`
26 3 14 4 15 6 lsppr0
` |-  ( ph -> ( N ` { X , ( 0g ` U ) } ) = ( N ` { X } ) )`
27 25 26 sylan9eqr
` |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( N ` { X , Y } ) = ( N ` { X } ) )`
28 27 eleq2d
` |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( z e. ( N ` { X , Y } ) <-> z e. ( N ` { X } ) ) )`
29 28 notbid
` |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( -. z e. ( N ` { X , Y } ) <-> -. z e. ( N ` { X } ) ) )`
30 29 rexbidv
` |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( E. z e. V -. z e. ( N ` { X , Y } ) <-> E. z e. V -. z e. ( N ` { X } ) ) )`
31 23 30 mpbird
` |-  ( ( ph /\ Y = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , Y } ) )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> ( K e. HL /\ W e. H ) )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X e. V )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y e. V )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X =/= ( 0g ` U ) )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y =/= ( 0g ` U ) )`
` |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> E. z e. V -. z e. ( N ` { X , Y } ) )`
` |-  ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) )`