Metamath Proof Explorer

Theorem grplactcnv

Description: The left group action of element A of group G maps the underlying set X of G one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008) (Proof shortened by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses grplact.1 
|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
grplact.2 
|- X = ( Base ` G )
grplact.3 
|- .+ = ( +g ` G )
grplactcnv.4 
|- I = ( invg ` G )
Assertion grplactcnv 
|- ( ( G e. Grp /\ A e. X ) -> ( ( F ` A ) : X -1-1-onto-> X /\ `' ( F ` A ) = ( F ` ( I ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 grplact.1 
 |-  F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
2 grplact.2 
 |-  X = ( Base ` G )
3 grplact.3 
 |-  .+ = ( +g ` G )
4 grplactcnv.4 
 |-  I = ( invg ` G )
5 eqid 
 |-  ( a e. X |-> ( A .+ a ) ) = ( a e. X |-> ( A .+ a ) )
6 2 3 grpcl 
 |-  ( ( G e. Grp /\ A e. X /\ a e. X ) -> ( A .+ a ) e. X )
7 6 3expa 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ a e. X ) -> ( A .+ a ) e. X )
8 2 4 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( I ` A ) e. X )
9 2 3 grpcl 
 |-  ( ( G e. Grp /\ ( I ` A ) e. X /\ b e. X ) -> ( ( I ` A ) .+ b ) e. X )
10 9 3expa 
 |-  ( ( ( G e. Grp /\ ( I ` A ) e. X ) /\ b e. X ) -> ( ( I ` A ) .+ b ) e. X )
11 8 10 syldanl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ b e. X ) -> ( ( I ` A ) .+ b ) e. X )
12 eqcom 
 |-  ( a = ( ( I ` A ) .+ b ) <-> ( ( I ` A ) .+ b ) = a )
13 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
14 2 3 13 4 grplinv 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( I ` A ) .+ A ) = ( 0g ` G ) )
15 14 adantr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( ( I ` A ) .+ A ) = ( 0g ` G ) )
16 15 oveq1d 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( I ` A ) .+ A ) .+ a ) = ( ( 0g ` G ) .+ a ) )
17 simpll 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> G e. Grp )
18 8 adantr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( I ` A ) e. X )
19 simplr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> A e. X )
20 simprl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> a e. X )
21 2 3 grpass 
 |-  ( ( G e. Grp /\ ( ( I ` A ) e. X /\ A e. X /\ a e. X ) ) -> ( ( ( I ` A ) .+ A ) .+ a ) = ( ( I ` A ) .+ ( A .+ a ) ) )
22 17 18 19 20 21 syl13anc 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( I ` A ) .+ A ) .+ a ) = ( ( I ` A ) .+ ( A .+ a ) ) )
23 2 3 13 grplid 
 |-  ( ( G e. Grp /\ a e. X ) -> ( ( 0g ` G ) .+ a ) = a )
24 23 ad2ant2r 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( ( 0g ` G ) .+ a ) = a )
25 16 22 24 3eqtr3rd 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> a = ( ( I ` A ) .+ ( A .+ a ) ) )
26 25 eqeq2d 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( I ` A ) .+ b ) = a <-> ( ( I ` A ) .+ b ) = ( ( I ` A ) .+ ( A .+ a ) ) ) )
27 12 26 syl5bb 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( a = ( ( I ` A ) .+ b ) <-> ( ( I ` A ) .+ b ) = ( ( I ` A ) .+ ( A .+ a ) ) ) )
28 simprr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> b e. X )
29 7 adantrr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( A .+ a ) e. X )
30 2 3 grplcan 
 |-  ( ( G e. Grp /\ ( b e. X /\ ( A .+ a ) e. X /\ ( I ` A ) e. X ) ) -> ( ( ( I ` A ) .+ b ) = ( ( I ` A ) .+ ( A .+ a ) ) <-> b = ( A .+ a ) ) )
31 17 28 29 18 30 syl13anc 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( I ` A ) .+ b ) = ( ( I ` A ) .+ ( A .+ a ) ) <-> b = ( A .+ a ) ) )
32 27 31 bitrd 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( a e. X /\ b e. X ) ) -> ( a = ( ( I ` A ) .+ b ) <-> b = ( A .+ a ) ) )
33 5 7 11 32 f1ocnv2d 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( a e. X |-> ( A .+ a ) ) : X -1-1-onto-> X /\ `' ( a e. X |-> ( A .+ a ) ) = ( b e. X |-> ( ( I ` A ) .+ b ) ) ) )
34 1 2 grplactfval 
 |-  ( A e. X -> ( F ` A ) = ( a e. X |-> ( A .+ a ) ) )
35 34 adantl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( F ` A ) = ( a e. X |-> ( A .+ a ) ) )
36 35 f1oeq1d 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( F ` A ) : X -1-1-onto-> X <-> ( a e. X |-> ( A .+ a ) ) : X -1-1-onto-> X ) )
37 35 cnveqd 
 |-  ( ( G e. Grp /\ A e. X ) -> `' ( F ` A ) = `' ( a e. X |-> ( A .+ a ) ) )
38 1 2 grplactfval 
 |-  ( ( I ` A ) e. X -> ( F ` ( I ` A ) ) = ( a e. X |-> ( ( I ` A ) .+ a ) ) )
39 oveq2 
 |-  ( a = b -> ( ( I ` A ) .+ a ) = ( ( I ` A ) .+ b ) )
40 39 cbvmptv 
 |-  ( a e. X |-> ( ( I ` A ) .+ a ) ) = ( b e. X |-> ( ( I ` A ) .+ b ) )
41 38 40 eqtrdi 
 |-  ( ( I ` A ) e. X -> ( F ` ( I ` A ) ) = ( b e. X |-> ( ( I ` A ) .+ b ) ) )
42 8 41 syl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( F ` ( I ` A ) ) = ( b e. X |-> ( ( I ` A ) .+ b ) ) )
43 37 42 eqeq12d 
 |-  ( ( G e. Grp /\ A e. X ) -> ( `' ( F ` A ) = ( F ` ( I ` A ) ) <-> `' ( a e. X |-> ( A .+ a ) ) = ( b e. X |-> ( ( I ` A ) .+ b ) ) ) )
44 36 43 anbi12d 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( ( F ` A ) : X -1-1-onto-> X /\ `' ( F ` A ) = ( F ` ( I ` A ) ) ) <-> ( ( a e. X |-> ( A .+ a ) ) : X -1-1-onto-> X /\ `' ( a e. X |-> ( A .+ a ) ) = ( b e. X |-> ( ( I ` A ) .+ b ) ) ) ) )
45 33 44 mpbird 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( F ` A ) : X -1-1-onto-> X /\ `' ( F ` A ) = ( F ` ( I ` A ) ) ) )