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 𝑋 ) ) |
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 𝑋 ) ) |