Metamath Proof Explorer

Theorem gapm

Description: The action of a particular group element is a permutation of the base set. (Contributed by Jeff Hankins, 11-Aug-2009) (Proof shortened by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses gapm.1 
|- X = ( Base ` G )
gapm.2 
|- F = ( x e. Y |-> ( A .(+) x ) )
Assertion gapm 
|- ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) -> F : Y -1-1-onto-> Y )

Proof

Step Hyp Ref Expression
1 gapm.1 
 |-  X = ( Base ` G )
2 gapm.2 
 |-  F = ( x e. Y |-> ( A .(+) x ) )
3 1 gaf 
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
4 3 ad2antrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ x e. Y ) -> .(+) : ( X X. Y ) --> Y )
5 simplr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ x e. Y ) -> A e. X )
6 simpr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ x e. Y ) -> x e. Y )
7 4 5 6 fovrnd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ x e. Y ) -> ( A .(+) x ) e. Y )
8 3 ad2antrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ y e. Y ) -> .(+) : ( X X. Y ) --> Y )
9 gagrp 
 |-  ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
10 9 ad2antrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ y e. Y ) -> G e. Grp )
11 simplr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ y e. Y ) -> A e. X )
12 eqid 
 |-  ( invg ` G ) = ( invg ` G )
13 1 12 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X )
14 10 11 13 syl2anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ y e. Y ) -> ( ( invg ` G ) ` A ) e. X )
15 simpr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ y e. Y ) -> y e. Y )
16 8 14 15 fovrnd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ y e. Y ) -> ( ( ( invg ` G ) ` A ) .(+) y ) e. Y )
17 simpll 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ ( x e. Y /\ y e. Y ) ) -> .(+) e. ( G GrpAct Y ) )
18 simplr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ ( x e. Y /\ y e. Y ) ) -> A e. X )
19 simprl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ ( x e. Y /\ y e. Y ) ) -> x e. Y )
20 simprr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ ( x e. Y /\ y e. Y ) ) -> y e. Y )
21 1 12 gacan 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ x e. Y /\ y e. Y ) ) -> ( ( A .(+) x ) = y <-> ( ( ( invg ` G ) ` A ) .(+) y ) = x ) )
22 17 18 19 20 21 syl13anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ ( x e. Y /\ y e. Y ) ) -> ( ( A .(+) x ) = y <-> ( ( ( invg ` G ) ` A ) .(+) y ) = x ) )
23 22 bicomd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ ( x e. Y /\ y e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) .(+) y ) = x <-> ( A .(+) x ) = y ) )
24 eqcom 
 |-  ( x = ( ( ( invg ` G ) ` A ) .(+) y ) <-> ( ( ( invg ` G ) ` A ) .(+) y ) = x )
25 eqcom 
 |-  ( y = ( A .(+) x ) <-> ( A .(+) x ) = y )
26 23 24 25 3bitr4g 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) /\ ( x e. Y /\ y e. Y ) ) -> ( x = ( ( ( invg ` G ) ` A ) .(+) y ) <-> y = ( A .(+) x ) ) )
27 2 7 16 26 f1o2d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) -> F : Y -1-1-onto-> Y )