Metamath Proof Explorer

Theorem dvhset

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

Ref Expression
Hypotheses dvhset.h 
|- H = ( LHyp ` K )
dvhset.t 
|- T = ( ( LTrn ` K ) ` W )
dvhset.e 
|- E = ( ( TEndo ` K ) ` W )
dvhset.d 
|- D = ( ( EDRing ` K ) ` W )
dvhset.u 
|- U = ( ( DVecH ` K ) ` W )
Assertion dvhset 
|- ( ( K e. X /\ W e. H ) -> U = ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , D >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) )

Proof

Step Hyp Ref Expression
1 dvhset.h 
 |-  H = ( LHyp ` K )
2 dvhset.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dvhset.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 dvhset.d 
 |-  D = ( ( EDRing ` K ) ` W )
5 dvhset.u 
 |-  U = ( ( DVecH ` K ) ` W )
6 1 dvhfset 
 |-  ( K e. X -> ( DVecH ` K ) = ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) )
7 6 fveq1d 
 |-  ( K e. X -> ( ( DVecH ` K ) ` W ) = ( ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) ` W ) )
8 5 7 syl5eq 
 |-  ( K e. X -> U = ( ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) ` W ) )
9 fveq2 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = ( ( LTrn ` K ) ` W ) )
10 9 2 eqtr4di 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = T )
11 fveq2 
 |-  ( w = W -> ( ( TEndo ` K ) ` w ) = ( ( TEndo ` K ) ` W ) )
12 11 3 eqtr4di 
 |-  ( w = W -> ( ( TEndo ` K ) ` w ) = E )
13 10 12 xpeq12d 
 |-  ( w = W -> ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) = ( T X. E ) )
14 13 opeq2d 
 |-  ( w = W -> <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. = <. ( Base ` ndx ) , ( T X. E ) >. )
15 10 mpteq1d 
 |-  ( w = W -> ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) = ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) )
16 15 opeq2d 
 |-  ( w = W -> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. = <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. )
17 13 13 16 mpoeq123dv 
 |-  ( w = W -> ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) )
18 17 opeq2d 
 |-  ( w = W -> <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. = <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. )
19 fveq2 
 |-  ( w = W -> ( ( EDRing ` K ) ` w ) = ( ( EDRing ` K ) ` W ) )
20 19 4 eqtr4di 
 |-  ( w = W -> ( ( EDRing ` K ) ` w ) = D )
21 20 opeq2d 
 |-  ( w = W -> <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. = <. ( Scalar ` ndx ) , D >. )
22 14 18 21 tpeq123d 
 |-  ( w = W -> { <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } = { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , D >. } )
23 eqidd 
 |-  ( w = W -> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. = <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )
24 12 13 23 mpoeq123dv 
 |-  ( w = W -> ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) )
25 24 opeq2d 
 |-  ( w = W -> <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. = <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. )
26 25 sneqd 
 |-  ( w = W -> { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } = { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } )
27 22 26 uneq12d 
 |-  ( w = W -> ( { <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) = ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , D >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) )
28 eqid 
 |-  ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) = ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) )
29 tpex 
 |-  { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , D >. } e. _V
30 snex 
 |-  { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } e. _V
31 29 30 unex 
 |-  ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , D >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) e. _V
32 27 28 31 fvmpt 
 |-  ( W e. H -> ( ( w e. H |-> ( { <. ( Base ` ndx ) , ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) >. , <. ( +g ` ndx ) , ( f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) , g e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. ( ( LTrn ` K ) ` w ) |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` w ) >. } u. { <. ( .s ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , f e. ( ( ( LTrn ` K ) ` w ) X. ( ( TEndo ` K ) ` w ) ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) ` W ) = ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , D >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) )
33 8 32 sylan9eq 
 |-  ( ( K e. X /\ W e. H ) -> U = ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , D >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) )