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 e. Grp -> (/) e. ( G GrpAct (/) ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 jctr 
 |-  ( G e. Grp -> ( G e. Grp /\ (/) e. _V ) )
3 f0 
 |-  (/) : (/) --> (/)
4 xp0 
 |-  ( ( Base ` G ) X. (/) ) = (/)
5 4 feq2i 
 |-  ( (/) : ( ( Base ` G ) X. (/) ) --> (/) <-> (/) : (/) --> (/) )
6 3 5 mpbir 
 |-  (/) : ( ( Base ` G ) X. (/) ) --> (/)
7 ral0 
 |-  A. x e. (/) ( ( ( 0g ` G ) (/) x ) = x /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) (/) x ) = ( y (/) ( z (/) x ) ) )
8 6 7 pm3.2i 
 |-  ( (/) : ( ( Base ` G ) X. (/) ) --> (/) /\ A. x e. (/) ( ( ( 0g ` G ) (/) x ) = x /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) (/) x ) = ( y (/) ( z (/) x ) ) ) )
9 eqid 
 |-  ( Base ` G ) = ( Base ` G )
10 eqid 
 |-  ( +g ` G ) = ( +g ` G )
11 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
12 9 10 11 isga 
 |-  ( (/) e. ( G GrpAct (/) ) <-> ( ( G e. Grp /\ (/) e. _V ) /\ ( (/) : ( ( Base ` G ) X. (/) ) --> (/) /\ A. x e. (/) ( ( ( 0g ` G ) (/) x ) = x /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) (/) x ) = ( y (/) ( z (/) x ) ) ) ) ) )
13 2 8 12 sylanblrc 
 |-  ( G e. Grp -> (/) e. ( G GrpAct (/) ) )