Metamath Proof Explorer


Theorem gafo

Description: A group action is onto its base set. (Contributed by Jeff Hankins, 10-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypothesis gaf.1
|- X = ( Base ` G )
Assertion gafo
|- ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) -onto-> Y )

Proof

Step Hyp Ref Expression
1 gaf.1
 |-  X = ( Base ` G )
2 1 gaf
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
3 gagrp
 |-  ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
4 3 adantr
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> G e. Grp )
5 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
6 1 5 grpidcl
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
7 4 6 syl
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> ( 0g ` G ) e. X )
8 simpr
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> x e. Y )
9 5 gagrpid
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> ( ( 0g ` G ) .(+) x ) = x )
10 9 eqcomd
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> x = ( ( 0g ` G ) .(+) x ) )
11 rspceov
 |-  ( ( ( 0g ` G ) e. X /\ x e. Y /\ x = ( ( 0g ` G ) .(+) x ) ) -> E. y e. X E. z e. Y x = ( y .(+) z ) )
12 7 8 10 11 syl3anc
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> E. y e. X E. z e. Y x = ( y .(+) z ) )
13 12 ralrimiva
 |-  ( .(+) e. ( G GrpAct Y ) -> A. x e. Y E. y e. X E. z e. Y x = ( y .(+) z ) )
14 foov
 |-  ( .(+) : ( X X. Y ) -onto-> Y <-> ( .(+) : ( X X. Y ) --> Y /\ A. x e. Y E. y e. X E. z e. Y x = ( y .(+) z ) ) )
15 2 13 14 sylanbrc
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) -onto-> Y )