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
`|- ( ph -> ( K e. HL /\ W e. H ) )`
Assertion hgmaprnN
`|- ( ph -> 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
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
7 1 2 3 4 5 6 hgmapfnN
` |-  ( ph -> 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 ) ) )`
` |-  ( ( ph /\ z e. B ) -> ( K e. HL /\ W e. H ) )`
12 simpr
` |-  ( ( ph /\ z e. B ) -> z e. B )`
13 1 2 3 4 8 9 10 5 11 12 hgmapdcl
` |-  ( ( ph /\ z e. B ) -> ( G ` z ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )`
14 13 ralrimiva
` |-  ( ph -> A. z e. B ( G ` z ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )`
15 fnfvrnss
` |-  ( ( G Fn B /\ A. z e. B ( G ` z ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) -> ran G C_ ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )`
16 7 14 15 syl2anc
` |-  ( ph -> ran G C_ ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )`
17 eqid
` |-  ( Base ` U ) = ( Base ` U )`
18 eqid
` |-  ( .s ` U ) = ( .s ` U )`
19 eqid
` |-  ( 0g ` U ) = ( 0g ` U )`
20 eqid
` |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )`
21 eqid
` |-  ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )`
22 eqid
` |-  ( 0g ` ( ( LCDual ` K ) ` W ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) )`
23 eqid
` |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )`
` |-  ( ( ph /\ z e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) -> ( K e. HL /\ W e. H ) )`
` |-  ( ( ph /\ z e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) -> z e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )`
` |-  ( ( ph /\ z e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) -> z e. ran G )`
` |-  ( ph -> ran G = ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )`
` |-  ( ph -> ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = B )`
` |-  ( ph -> ran G = B )`