Metamath Proof Explorer


Theorem hgmaprnlem1N

Description: Lemma for hgmaprnN . (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.k2 ( 𝜑𝑘𝐵 )
hgmaprnlem1.sk ( 𝜑𝑠 = ( 𝑘 · 𝑡 ) )
Assertion hgmaprnlem1N ( 𝜑𝑧 ∈ 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.k2 ( 𝜑𝑘𝐵 )
22 hgmaprnlem1.sk ( 𝜑𝑠 = ( 𝑘 · 𝑡 ) )
23 22 fveq2d ( 𝜑 → ( 𝑆𝑠 ) = ( 𝑆 ‘ ( 𝑘 · 𝑡 ) ) )
24 18 eldifad ( 𝜑𝑡𝑉 )
25 1 2 3 6 4 5 8 12 14 15 16 24 21 hgmapvs ( 𝜑 → ( 𝑆 ‘ ( 𝑘 · 𝑡 ) ) = ( ( 𝐺𝑘 ) ( 𝑆𝑡 ) ) )
26 23 20 25 3eqtr3d ( 𝜑 → ( 𝑧 ( 𝑆𝑡 ) ) = ( ( 𝐺𝑘 ) ( 𝑆𝑡 ) ) )
27 1 8 16 lcdlvec ( 𝜑𝐶 ∈ LVec )
28 1 2 4 5 8 10 11 15 16 21 hgmapdcl ( 𝜑 → ( 𝐺𝑘 ) ∈ 𝐴 )
29 1 2 3 8 9 14 16 24 hdmapcl ( 𝜑 → ( 𝑆𝑡 ) ∈ 𝐷 )
30 eldifsni ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) → 𝑡0 )
31 18 30 syl ( 𝜑𝑡0 )
32 1 2 3 7 8 13 14 16 24 hdmapeq0 ( 𝜑 → ( ( 𝑆𝑡 ) = 𝑄𝑡 = 0 ) )
33 32 necon3bid ( 𝜑 → ( ( 𝑆𝑡 ) ≠ 𝑄𝑡0 ) )
34 31 33 mpbird ( 𝜑 → ( 𝑆𝑡 ) ≠ 𝑄 )
35 9 12 10 11 13 27 17 28 29 34 lvecvscan2 ( 𝜑 → ( ( 𝑧 ( 𝑆𝑡 ) ) = ( ( 𝐺𝑘 ) ( 𝑆𝑡 ) ) ↔ 𝑧 = ( 𝐺𝑘 ) ) )
36 26 35 mpbid ( 𝜑𝑧 = ( 𝐺𝑘 ) )
37 1 2 4 5 15 16 hgmapfnN ( 𝜑𝐺 Fn 𝐵 )
38 fnfvelrn ( ( 𝐺 Fn 𝐵𝑘𝐵 ) → ( 𝐺𝑘 ) ∈ ran 𝐺 )
39 37 21 38 syl2anc ( 𝜑 → ( 𝐺𝑘 ) ∈ ran 𝐺 )
40 36 39 eqeltrd ( 𝜑𝑧 ∈ ran 𝐺 )