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 𝑋 = ( Base ‘ 𝐺 )
gaid2.2 + = ( +g𝐺 )
gaid2.3 𝐹 = ( 𝑥𝑋 , 𝑦𝑋 ↦ ( 𝑥 + 𝑦 ) )
Assertion gaid2 ( 𝐺 ∈ Grp → 𝐹 ∈ ( 𝐺 GrpAct 𝑋 ) )

Proof

Step Hyp Ref Expression
1 gaid2.1 𝑋 = ( Base ‘ 𝐺 )
2 gaid2.2 + = ( +g𝐺 )
3 gaid2.3 𝐹 = ( 𝑥𝑋 , 𝑦𝑋 ↦ ( 𝑥 + 𝑦 ) )
4 1 subgid ( 𝐺 ∈ Grp → 𝑋 ∈ ( SubGrp ‘ 𝐺 ) )
5 eqid ( 𝐺s 𝑋 ) = ( 𝐺s 𝑋 )
6 1 2 5 3 subgga ( 𝑋 ∈ ( SubGrp ‘ 𝐺 ) → 𝐹 ∈ ( ( 𝐺s 𝑋 ) GrpAct 𝑋 ) )
7 4 6 syl ( 𝐺 ∈ Grp → 𝐹 ∈ ( ( 𝐺s 𝑋 ) GrpAct 𝑋 ) )
8 1 ressid ( 𝐺 ∈ Grp → ( 𝐺s 𝑋 ) = 𝐺 )
9 8 oveq1d ( 𝐺 ∈ Grp → ( ( 𝐺s 𝑋 ) GrpAct 𝑋 ) = ( 𝐺 GrpAct 𝑋 ) )
10 7 9 eleqtrd ( 𝐺 ∈ Grp → 𝐹 ∈ ( 𝐺 GrpAct 𝑋 ) )