Metamath Proof Explorer

Theorem hgmapffval

Description: Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015)

Ref Expression
Hypothesis hgmapval.h 
|- H = ( LHyp ` K )
Assertion hgmapffval 
|- ( K e. X -> ( HGMap ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) )

Proof

Step Hyp Ref Expression
1 hgmapval.h 
 |-  H = ( LHyp ` K )
2 elex 
 |-  ( K e. X -> K e. _V )
3 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
4 3 1 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
5 fveq2 
 |-  ( k = K -> ( DVecH ` k ) = ( DVecH ` K ) )
6 5 fveq1d 
 |-  ( k = K -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` w ) )
7 fveq2 
 |-  ( k = K -> ( HDMap ` k ) = ( HDMap ` K ) )
8 7 fveq1d 
 |-  ( k = K -> ( ( HDMap ` k ) ` w ) = ( ( HDMap ` K ) ` w ) )
9 fveq2 
 |-  ( k = K -> ( LCDual ` k ) = ( LCDual ` K ) )
10 9 fveq1d 
 |-  ( k = K -> ( ( LCDual ` k ) ` w ) = ( ( LCDual ` K ) ` w ) )
11 10 fveq2d 
 |-  ( k = K -> ( .s ` ( ( LCDual ` k ) ` w ) ) = ( .s ` ( ( LCDual ` K ) ` w ) ) )
12 11 oveqd 
 |-  ( k = K -> ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) )
13 12 eqeq2d 
 |-  ( k = K -> ( ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) <-> ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) )
14 13 ralbidv 
 |-  ( k = K -> ( A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) <-> A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) )
15 14 riotabidv 
 |-  ( k = K -> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) = ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) )
16 15 mpteq2dv 
 |-  ( k = K -> ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) = ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) )
17 16 eleq2d 
 |-  ( k = K -> ( a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) <-> a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) ) )
18 8 17 sbceqbid 
 |-  ( k = K -> ( [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) <-> [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) ) )
19 18 sbcbidv 
 |-  ( k = K -> ( [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) <-> [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) ) )
20 6 19 sbceqbid 
 |-  ( k = K -> ( [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) <-> [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) ) )
21 20 abbidv 
 |-  ( k = K -> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } = { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } )
22 4 21 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) )
23 df-hgmap 
 |-  HGMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } ) )
24 22 23 1 mptfvmpt 
 |-  ( K e. _V -> ( HGMap ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) )
25 2 24 syl 
 |-  ( K e. X -> ( HGMap ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) )