Metamath Proof Explorer


Theorem cayleylem2

Description: Lemma for cayley . (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses cayleylem1.x X = Base G
cayleylem1.p + ˙ = + G
cayleylem1.u 0 ˙ = 0 G
cayleylem1.h H = SymGrp X
cayleylem1.s S = Base H
cayleylem1.f F = g X a X g + ˙ a
Assertion cayleylem2 G Grp F : X 1-1 S

Proof

Step Hyp Ref Expression
1 cayleylem1.x X = Base G
2 cayleylem1.p + ˙ = + G
3 cayleylem1.u 0 ˙ = 0 G
4 cayleylem1.h H = SymGrp X
5 cayleylem1.s S = Base H
6 cayleylem1.f F = g X a X g + ˙ a
7 fveq1 F x = 0 H F x 0 ˙ = 0 H 0 ˙
8 simpr G Grp x X x X
9 1 3 grpidcl G Grp 0 ˙ X
10 9 adantr G Grp x X 0 ˙ X
11 6 1 grplactval x X 0 ˙ X F x 0 ˙ = x + ˙ 0 ˙
12 8 10 11 syl2anc G Grp x X F x 0 ˙ = x + ˙ 0 ˙
13 1 2 3 grprid G Grp x X x + ˙ 0 ˙ = x
14 12 13 eqtrd G Grp x X F x 0 ˙ = x
15 1 fvexi X V
16 4 symgid X V I X = 0 H
17 15 16 ax-mp I X = 0 H
18 17 fveq1i I X 0 ˙ = 0 H 0 ˙
19 fvresi 0 ˙ X I X 0 ˙ = 0 ˙
20 10 19 syl G Grp x X I X 0 ˙ = 0 ˙
21 18 20 eqtr3id G Grp x X 0 H 0 ˙ = 0 ˙
22 14 21 eqeq12d G Grp x X F x 0 ˙ = 0 H 0 ˙ x = 0 ˙
23 7 22 syl5ib G Grp x X F x = 0 H x = 0 ˙
24 23 ralrimiva G Grp x X F x = 0 H x = 0 ˙
25 1 2 3 4 5 6 cayleylem1 G Grp F G GrpHom H
26 eqid 0 H = 0 H
27 1 5 3 26 ghmf1 F G GrpHom H F : X 1-1 S x X F x = 0 H x = 0 ˙
28 25 27 syl G Grp F : X 1-1 S x X F x = 0 H x = 0 ˙
29 24 28 mpbird G Grp F : X 1-1 S