# Metamath Proof Explorer

## Theorem hgmaprnlem3N

Description: Lemma for hgmaprnN . Eliminate k . (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. } ) )`
hgmaprnlem1.s2
`|- ( ph -> s e. V )`
hgmaprnlem1.sz
`|- ( ph -> ( S ` s ) = ( z .xb ( S ` t ) ) )`
hgmaprnlem1.m
`|- M = ( ( mapd ` K ) ` W )`
hgmaprnlem1.n
`|- N = ( LSpan ` U )`
hgmaprnlem1.l
`|- L = ( LSpan ` C )`
Assertion hgmaprnlem3N
`|- ( 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 hgmaprnlem1.s2
` |-  ( ph -> s e. V )`
20 hgmaprnlem1.sz
` |-  ( ph -> ( S ` s ) = ( z .xb ( S ` t ) ) )`
21 hgmaprnlem1.m
` |-  M = ( ( mapd ` K ) ` W )`
22 hgmaprnlem1.n
` |-  N = ( LSpan ` U )`
23 hgmaprnlem1.l
` |-  L = ( LSpan ` C )`
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 hgmaprnlem2N
` |-  ( ph -> ( N ` { s } ) C_ ( N ` { t } ) )`
25 1 2 16 dvhlmod
` |-  ( ph -> U e. LMod )`
` |-  ( ph -> t e. V )`
27 3 4 5 6 22 25 19 26 lspsnss2
` |-  ( ph -> ( ( N ` { s } ) C_ ( N ` { t } ) <-> E. k e. B s = ( k .x. t ) ) )`
28 24 27 mpbid
` |-  ( ph -> E. k e. B s = ( k .x. t ) )`
` |-  ( ( ph /\ k e. B /\ s = ( k .x. t ) ) -> ( K e. HL /\ W e. H ) )`
` |-  ( ( ph /\ k e. B /\ s = ( k .x. t ) ) -> z e. A )`
` |-  ( ( ph /\ k e. B /\ s = ( k .x. t ) ) -> t e. ( V \ { .0. } ) )`
` |-  ( ( ph /\ k e. B /\ s = ( k .x. t ) ) -> s e. V )`
` |-  ( ( ph /\ k e. B /\ s = ( k .x. t ) ) -> ( S ` s ) = ( z .xb ( S ` t ) ) )`
` |-  ( ( ph /\ k e. B /\ s = ( k .x. t ) ) -> k e. B )`
` |-  ( ( ph /\ k e. B /\ s = ( k .x. t ) ) -> s = ( k .x. t ) )`
` |-  ( ( ph /\ k e. B /\ s = ( k .x. t ) ) -> z e. ran G )`
` |-  ( ph -> ( E. k e. B s = ( k .x. t ) -> z e. ran G ) )`
` |-  ( ph -> z e. ran G )`