Step |
Hyp |
Ref |
Expression |
1 |
|
gaid2.1 |
|- X = ( Base ` G ) |
2 |
|
gaid2.2 |
|- .+ = ( +g ` G ) |
3 |
|
gaid2.3 |
|- F = ( x e. X , y e. X |-> ( x .+ y ) ) |
4 |
1
|
subgid |
|- ( G e. Grp -> X e. ( SubGrp ` G ) ) |
5 |
|
eqid |
|- ( G |`s X ) = ( G |`s X ) |
6 |
1 2 5 3
|
subgga |
|- ( X e. ( SubGrp ` G ) -> F e. ( ( G |`s X ) GrpAct X ) ) |
7 |
4 6
|
syl |
|- ( G e. Grp -> F e. ( ( G |`s X ) GrpAct X ) ) |
8 |
1
|
ressid |
|- ( G e. Grp -> ( G |`s X ) = G ) |
9 |
8
|
oveq1d |
|- ( G e. Grp -> ( ( G |`s X ) GrpAct X ) = ( G GrpAct X ) ) |
10 |
7 9
|
eleqtrd |
|- ( G e. Grp -> F e. ( G GrpAct X ) ) |