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→∅∈GGrpAct∅

Proof

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