Metamath Proof Explorer

Theorem ga0

Description: The action of a group on the empty set. (Contributed by Jeff Hankins, 11-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Assertion ga0 ⊢ G ∈ Grp → ∅ ∈ G GrpAct ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 1 jctr ⊢ G ∈ Grp → G ∈ Grp ∧ ∅ ∈ V
3 f0 ⊢ ∅ : ∅ ⟶ ∅
4 xp0 ⊢ Base G × ∅ = ∅
5 4 feq2i ⊢ ∅ : Base G × ∅ ⟶ ∅ ↔ ∅ : ∅ ⟶ ∅
6 3 5 mpbir ⊢ ∅ : Base G × ∅ ⟶ ∅
7 ral0 ⊢ ∀ x ∈ ∅ 0 G ∅ x = x ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ∅ x = y ∅ z ∅ x
8 6 7 pm3.2i ⊢ ∅ : Base G × ∅ ⟶ ∅ ∧ ∀ x ∈ ∅ 0 G ∅ x = x ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ∅ x = y ∅ z ∅ x
9 eqid ⊢ Base G = Base G
10 eqid ⊢ + G = + G
11 eqid ⊢ 0 G = 0 G
12 9 10 11 isga ⊢ ∅ ∈ G GrpAct ∅ ↔ G ∈ Grp ∧ ∅ ∈ V ∧ ∅ : Base G × ∅ ⟶ ∅ ∧ ∀ x ∈ ∅ 0 G ∅ x = x ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ∅ x = y ∅ z ∅ x
13 2 8 12 sylanblrc ⊢ G ∈ Grp → ∅ ∈ G GrpAct ∅