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
grplmulf1o.n F = x B X + ˙ x
Assertion grplmulf1o G Grp X B F : B 1-1 onto B

Proof

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