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