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 ⊢ H = LHyp ⁡ K
hgmaprn.u ⊢ U = DVecH ⁡ K ⁡ W
hgmaprn.r ⊢ R = Scalar ⁡ U
hgmaprn.b ⊢ B = Base R
hgmaprn.g ⊢ G = HGMap ⁡ K ⁡ W
hgmaprn.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion hgmaprnN ⊢ φ → ran ⁡ G = B

Proof

Step Hyp Ref Expression
1 hgmaprn.h ⊢ H = LHyp ⁡ K
2 hgmaprn.u ⊢ U = DVecH ⁡ K ⁡ W
3 hgmaprn.r ⊢ R = Scalar ⁡ U
4 hgmaprn.b ⊢ B = Base R
5 hgmaprn.g ⊢ G = HGMap ⁡ K ⁡ W
6 hgmaprn.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 1 2 3 4 5 6 hgmapfnN ⊢ φ → G Fn B
8 eqid ⊢ LCDual ⁡ K ⁡ W = LCDual ⁡ K ⁡ W
9 eqid ⊢ Scalar ⁡ LCDual ⁡ K ⁡ W = Scalar ⁡ LCDual ⁡ K ⁡ W
10 eqid ⊢ Base Scalar ⁡ LCDual ⁡ K ⁡ W = Base Scalar ⁡ LCDual ⁡ K ⁡ W
11 6 adantr ⊢ φ ∧ z ∈ B → K ∈ HL ∧ W ∈ H
12 simpr ⊢ φ ∧ z ∈ B → z ∈ B
13 1 2 3 4 8 9 10 5 11 12 hgmapdcl ⊢ φ ∧ z ∈ B → G ⁡ z ∈ Base Scalar ⁡ LCDual ⁡ K ⁡ W
14 13 ralrimiva ⊢ φ → ∀ z ∈ B G ⁡ z ∈ Base Scalar ⁡ LCDual ⁡ K ⁡ W
15 fnfvrnss ⊢ G Fn B ∧ ∀ z ∈ B G ⁡ z ∈ Base Scalar ⁡ LCDual ⁡ K ⁡ W → ran ⁡ G ⊆ Base Scalar ⁡ LCDual ⁡ K ⁡ W
16 7 14 15 syl2anc ⊢ φ → ran ⁡ G ⊆ Base Scalar ⁡ LCDual ⁡ K ⁡ W
17 eqid ⊢ Base U = Base U
18 eqid ⊢ ⋅ U = ⋅ U
19 eqid ⊢ 0 U = 0 U
20 eqid ⊢ Base LCDual ⁡ K ⁡ W = Base LCDual ⁡ K ⁡ W
21 eqid ⊢ ⋅ LCDual ⁡ K ⁡ W = ⋅ LCDual ⁡ K ⁡ W
22 eqid ⊢ 0 LCDual ⁡ K ⁡ W = 0 LCDual ⁡ K ⁡ W
23 eqid ⊢ HDMap ⁡ K ⁡ W = HDMap ⁡ K ⁡ W
24 6 adantr ⊢ φ ∧ z ∈ Base Scalar ⁡ LCDual ⁡ K ⁡ W → K ∈ HL ∧ W ∈ H
25 simpr ⊢ φ ∧ z ∈ Base Scalar ⁡ LCDual ⁡ K ⁡ W → z ∈ Base Scalar ⁡ LCDual ⁡ K ⁡ W
26 1 2 17 3 4 18 19 8 20 9 10 21 22 23 5 24 25 hgmaprnlem5N ⊢ φ ∧ z ∈ Base Scalar ⁡ LCDual ⁡ K ⁡ W → z ∈ ran ⁡ G
27 16 26 eqelssd ⊢ φ → ran ⁡ G = Base Scalar ⁡ LCDual ⁡ K ⁡ W
28 1 2 3 4 8 9 10 6 lcdsbase ⊢ φ → Base Scalar ⁡ LCDual ⁡ K ⁡ W = B
29 27 28 eqtrd ⊢ φ → ran ⁡ G = B