Step |
Hyp |
Ref |
Expression |
1 |
|
tgrpset.h |
|- H = ( LHyp ` K ) |
2 |
|
tgrpset.t |
|- T = ( ( LTrn ` K ) ` W ) |
3 |
|
tgrpset.g |
|- G = ( ( TGrp ` K ) ` W ) |
4 |
1
|
tgrpfset |
|- ( K e. V -> ( TGrp ` K ) = ( w e. H |-> { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. } ) ) |
5 |
4
|
fveq1d |
|- ( K e. V -> ( ( TGrp ` K ) ` W ) = ( ( w e. H |-> { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. } ) ` W ) ) |
6 |
|
fveq2 |
|- ( w = W -> ( ( LTrn ` K ) ` w ) = ( ( LTrn ` K ) ` W ) ) |
7 |
6
|
opeq2d |
|- ( w = W -> <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. = <. ( Base ` ndx ) , ( ( LTrn ` K ) ` W ) >. ) |
8 |
|
eqidd |
|- ( w = W -> ( f o. g ) = ( f o. g ) ) |
9 |
6 6 8
|
mpoeq123dv |
|- ( w = W -> ( 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 |
|- ( w = W -> <. ( +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 |
7 10
|
preq12d |
|- ( w = W -> { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. } = { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` W ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` W ) , g e. ( ( LTrn ` K ) ` W ) |-> ( f o. g ) ) >. } ) |
12 |
|
eqid |
|- ( w e. H |-> { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. } ) = ( w e. H |-> { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. } ) |
13 |
|
prex |
|- { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` W ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` W ) , g e. ( ( LTrn ` K ) ` W ) |-> ( f o. g ) ) >. } e. _V |
14 |
11 12 13
|
fvmpt |
|- ( W e. H -> ( ( w e. H |-> { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. } ) ` W ) = { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` W ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` W ) , g e. ( ( LTrn ` K ) ` W ) |-> ( f o. g ) ) >. } ) |
15 |
2
|
opeq2i |
|- <. ( Base ` ndx ) , T >. = <. ( Base ` ndx ) , ( ( LTrn ` K ) ` W ) >. |
16 |
|
eqid |
|- ( f o. g ) = ( f o. g ) |
17 |
2 2 16
|
mpoeq123i |
|- ( f e. T , g e. T |-> ( f o. g ) ) = ( f e. ( ( LTrn ` K ) ` W ) , g e. ( ( LTrn ` K ) ` W ) |-> ( f o. g ) ) |
18 |
17
|
opeq2i |
|- <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. = <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` W ) , g e. ( ( LTrn ` K ) ` W ) |-> ( f o. g ) ) >. |
19 |
15 18
|
preq12i |
|- { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } = { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` W ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` W ) , g e. ( ( LTrn ` K ) ` W ) |-> ( f o. g ) ) >. } |
20 |
14 19
|
eqtr4di |
|- ( W e. H -> ( ( w e. H |-> { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. } ) ` W ) = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) |
21 |
5 20
|
sylan9eq |
|- ( ( K e. V /\ W e. H ) -> ( ( TGrp ` K ) ` W ) = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) |
22 |
3 21
|
syl5eq |
|- ( ( K e. V /\ W e. H ) -> G = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) |