# 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 𝐻 = ( 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 ( 𝜑𝑧𝐴 )
hgmaprnlem1.t2 ( 𝜑𝑡 ∈ ( 𝑉 ∖ { 0 } ) )
hgmaprnlem1.s2 ( 𝜑𝑠𝑉 )
hgmaprnlem1.sz ( 𝜑 → ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) )
hgmaprnlem1.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
hgmaprnlem1.n 𝑁 = ( LSpan ‘ 𝑈 )
hgmaprnlem1.l 𝐿 = ( LSpan ‘ 𝐶 )
Assertion hgmaprnlem3N ( 𝜑𝑧 ∈ 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 hgmaprnlem1.t2 ( 𝜑𝑡 ∈ ( 𝑉 ∖ { 0 } ) )
19 hgmaprnlem1.s2 ( 𝜑𝑠𝑉 )
20 hgmaprnlem1.sz ( 𝜑 → ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) )
21 hgmaprnlem1.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
22 hgmaprnlem1.n 𝑁 = ( LSpan ‘ 𝑈 )
23 hgmaprnlem1.l 𝐿 = ( LSpan ‘ 𝐶 )
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 ( 𝜑 → ( 𝑁 ‘ { 𝑠 } ) ⊆ ( 𝑁 ‘ { 𝑡 } ) )
25 1 2 16 dvhlmod ( 𝜑𝑈 ∈ LMod )
26 18 eldifad ( 𝜑𝑡𝑉 )
27 3 4 5 6 22 25 19 26 lspsnss2 ( 𝜑 → ( ( 𝑁 ‘ { 𝑠 } ) ⊆ ( 𝑁 ‘ { 𝑡 } ) ↔ ∃ 𝑘𝐵 𝑠 = ( 𝑘 · 𝑡 ) ) )
28 24 27 mpbid ( 𝜑 → ∃ 𝑘𝐵 𝑠 = ( 𝑘 · 𝑡 ) )
29 16 3ad2ant1 ( ( 𝜑𝑘𝐵𝑠 = ( 𝑘 · 𝑡 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
30 17 3ad2ant1 ( ( 𝜑𝑘𝐵𝑠 = ( 𝑘 · 𝑡 ) ) → 𝑧𝐴 )
31 18 3ad2ant1 ( ( 𝜑𝑘𝐵𝑠 = ( 𝑘 · 𝑡 ) ) → 𝑡 ∈ ( 𝑉 ∖ { 0 } ) )
32 19 3ad2ant1 ( ( 𝜑𝑘𝐵𝑠 = ( 𝑘 · 𝑡 ) ) → 𝑠𝑉 )
33 20 3ad2ant1 ( ( 𝜑𝑘𝐵𝑠 = ( 𝑘 · 𝑡 ) ) → ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) )
34 simp2 ( ( 𝜑𝑘𝐵𝑠 = ( 𝑘 · 𝑡 ) ) → 𝑘𝐵 )
35 simp3 ( ( 𝜑𝑘𝐵𝑠 = ( 𝑘 · 𝑡 ) ) → 𝑠 = ( 𝑘 · 𝑡 ) )
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 29 30 31 32 33 34 35 hgmaprnlem1N ( ( 𝜑𝑘𝐵𝑠 = ( 𝑘 · 𝑡 ) ) → 𝑧 ∈ ran 𝐺 )
37 36 rexlimdv3a ( 𝜑 → ( ∃ 𝑘𝐵 𝑠 = ( 𝑘 · 𝑡 ) → 𝑧 ∈ ran 𝐺 ) )
38 28 37 mpd ( 𝜑𝑧 ∈ ran 𝐺 )