Metamath Proof Explorer

Theorem dvh2dim

Description: There is a vector that is outside the span of another. (Contributed by NM, 25-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 )
Assertion dvh2dim 
|- ( ph -> E. z e. V -. z e. ( N ` { X } ) )

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 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
8 1 2 3 7 5 dvh1dim 
 |-  ( ph -> E. z e. V z =/= ( 0g ` U ) )
9 8 adantr 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> E. z e. V z =/= ( 0g ` U ) )
10 simpr 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> X = ( 0g ` U ) )
11 10 sneqd 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> { X } = { ( 0g ` U ) } )
12 11 fveq2d 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( N ` { X } ) = ( N ` { ( 0g ` U ) } ) )
13 1 2 5 dvhlmod 
 |-  ( ph -> U e. LMod )
14 7 4 lspsn0 
 |-  ( U e. LMod -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
15 13 14 syl 
 |-  ( ph -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
16 15 adantr 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
17 12 16 eqtrd 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( N ` { X } ) = { ( 0g ` U ) } )
18 17 eleq2d 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( z e. ( N ` { X } ) <-> z e. { ( 0g ` U ) } ) )
19 velsn 
 |-  ( z e. { ( 0g ` U ) } <-> z = ( 0g ` U ) )
20 18 19 bitrdi 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( z e. ( N ` { X } ) <-> z = ( 0g ` U ) ) )
21 20 necon3bbid 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( -. z e. ( N ` { X } ) <-> z =/= ( 0g ` U ) ) )
22 21 rexbidv 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( E. z e. V -. z e. ( N ` { X } ) <-> E. z e. V z =/= ( 0g ` U ) ) )
23 9 22 mpbird 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X } ) )
24 5 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
25 6 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> X e. V )
26 simpr 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> X =/= ( 0g ` U ) )
27 1 2 3 4 24 25 25 7 26 26 dvhdimlem 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , X } ) )
28 dfsn2 
 |-  { X } = { X , X }
29 28 fveq2i 
 |-  ( N ` { X } ) = ( N ` { X , X } )
30 29 eleq2i 
 |-  ( z e. ( N ` { X } ) <-> z e. ( N ` { X , X } ) )
31 30 notbii 
 |-  ( -. z e. ( N ` { X } ) <-> -. z e. ( N ` { X , X } ) )
32 31 rexbii 
 |-  ( E. z e. V -. z e. ( N ` { X } ) <-> E. z e. V -. z e. ( N ` { X , X } ) )
33 27 32 sylibr 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X } ) )
34 23 33 pm2.61dane 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X } ) )