# 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 𝐻 = ( 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 } ) )
Assertion hgmaprnlem4N ( 𝜑𝑧 ∈ 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 1 8 16 lcdlmod ( 𝜑𝐶 ∈ LMod )
20 18 eldifad ( 𝜑𝑡𝑉 )
21 1 2 3 8 9 14 16 20 hdmapcl ( 𝜑 → ( 𝑆𝑡 ) ∈ 𝐷 )
22 9 10 12 11 lmodvscl ( ( 𝐶 ∈ LMod ∧ 𝑧𝐴 ∧ ( 𝑆𝑡 ) ∈ 𝐷 ) → ( 𝑧 ( 𝑆𝑡 ) ) ∈ 𝐷 )
23 19 17 21 22 syl3anc ( 𝜑 → ( 𝑧 ( 𝑆𝑡 ) ) ∈ 𝐷 )
24 1 8 9 14 16 hdmaprnN ( 𝜑 → ran 𝑆 = 𝐷 )
25 23 24 eleqtrrd ( 𝜑 → ( 𝑧 ( 𝑆𝑡 ) ) ∈ ran 𝑆 )
26 1 2 3 14 16 hdmapfnN ( 𝜑𝑆 Fn 𝑉 )
27 fvelrnb ( 𝑆 Fn 𝑉 → ( ( 𝑧 ( 𝑆𝑡 ) ) ∈ ran 𝑆 ↔ ∃ 𝑠𝑉 ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) ) )
28 26 27 syl ( 𝜑 → ( ( 𝑧 ( 𝑆𝑡 ) ) ∈ ran 𝑆 ↔ ∃ 𝑠𝑉 ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) ) )
29 25 28 mpbid ( 𝜑 → ∃ 𝑠𝑉 ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) )
30 16 3ad2ant1 ( ( 𝜑𝑠𝑉 ∧ ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
31 17 3ad2ant1 ( ( 𝜑𝑠𝑉 ∧ ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) ) → 𝑧𝐴 )
32 18 3ad2ant1 ( ( 𝜑𝑠𝑉 ∧ ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) ) → 𝑡 ∈ ( 𝑉 ∖ { 0 } ) )
33 simp2 ( ( 𝜑𝑠𝑉 ∧ ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) ) → 𝑠𝑉 )
34 simp3 ( ( 𝜑𝑠𝑉 ∧ ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) ) → ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) )
35 eqid ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
36 eqid ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
37 eqid ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
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 ( ( 𝜑𝑠𝑉 ∧ ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) ) → 𝑧 ∈ ran 𝐺 )
39 38 rexlimdv3a ( 𝜑 → ( ∃ 𝑠𝑉 ( 𝑆𝑠 ) = ( 𝑧 ( 𝑆𝑡 ) ) → 𝑧 ∈ ran 𝐺 ) )
40 29 39 mpd ( 𝜑𝑧 ∈ ran 𝐺 )