Metamath Proof Explorer


Theorem gaid2

Description: A group operation is a left group action of the group on itself. (Contributed by FL, 17-May-2010) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses gaid2.1 X = Base G
gaid2.2 + ˙ = + G
gaid2.3 F = x X , y X x + ˙ y
Assertion gaid2 G Grp F G GrpAct X

Proof

Step Hyp Ref Expression
1 gaid2.1 X = Base G
2 gaid2.2 + ˙ = + G
3 gaid2.3 F = x X , y X x + ˙ y
4 1 subgid G Grp X SubGrp G
5 eqid G 𝑠 X = G 𝑠 X
6 1 2 5 3 subgga X SubGrp G F G 𝑠 X GrpAct X
7 4 6 syl G Grp F G 𝑠 X GrpAct X
8 1 ressid G Grp G 𝑠 X = G
9 8 oveq1d G Grp G 𝑠 X GrpAct X = G GrpAct X
10 7 9 eleqtrd G Grp F G GrpAct X