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