Metamath Proof Explorer

Theorem dvafset

Description: The constructed partial vector space A for a lattice K . (Contributed by NM, 8-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypothesis dvaset.h 
|- H = ( LHyp ` K )
Assertion dvafset 
|- ( K e. V -> ( DVecA ` K ) = ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( LTrn ` K ) ` w ) |-> ( s ` f ) ) >. } ) ) )

Proof

Step Hyp Ref Expression
1 dvaset.h 
 |-  H = ( LHyp ` K )
2 elex 
 |-  ( K e. V -> K e. _V )
3 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
4 3 1 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
5 fveq2 
 |-  ( k = K -> ( LTrn ` k ) = ( LTrn ` K ) )
6 5 fveq1d 
 |-  ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
7 6 opeq2d 
 |-  ( k = K -> <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. = <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. )
8 eqidd 
 |-  ( k = K -> ( f o. g ) = ( f o. g ) )
9 6 6 8 mpoeq123dv 
 |-  ( k = K -> ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) = ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) )
10 9 opeq2d 
 |-  ( k = K -> <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. = <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. )
11 fveq2 
 |-  ( k = K -> ( EDRing ` k ) = ( EDRing ` K ) )
12 11 fveq1d 
 |-  ( k = K -> ( ( EDRing ` k ) ` w ) = ( ( EDRing ` K ) ` w ) )
13 12 opeq2d 
 |-  ( k = K -> <. ( Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. = <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. )
14 7 10 13 tpeq123d 
 |-  ( k = K -> { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } = { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } )
15 fveq2 
 |-  ( k = K -> ( TEndo ` k ) = ( TEndo ` K ) )
16 15 fveq1d 
 |-  ( k = K -> ( ( TEndo ` k ) ` w ) = ( ( TEndo ` K ) ` w ) )
17 eqidd 
 |-  ( k = K -> ( s ` f ) = ( s ` f ) )
18 16 6 17 mpoeq123dv 
 |-  ( k = K -> ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) = ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( LTrn ` K ) ` w ) |-> ( s ` f ) ) )
19 18 opeq2d 
 |-  ( k = K -> <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. = <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( LTrn ` K ) ` w ) |-> ( s ` f ) ) >. )
20 19 sneqd 
 |-  ( k = K -> { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. } = { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( LTrn ` K ) ` w ) |-> ( s ` f ) ) >. } )
21 14 20 uneq12d 
 |-  ( k = K -> ( { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. } ) = ( { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( LTrn ` K ) ` w ) |-> ( s ` f ) ) >. } ) )
22 4 21 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. } ) ) = ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( LTrn ` K ) ` w ) |-> ( s ` f ) ) >. } ) ) )
23 df-dveca 
 |-  DVecA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` k ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , f e. ( ( LTrn ` k ) ` w ) |-> ( s ` f ) ) >. } ) ) )
24 22 23 1 mptfvmpt 
 |-  ( K e. _V -> ( DVecA ` K ) = ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( LTrn ` K ) ` w ) |-> ( s ` f ) ) >. } ) ) )
25 2 24 syl 
 |-  ( K e. V -> ( DVecA ` K ) = ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( LTrn ` K ) ` w ) |-> ( s ` f ) ) >. } ) ) )