Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
⊢ ∅ ∈ V |
2 |
1
|
jctr |
⊢ ( 𝐺 ∈ Grp → ( 𝐺 ∈ Grp ∧ ∅ ∈ V ) ) |
3 |
|
f0 |
⊢ ∅ : ∅ ⟶ ∅ |
4 |
|
xp0 |
⊢ ( ( Base ‘ 𝐺 ) × ∅ ) = ∅ |
5 |
4
|
feq2i |
⊢ ( ∅ : ( ( Base ‘ 𝐺 ) × ∅ ) ⟶ ∅ ↔ ∅ : ∅ ⟶ ∅ ) |
6 |
3 5
|
mpbir |
⊢ ∅ : ( ( Base ‘ 𝐺 ) × ∅ ) ⟶ ∅ |
7 |
|
ral0 |
⊢ ∀ 𝑥 ∈ ∅ ( ( ( 0g ‘ 𝐺 ) ∅ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∅ 𝑥 ) = ( 𝑦 ∅ ( 𝑧 ∅ 𝑥 ) ) ) |
8 |
6 7
|
pm3.2i |
⊢ ( ∅ : ( ( Base ‘ 𝐺 ) × ∅ ) ⟶ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( ( 0g ‘ 𝐺 ) ∅ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∅ 𝑥 ) = ( 𝑦 ∅ ( 𝑧 ∅ 𝑥 ) ) ) ) |
9 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
10 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
11 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
12 |
9 10 11
|
isga |
⊢ ( ∅ ∈ ( 𝐺 GrpAct ∅ ) ↔ ( ( 𝐺 ∈ Grp ∧ ∅ ∈ V ) ∧ ( ∅ : ( ( Base ‘ 𝐺 ) × ∅ ) ⟶ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( ( 0g ‘ 𝐺 ) ∅ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∅ 𝑥 ) = ( 𝑦 ∅ ( 𝑧 ∅ 𝑥 ) ) ) ) ) ) |
13 |
2 8 12
|
sylanblrc |
⊢ ( 𝐺 ∈ Grp → ∅ ∈ ( 𝐺 GrpAct ∅ ) ) |