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 |
|
tgrp.o |
|- .+ = ( +g ` G ) |
5 |
1 2 3
|
tgrpset |
|- ( ( K e. V /\ W e. H ) -> G = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) |
6 |
5
|
fveq2d |
|- ( ( K e. V /\ W e. H ) -> ( +g ` G ) = ( +g ` { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) ) |
7 |
2
|
fvexi |
|- T e. _V |
8 |
7 7
|
mpoex |
|- ( f e. T , g e. T |-> ( f o. g ) ) e. _V |
9 |
|
eqid |
|- { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } |
10 |
9
|
grpplusg |
|- ( ( f e. T , g e. T |-> ( f o. g ) ) e. _V -> ( f e. T , g e. T |-> ( f o. g ) ) = ( +g ` { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) ) |
11 |
8 10
|
ax-mp |
|- ( f e. T , g e. T |-> ( f o. g ) ) = ( +g ` { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) |
12 |
6 4 11
|
3eqtr4g |
|- ( ( K e. V /\ W e. H ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) ) |