# Metamath Proof Explorer

## Theorem hgmaprnN

Description: Part of proof of part 16 in Baer p. 50 line 23, Fs=G, except that we use the original vector space scalars for the range. (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hgmaprn.h 𝐻 = ( LHyp ‘ 𝐾 )
hgmaprn.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hgmaprn.r 𝑅 = ( Scalar ‘ 𝑈 )
hgmaprn.b 𝐵 = ( Base ‘ 𝑅 )
hgmaprn.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hgmaprn.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
Assertion hgmaprnN ( 𝜑 → ran 𝐺 = 𝐵 )

### Proof

Step Hyp Ref Expression
1 hgmaprn.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hgmaprn.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hgmaprn.r 𝑅 = ( Scalar ‘ 𝑈 )
4 hgmaprn.b 𝐵 = ( Base ‘ 𝑅 )
5 hgmaprn.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
6 hgmaprn.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
7 1 2 3 4 5 6 hgmapfnN ( 𝜑𝐺 Fn 𝐵 )
8 eqid ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
10 eqid ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
11 6 adantr ( ( 𝜑𝑧𝐵 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 simpr ( ( 𝜑𝑧𝐵 ) → 𝑧𝐵 )
13 1 2 3 4 8 9 10 5 11 12 hgmapdcl ( ( 𝜑𝑧𝐵 ) → ( 𝐺𝑧 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
14 13 ralrimiva ( 𝜑 → ∀ 𝑧𝐵 ( 𝐺𝑧 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
15 fnfvrnss ( ( 𝐺 Fn 𝐵 ∧ ∀ 𝑧𝐵 ( 𝐺𝑧 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ran 𝐺 ⊆ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
16 7 14 15 syl2anc ( 𝜑 → ran 𝐺 ⊆ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
17 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
18 eqid ( ·𝑠𝑈 ) = ( ·𝑠𝑈 )
19 eqid ( 0g𝑈 ) = ( 0g𝑈 )
20 eqid ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
21 eqid ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
22 eqid ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
23 eqid ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
24 6 adantr ( ( 𝜑𝑧 ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
25 simpr ( ( 𝜑𝑧 ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → 𝑧 ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
26 1 2 17 3 4 18 19 8 20 9 10 21 22 23 5 24 25 hgmaprnlem5N ( ( 𝜑𝑧 ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → 𝑧 ∈ ran 𝐺 )
27 16 26 eqelssd ( 𝜑 → ran 𝐺 = ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
28 1 2 3 4 8 9 10 6 lcdsbase ( 𝜑 → ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = 𝐵 )
29 27 28 eqtrd ( 𝜑 → ran 𝐺 = 𝐵 )