Metamath Proof Explorer

Theorem hgmaprnlem4N

Description: Lemma for hgmaprnN . Eliminate s . (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hgmaprnlem1.h
`|- H = ( LHyp ` K )`
hgmaprnlem1.u
`|- U = ( ( DVecH ` K ) ` W )`
hgmaprnlem1.v
`|- V = ( Base ` U )`
hgmaprnlem1.r
`|- R = ( Scalar ` U )`
hgmaprnlem1.b
`|- B = ( Base ` R )`
hgmaprnlem1.t
`|- .x. = ( .s ` U )`
hgmaprnlem1.o
`|- .0. = ( 0g ` U )`
hgmaprnlem1.c
`|- C = ( ( LCDual ` K ) ` W )`
hgmaprnlem1.d
`|- D = ( Base ` C )`
hgmaprnlem1.p
`|- P = ( Scalar ` C )`
hgmaprnlem1.a
`|- A = ( Base ` P )`
hgmaprnlem1.e
`|- .xb = ( .s ` C )`
hgmaprnlem1.q
`|- Q = ( 0g ` C )`
hgmaprnlem1.s
`|- S = ( ( HDMap ` K ) ` W )`
hgmaprnlem1.g
`|- G = ( ( HGMap ` K ) ` W )`
hgmaprnlem1.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
hgmaprnlem1.z
`|- ( ph -> z e. A )`
hgmaprnlem1.t2
`|- ( ph -> t e. ( V \ { .0. } ) )`
Assertion hgmaprnlem4N
`|- ( ph -> z e. ran G )`

Proof

Step Hyp Ref Expression
1 hgmaprnlem1.h
` |-  H = ( LHyp ` K )`
2 hgmaprnlem1.u
` |-  U = ( ( DVecH ` K ) ` W )`
3 hgmaprnlem1.v
` |-  V = ( Base ` U )`
4 hgmaprnlem1.r
` |-  R = ( Scalar ` U )`
5 hgmaprnlem1.b
` |-  B = ( Base ` R )`
6 hgmaprnlem1.t
` |-  .x. = ( .s ` U )`
7 hgmaprnlem1.o
` |-  .0. = ( 0g ` U )`
8 hgmaprnlem1.c
` |-  C = ( ( LCDual ` K ) ` W )`
9 hgmaprnlem1.d
` |-  D = ( Base ` C )`
10 hgmaprnlem1.p
` |-  P = ( Scalar ` C )`
11 hgmaprnlem1.a
` |-  A = ( Base ` P )`
12 hgmaprnlem1.e
` |-  .xb = ( .s ` C )`
13 hgmaprnlem1.q
` |-  Q = ( 0g ` C )`
14 hgmaprnlem1.s
` |-  S = ( ( HDMap ` K ) ` W )`
15 hgmaprnlem1.g
` |-  G = ( ( HGMap ` K ) ` W )`
16 hgmaprnlem1.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
17 hgmaprnlem1.z
` |-  ( ph -> z e. A )`
18 hgmaprnlem1.t2
` |-  ( ph -> t e. ( V \ { .0. } ) )`
19 1 8 16 lcdlmod
` |-  ( ph -> C e. LMod )`
20 18 eldifad
` |-  ( ph -> t e. V )`
21 1 2 3 8 9 14 16 20 hdmapcl
` |-  ( ph -> ( S ` t ) e. D )`
22 9 10 12 11 lmodvscl
` |-  ( ( C e. LMod /\ z e. A /\ ( S ` t ) e. D ) -> ( z .xb ( S ` t ) ) e. D )`
23 19 17 21 22 syl3anc
` |-  ( ph -> ( z .xb ( S ` t ) ) e. D )`
24 1 8 9 14 16 hdmaprnN
` |-  ( ph -> ran S = D )`
25 23 24 eleqtrrd
` |-  ( ph -> ( z .xb ( S ` t ) ) e. ran S )`
26 1 2 3 14 16 hdmapfnN
` |-  ( ph -> S Fn V )`
27 fvelrnb
` |-  ( S Fn V -> ( ( z .xb ( S ` t ) ) e. ran S <-> E. s e. V ( S ` s ) = ( z .xb ( S ` t ) ) ) )`
28 26 27 syl
` |-  ( ph -> ( ( z .xb ( S ` t ) ) e. ran S <-> E. s e. V ( S ` s ) = ( z .xb ( S ` t ) ) ) )`
29 25 28 mpbid
` |-  ( ph -> E. s e. V ( S ` s ) = ( z .xb ( S ` t ) ) )`
30 16 3ad2ant1
` |-  ( ( ph /\ s e. V /\ ( S ` s ) = ( z .xb ( S ` t ) ) ) -> ( K e. HL /\ W e. H ) )`
31 17 3ad2ant1
` |-  ( ( ph /\ s e. V /\ ( S ` s ) = ( z .xb ( S ` t ) ) ) -> z e. A )`
32 18 3ad2ant1
` |-  ( ( ph /\ s e. V /\ ( S ` s ) = ( z .xb ( S ` t ) ) ) -> t e. ( V \ { .0. } ) )`
33 simp2
` |-  ( ( ph /\ s e. V /\ ( S ` s ) = ( z .xb ( S ` t ) ) ) -> s e. V )`
34 simp3
` |-  ( ( ph /\ s e. V /\ ( S ` s ) = ( z .xb ( S ` t ) ) ) -> ( S ` s ) = ( z .xb ( S ` t ) ) )`
35 eqid
` |-  ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )`
36 eqid
` |-  ( LSpan ` U ) = ( LSpan ` U )`
37 eqid
` |-  ( LSpan ` C ) = ( LSpan ` C )`
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 30 31 32 33 34 35 36 37 hgmaprnlem3N
` |-  ( ( ph /\ s e. V /\ ( S ` s ) = ( z .xb ( S ` t ) ) ) -> z e. ran G )`
39 38 rexlimdv3a
` |-  ( ph -> ( E. s e. V ( S ` s ) = ( z .xb ( S ` t ) ) -> z e. ran G ) )`
40 29 39 mpd
` |-  ( ph -> z e. ran G )`