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={\mathrm{Base}}_G$$
	gaid2.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	gaid2.3	$$⊢F=\left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)$$
Assertion	gaid2	$$⊢G\in \mathrm{Grp}\to F\in \left(G\mathrm{GrpAct}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		gaid2.1	$$⊢X={\mathrm{Base}}_G$$
2		gaid2.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gaid2.3	$$⊢F=\left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)$$
4	1	subgid	$$⊢G\in \mathrm{Grp}\to X\in \mathrm{SubGrp}\left(G\right)$$
5		eqid	$$⊢G{\upharpoonright }_{𝑠}X=G{\upharpoonright }_{𝑠}X$$
6	1 2 5 3	subgga	$$⊢X\in \mathrm{SubGrp}\left(G\right)\to F\in \left(\left(G{\upharpoonright }_{𝑠}X\right)\mathrm{GrpAct}X\right)$$
7	4 6	syl	$$⊢G\in \mathrm{Grp}\to F\in \left(\left(G{\upharpoonright }_{𝑠}X\right)\mathrm{GrpAct}X\right)$$
8	1	ressid	$$⊢G\in \mathrm{Grp}\to G{\upharpoonright }_{𝑠}X=G$$
9	8	oveq1d	$$⊢G\in \mathrm{Grp}\to \left(G{\upharpoonright }_{𝑠}X\right)\mathrm{GrpAct}X=G\mathrm{GrpAct}X$$
10	7 9	eleqtrd	$$⊢G\in \mathrm{Grp}\to F\in \left(G\mathrm{GrpAct}X\right)$$