Metamath Proof Explorer

Theorem grpraddf1o

Description: Right addition by a group element is a bijection on any group. (Contributed by SN, 28-Apr-2012)

Ref Expression
Hypotheses grpraddf1o.b 
|- B = ( Base ` G )
grpraddf1o.p 
|- .+ = ( +g ` G )
grpraddf1o.n 
|- F = ( x e. B |-> ( x .+ X ) )
Assertion grpraddf1o 
|- ( ( G e. Grp /\ X e. B ) -> F : B -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 grpraddf1o.b 
 |-  B = ( Base ` G )
2 grpraddf1o.p 
 |-  .+ = ( +g ` G )
3 grpraddf1o.n 
 |-  F = ( x e. B |-> ( x .+ X ) )
4 simpll 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ x e. B ) -> G e. Grp )
5 simpr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ x e. B ) -> x e. B )
6 simplr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ x e. B ) -> X e. B )
7 1 2 4 5 6 grpcld 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ x e. B ) -> ( x .+ X ) e. B )
8 simpll 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ y e. B ) -> G e. Grp )
9 simpr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ y e. B ) -> y e. B )
10 eqid 
 |-  ( invg ` G ) = ( invg ` G )
11 simplr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ y e. B ) -> X e. B )
12 1 10 8 11 grpinvcld 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ y e. B ) -> ( ( invg ` G ) ` X ) e. B )
13 1 2 8 9 12 grpcld 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ y e. B ) -> ( y .+ ( ( invg ` G ) ` X ) ) e. B )
14 eqcom 
 |-  ( x = ( y .+ ( ( invg ` G ) ` X ) ) <-> ( y .+ ( ( invg ` G ) ` X ) ) = x )
15 simpll 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> G e. Grp )
16 13 adantrl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( y .+ ( ( invg ` G ) ` X ) ) e. B )
17 simprl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> x e. B )
18 simplr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> X e. B )
19 1 2 grprcan 
 |-  ( ( G e. Grp /\ ( ( y .+ ( ( invg ` G ) ` X ) ) e. B /\ x e. B /\ X e. B ) ) -> ( ( ( y .+ ( ( invg ` G ) ` X ) ) .+ X ) = ( x .+ X ) <-> ( y .+ ( ( invg ` G ) ` X ) ) = x ) )
20 15 16 17 18 19 syl13anc 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( y .+ ( ( invg ` G ) ` X ) ) .+ X ) = ( x .+ X ) <-> ( y .+ ( ( invg ` G ) ` X ) ) = x ) )
21 simprr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> y e. B )
22 12 adantrl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( invg ` G ) ` X ) e. B )
23 1 2 15 21 22 18 grpassd 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( y .+ ( ( invg ` G ) ` X ) ) .+ X ) = ( y .+ ( ( ( invg ` G ) ` X ) .+ X ) ) )
24 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
25 1 2 24 10 grplinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( ( invg ` G ) ` X ) .+ X ) = ( 0g ` G ) )
26 25 adantr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( invg ` G ) ` X ) .+ X ) = ( 0g ` G ) )
27 26 oveq2d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( y .+ ( ( ( invg ` G ) ` X ) .+ X ) ) = ( y .+ ( 0g ` G ) ) )
28 1 2 24 grprid 
 |-  ( ( G e. Grp /\ y e. B ) -> ( y .+ ( 0g ` G ) ) = y )
29 28 ad2ant2rl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( y .+ ( 0g ` G ) ) = y )
30 23 27 29 3eqtrd 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( y .+ ( ( invg ` G ) ` X ) ) .+ X ) = y )
31 30 eqeq1d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( y .+ ( ( invg ` G ) ` X ) ) .+ X ) = ( x .+ X ) <-> y = ( x .+ X ) ) )
32 20 31 bitr3d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( y .+ ( ( invg ` G ) ` X ) ) = x <-> y = ( x .+ X ) ) )
33 14 32 bitrid 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( x = ( y .+ ( ( invg ` G ) ` X ) ) <-> y = ( x .+ X ) ) )
34 3 7 13 33 f1o2d 
 |-  ( ( G e. Grp /\ X e. B ) -> F : B -1-1-onto-> B )