# 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 𝐻 = ( LHyp ‘ 𝐾 )
hgmaprnlem1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.v 𝑉 = ( Base ‘ 𝑈 )
hgmaprnlem1.r 𝑅 = ( Scalar ‘ 𝑈 )
hgmaprnlem1.b 𝐵 = ( Base ‘ 𝑅 )
hgmaprnlem1.t · = ( ·𝑠𝑈 )
hgmaprnlem1.o 0 = ( 0g𝑈 )
hgmaprnlem1.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.d 𝐷 = ( Base ‘ 𝐶 )
hgmaprnlem1.p 𝑃 = ( Scalar ‘ 𝐶 )
hgmaprnlem1.a 𝐴 = ( Base ‘ 𝑃 )
hgmaprnlem1.e = ( ·𝑠𝐶 )
hgmaprnlem1.q 𝑄 = ( 0g𝐶 )
hgmaprnlem1.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hgmaprnlem1.z ( 𝜑𝑧𝐴 )
Assertion hgmaprnlem5N ( 𝜑𝑧 ∈ ran 𝐺 )

### Proof

Step Hyp Ref Expression
1 hgmaprnlem1.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hgmaprnlem1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hgmaprnlem1.v 𝑉 = ( Base ‘ 𝑈 )
4 hgmaprnlem1.r 𝑅 = ( Scalar ‘ 𝑈 )
5 hgmaprnlem1.b 𝐵 = ( Base ‘ 𝑅 )
6 hgmaprnlem1.t · = ( ·𝑠𝑈 )
7 hgmaprnlem1.o 0 = ( 0g𝑈 )
8 hgmaprnlem1.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
9 hgmaprnlem1.d 𝐷 = ( Base ‘ 𝐶 )
10 hgmaprnlem1.p 𝑃 = ( Scalar ‘ 𝐶 )
11 hgmaprnlem1.a 𝐴 = ( Base ‘ 𝑃 )
12 hgmaprnlem1.e = ( ·𝑠𝐶 )
13 hgmaprnlem1.q 𝑄 = ( 0g𝐶 )
14 hgmaprnlem1.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
15 hgmaprnlem1.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
16 hgmaprnlem1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
17 hgmaprnlem1.z ( 𝜑𝑧𝐴 )
18 1 2 3 7 16 dvh1dim ( 𝜑 → ∃ 𝑡𝑉 𝑡0 )
19 eldifsn ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑡𝑉𝑡0 ) )
20 16 adantr ( ( 𝜑𝑡 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
21 17 adantr ( ( 𝜑𝑡 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑧𝐴 )
22 simpr ( ( 𝜑𝑡 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑡 ∈ ( 𝑉 ∖ { 0 } ) )
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 20 21 22 hgmaprnlem4N ( ( 𝜑𝑡 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑧 ∈ ran 𝐺 )
24 19 23 sylan2br ( ( 𝜑 ∧ ( 𝑡𝑉𝑡0 ) ) → 𝑧 ∈ ran 𝐺 )
25 18 24 rexlimddv ( 𝜑𝑧 ∈ ran 𝐺 )