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 } ) )
9 8 adantr 
 |-  ( ( 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 } ) )
23 22 adantr 
 |-  ( ( 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 } ) )
32 5 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> ( K e. HL /\ W e. H ) )
33 6 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X e. V )
34 7 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y e. V )
35 simprl 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X =/= ( 0g ` U ) )
36 simprr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y =/= ( 0g ` U ) )
37 1 2 3 4 32 33 34 14 35 36 dvhdimlem 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> E. z e. V -. z e. ( N ` { X , Y } ) )
38 21 31 37 pm2.61da2ne 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) )