Metamath Proof Explorer


Theorem hdmaprnlem17N

Description: Lemma for hdmaprnN . Include zero. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmaprnlem15.h
|- H = ( LHyp ` K )
hdmaprnlem15.u
|- U = ( ( DVecH ` K ) ` W )
hdmaprnlem15.v
|- V = ( Base ` U )
hdmaprnlem15.n
|- N = ( LSpan ` U )
hdmaprnlem15.c
|- C = ( ( LCDual ` K ) ` W )
hdmaprnlem15.d
|- D = ( Base ` C )
hdmaprnlem15.q
|- .0. = ( 0g ` C )
hdmaprnlem15.l
|- L = ( LSpan ` C )
hdmaprnlem15.m
|- M = ( ( mapd ` K ) ` W )
hdmaprnlem15.s
|- S = ( ( HDMap ` K ) ` W )
hdmaprnlem15.k
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmaprnlem17.se
|- ( ph -> s e. D )
Assertion hdmaprnlem17N
|- ( ph -> s e. ran S )

Proof

Step Hyp Ref Expression
1 hdmaprnlem15.h
 |-  H = ( LHyp ` K )
2 hdmaprnlem15.u
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmaprnlem15.v
 |-  V = ( Base ` U )
4 hdmaprnlem15.n
 |-  N = ( LSpan ` U )
5 hdmaprnlem15.c
 |-  C = ( ( LCDual ` K ) ` W )
6 hdmaprnlem15.d
 |-  D = ( Base ` C )
7 hdmaprnlem15.q
 |-  .0. = ( 0g ` C )
8 hdmaprnlem15.l
 |-  L = ( LSpan ` C )
9 hdmaprnlem15.m
 |-  M = ( ( mapd ` K ) ` W )
10 hdmaprnlem15.s
 |-  S = ( ( HDMap ` K ) ` W )
11 hdmaprnlem15.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 hdmaprnlem17.se
 |-  ( ph -> s e. D )
13 eleq1
 |-  ( s = .0. -> ( s e. ran S <-> .0. e. ran S ) )
14 11 adantr
 |-  ( ( ph /\ s =/= .0. ) -> ( K e. HL /\ W e. H ) )
15 12 anim1i
 |-  ( ( ph /\ s =/= .0. ) -> ( s e. D /\ s =/= .0. ) )
16 eldifsn
 |-  ( s e. ( D \ { .0. } ) <-> ( s e. D /\ s =/= .0. ) )
17 15 16 sylibr
 |-  ( ( ph /\ s =/= .0. ) -> s e. ( D \ { .0. } ) )
18 1 2 3 4 5 6 7 8 9 10 14 17 hdmaprnlem16N
 |-  ( ( ph /\ s =/= .0. ) -> s e. ran S )
19 eqid
 |-  ( 0g ` U ) = ( 0g ` U )
20 1 2 19 5 7 10 11 hdmapval0
 |-  ( ph -> ( S ` ( 0g ` U ) ) = .0. )
21 1 2 3 10 11 hdmapfnN
 |-  ( ph -> S Fn V )
22 1 2 11 dvhlmod
 |-  ( ph -> U e. LMod )
23 3 19 lmod0vcl
 |-  ( U e. LMod -> ( 0g ` U ) e. V )
24 22 23 syl
 |-  ( ph -> ( 0g ` U ) e. V )
25 fnfvelrn
 |-  ( ( S Fn V /\ ( 0g ` U ) e. V ) -> ( S ` ( 0g ` U ) ) e. ran S )
26 21 24 25 syl2anc
 |-  ( ph -> ( S ` ( 0g ` U ) ) e. ran S )
27 20 26 eqeltrrd
 |-  ( ph -> .0. e. ran S )
28 13 18 27 pm2.61ne
 |-  ( ph -> s e. ran S )