This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )