# Metamath Proof Explorer

## Theorem hgmaprnlem5N

Description: Lemma for hgmaprnN . Eliminate t . (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 )`
Assertion hgmaprnlem5N
`|- ( 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 1 2 3 7 16 dvh1dim
` |-  ( ph -> E. t e. V t =/= .0. )`
19 eldifsn
` |-  ( t e. ( V \ { .0. } ) <-> ( t e. V /\ t =/= .0. ) )`
` |-  ( ( ph /\ t e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) )`
` |-  ( ( ph /\ t e. ( V \ { .0. } ) ) -> z e. A )`
` |-  ( ( ph /\ t e. ( V \ { .0. } ) ) -> t e. ( V \ { .0. } ) )`
` |-  ( ( ph /\ t e. ( V \ { .0. } ) ) -> z e. ran G )`
` |-  ( ( ph /\ ( t e. V /\ t =/= .0. ) ) -> z e. ran G )`
` |-  ( ph -> z e. ran G )`