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 ) ) )
11 6 adantr 
 |-  ( ( 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 )
24 6 adantr 
 |-  ( ( ph /\ z e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) -> ( K e. HL /\ W e. H ) )
25 simpr 
 |-  ( ( ph /\ z e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) -> z e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
26 1 2 17 3 4 18 19 8 20 9 10 21 22 23 5 24 25 hgmaprnlem5N 
 |-  ( ( ph /\ z e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) -> z e. ran G )
27 16 26 eqelssd 
 |-  ( ph -> ran G = ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
28 1 2 3 4 8 9 10 6 lcdsbase 
 |-  ( ph -> ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = B )
29 27 28 eqtrd 
 |-  ( ph -> ran G = B )