Metamath Proof Explorer


Theorem hdmap1ffval

Description: Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015)

Ref Expression
Hypothesis hdmap1val.h
|- H = ( LHyp ` K )
Assertion hdmap1ffval
|- ( K e. X -> ( HDMap1 ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )

Proof

Step Hyp Ref Expression
1 hdmap1val.h
 |-  H = ( LHyp ` K )
2 elex
 |-  ( K e. X -> K e. _V )
3 fveq2
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
4 3 1 syl6eqr
 |-  ( 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 -> ( LCDual ` k ) = ( LCDual ` K ) )
8 7 fveq1d
 |-  ( k = K -> ( ( LCDual ` k ) ` w ) = ( ( LCDual ` K ) ` w ) )
9 fveq2
 |-  ( k = K -> ( mapd ` k ) = ( mapd ` K ) )
10 9 fveq1d
 |-  ( k = K -> ( ( mapd ` k ) ` w ) = ( ( mapd ` K ) ` w ) )
11 10 sbceq1d
 |-  ( k = K -> ( [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
12 11 sbcbidv
 |-  ( k = K -> ( [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
13 12 sbcbidv
 |-  ( k = K -> ( [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
14 8 13 sbceqbid
 |-  ( k = K -> ( [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( ( LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
15 14 sbcbidv
 |-  ( k = K -> ( [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
16 15 sbcbidv
 |-  ( k = K -> ( [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
17 6 16 sbceqbid
 |-  ( k = K -> ( [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
18 17 abbidv
 |-  ( k = K -> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } = { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } )
19 4 18 mpteq12dv
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )
20 df-hdmap1
 |-  HDMap1 = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` k ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` k ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )
21 19 20 1 mptfvmpt
 |-  ( K e. _V -> ( HDMap1 ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )
22 2 21 syl
 |-  ( K e. X -> ( HDMap1 ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( ( LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( ( mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )