Metamath Proof Explorer

Theorem dihlsprn

Description: The span of a vector belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses dihlsprn.h 
|- H = ( LHyp ` K )
dihlsprn.u 
|- U = ( ( DVecH ` K ) ` W )
dihlsprn.v 
|- V = ( Base ` U )
dihlsprn.n 
|- N = ( LSpan ` U )
dihlsprn.i 
|- I = ( ( DIsoH ` K ) ` W )
Assertion dihlsprn 
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran I )

Proof

Step Hyp Ref Expression
1 dihlsprn.h 
 |-  H = ( LHyp ` K )
2 dihlsprn.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dihlsprn.v 
 |-  V = ( Base ` U )
4 dihlsprn.n 
 |-  N = ( LSpan ` U )
5 dihlsprn.i 
 |-  I = ( ( DIsoH ` K ) ` W )
6 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X = ( 0g ` U ) ) -> X = ( 0g ` U ) )
7 6 sneqd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X = ( 0g ` U ) ) -> { X } = { ( 0g ` U ) } )
8 7 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X = ( 0g ` U ) ) -> ( N ` { X } ) = ( N ` { ( 0g ` U ) } ) )
9 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X = ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
10 1 2 9 dvhlmod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X = ( 0g ` U ) ) -> U e. LMod )
11 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
12 11 4 lspsn0 
 |-  ( U e. LMod -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
13 10 12 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X = ( 0g ` U ) ) -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
14 8 13 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X = ( 0g ` U ) ) -> ( N ` { X } ) = { ( 0g ` U ) } )
15 1 5 2 11 dih0rn 
 |-  ( ( K e. HL /\ W e. H ) -> { ( 0g ` U ) } e. ran I )
16 15 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X = ( 0g ` U ) ) -> { ( 0g ` U ) } e. ran I )
17 14 16 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X = ( 0g ` U ) ) -> ( N ` { X } ) e. ran I )
18 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
19 1 2 18 dvhlmod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X =/= ( 0g ` U ) ) -> U e. LMod )
20 simplr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X =/= ( 0g ` U ) ) -> X e. V )
21 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X =/= ( 0g ` U ) ) -> X =/= ( 0g ` U ) )
22 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
23 3 4 11 22 lsatlspsn2 
 |-  ( ( U e. LMod /\ X e. V /\ X =/= ( 0g ` U ) ) -> ( N ` { X } ) e. ( LSAtoms ` U ) )
24 19 20 21 23 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X =/= ( 0g ` U ) ) -> ( N ` { X } ) e. ( LSAtoms ` U ) )
25 1 2 5 22 dih1dimat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X } ) e. ( LSAtoms ` U ) ) -> ( N ` { X } ) e. ran I )
26 18 24 25 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V ) /\ X =/= ( 0g ` U ) ) -> ( N ` { X } ) e. ran I )
27 17 26 pm2.61dane 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran I )