Metamath Proof Explorer

Theorem grplmulf1o

Description: Left multiplication by a group element is a bijection on any group. (Contributed by Mario Carneiro, 17-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 grplmulf1o.b 
 |-  B = ( Base ` G )
2 grplmulf1o.p 
 |-  .+ = ( +g ` G )
3 grplmulf1o.n 
 |-  F = ( x e. B |-> ( X .+ x ) )
4 1 2 grpcl 
 |-  ( ( G e. Grp /\ X e. B /\ x e. B ) -> ( X .+ x ) e. B )
5 4 3expa 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ x e. B ) -> ( X .+ x ) e. B )
6 eqid 
 |-  ( invg ` G ) = ( invg ` G )
7 1 6 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( invg ` G ) ` X ) e. B )
8 1 2 grpcl 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` X ) e. B /\ y e. B ) -> ( ( ( invg ` G ) ` X ) .+ y ) e. B )
9 8 3expa 
 |-  ( ( ( G e. Grp /\ ( ( invg ` G ) ` X ) e. B ) /\ y e. B ) -> ( ( ( invg ` G ) ` X ) .+ y ) e. B )
10 7 9 syldanl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ y e. B ) -> ( ( ( invg ` G ) ` X ) .+ y ) e. B )
11 eqcom 
 |-  ( x = ( ( ( invg ` G ) ` X ) .+ y ) <-> ( ( ( invg ` G ) ` X ) .+ y ) = x )
12 simpll 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> G e. Grp )
13 10 adantrl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( invg ` G ) ` X ) .+ y ) e. B )
14 simprl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> x e. B )
15 simplr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> X e. B )
16 1 2 grplcan 
 |-  ( ( G e. Grp /\ ( ( ( ( invg ` G ) ` X ) .+ y ) e. B /\ x e. B /\ X e. B ) ) -> ( ( X .+ ( ( ( invg ` G ) ` X ) .+ y ) ) = ( X .+ x ) <-> ( ( ( invg ` G ) ` X ) .+ y ) = x ) )
17 12 13 14 15 16 syl13anc 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( X .+ ( ( ( invg ` G ) ` X ) .+ y ) ) = ( X .+ x ) <-> ( ( ( invg ` G ) ` X ) .+ y ) = x ) )
18 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
19 1 2 18 6 grprinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .+ ( ( invg ` G ) ` X ) ) = ( 0g ` G ) )
20 19 adantr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( X .+ ( ( invg ` G ) ` X ) ) = ( 0g ` G ) )
21 20 oveq1d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( X .+ ( ( invg ` G ) ` X ) ) .+ y ) = ( ( 0g ` G ) .+ y ) )
22 7 adantr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( invg ` G ) ` X ) e. B )
23 simprr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> y e. B )
24 1 2 grpass 
 |-  ( ( G e. Grp /\ ( X e. B /\ ( ( invg ` G ) ` X ) e. B /\ y e. B ) ) -> ( ( X .+ ( ( invg ` G ) ` X ) ) .+ y ) = ( X .+ ( ( ( invg ` G ) ` X ) .+ y ) ) )
25 12 15 22 23 24 syl13anc 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( X .+ ( ( invg ` G ) ` X ) ) .+ y ) = ( X .+ ( ( ( invg ` G ) ` X ) .+ y ) ) )
26 1 2 18 grplid 
 |-  ( ( G e. Grp /\ y e. B ) -> ( ( 0g ` G ) .+ y ) = y )
27 26 ad2ant2rl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( 0g ` G ) .+ y ) = y )
28 21 25 27 3eqtr3d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( X .+ ( ( ( invg ` G ) ` X ) .+ y ) ) = y )
29 28 eqeq1d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( X .+ ( ( ( invg ` G ) ` X ) .+ y ) ) = ( X .+ x ) <-> y = ( X .+ x ) ) )
30 17 29 bitr3d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( ( invg ` G ) ` X ) .+ y ) = x <-> y = ( X .+ x ) ) )
31 11 30 syl5bb 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( x e. B /\ y e. B ) ) -> ( x = ( ( ( invg ` G ) ` X ) .+ y ) <-> y = ( X .+ x ) ) )
32 3 5 10 31 f1o2d 
 |-  ( ( G e. Grp /\ X e. B ) -> F : B -1-1-onto-> B )