Metamath Proof Explorer

Theorem hgmapfnN

Description: Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hgmapfn.h 
|- H = ( LHyp ` K )
hgmapfn.u 
|- U = ( ( DVecH ` K ) ` W )
hgmapfn.r 
|- R = ( Scalar ` U )
hgmapfn.b 
|- B = ( Base ` R )
hgmapfn.g 
|- G = ( ( HGMap ` K ) ` W )
hgmapfn.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion hgmapfnN 
|- ( ph -> G Fn B )

Proof

Step Hyp Ref Expression
1 hgmapfn.h 
 |-  H = ( LHyp ` K )
2 hgmapfn.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hgmapfn.r 
 |-  R = ( Scalar ` U )
4 hgmapfn.b 
 |-  B = ( Base ` R )
5 hgmapfn.g 
 |-  G = ( ( HGMap ` K ) ` W )
6 hgmapfn.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 riotaex 
 |-  ( iota_ j e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( k ( .s ` U ) x ) ) = ( j ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) ) e. _V
8 eqid 
 |-  ( k e. B |-> ( iota_ j e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( k ( .s ` U ) x ) ) = ( j ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) ) ) = ( k e. B |-> ( iota_ j e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( k ( .s ` U ) x ) ) = ( j ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) ) )
9 7 8 fnmpti 
 |-  ( k e. B |-> ( iota_ j e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( k ( .s ` U ) x ) ) = ( j ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) ) ) Fn B
10 eqid 
 |-  ( Base ` U ) = ( Base ` U )
11 eqid 
 |-  ( .s ` U ) = ( .s ` U )
12 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
13 eqid 
 |-  ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )
14 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
15 1 2 10 11 3 4 12 13 14 5 6 hgmapfval 
 |-  ( ph -> G = ( k e. B |-> ( iota_ j e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( k ( .s ` U ) x ) ) = ( j ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) ) ) )
16 15 fneq1d 
 |-  ( ph -> ( G Fn B <-> ( k e. B |-> ( iota_ j e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( k ( .s ` U ) x ) ) = ( j ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) ) ) Fn B ) )
17 9 16 mpbiri 
 |-  ( ph -> G Fn B )