This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \underset{˙}{+} = +_{G}$
		gaid2.3	$⊢ F = (x \in X, y \in X ⟼ x \underset{˙}{+} y)$
	Assertion	gaid2	$⊢ G \in Grp \to F \in (G GrpAct X)$

Proof

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