Metamath Proof Explorer


Theorem lactghmga

Description: The converse of galactghm . The uncurrying of a homomorphism into ( SymGrpY ) is a group action. Thus, group actions and group homomorphisms into a symmetric group are essentially equivalent notions. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses lactghmga.x X = Base G
lactghmga.h H = SymGrp Y
lactghmga.f ˙ = x X , y Y F x y
Assertion lactghmga F G GrpHom H ˙ G GrpAct Y

Proof

Step Hyp Ref Expression
1 lactghmga.x X = Base G
2 lactghmga.h H = SymGrp Y
3 lactghmga.f ˙ = x X , y Y F x y
4 ghmgrp1 F G GrpHom H G Grp
5 ghmgrp2 F G GrpHom H H Grp
6 grpn0 H Grp H
7 fvprc ¬ Y V SymGrp Y =
8 2 7 syl5eq ¬ Y V H =
9 8 necon1ai H Y V
10 5 6 9 3syl F G GrpHom H Y V
11 eqid Base H = Base H
12 1 11 ghmf F G GrpHom H F : X Base H
13 12 ffvelrnda F G GrpHom H x X F x Base H
14 10 adantr F G GrpHom H x X Y V
15 2 11 elsymgbas Y V F x Base H F x : Y 1-1 onto Y
16 14 15 syl F G GrpHom H x X F x Base H F x : Y 1-1 onto Y
17 13 16 mpbid F G GrpHom H x X F x : Y 1-1 onto Y
18 f1of F x : Y 1-1 onto Y F x : Y Y
19 17 18 syl F G GrpHom H x X F x : Y Y
20 19 ffvelrnda F G GrpHom H x X y Y F x y Y
21 20 ralrimiva F G GrpHom H x X y Y F x y Y
22 21 ralrimiva F G GrpHom H x X y Y F x y Y
23 3 fmpo x X y Y F x y Y ˙ : X × Y Y
24 22 23 sylib F G GrpHom H ˙ : X × Y Y
25 eqid 0 G = 0 G
26 1 25 grpidcl G Grp 0 G X
27 4 26 syl F G GrpHom H 0 G X
28 fveq2 x = 0 G F x = F 0 G
29 28 fveq1d x = 0 G F x y = F 0 G y
30 fveq2 y = z F 0 G y = F 0 G z
31 fvex F 0 G z V
32 29 30 3 31 ovmpo 0 G X z Y 0 G ˙ z = F 0 G z
33 27 32 sylan F G GrpHom H z Y 0 G ˙ z = F 0 G z
34 eqid 0 H = 0 H
35 25 34 ghmid F G GrpHom H F 0 G = 0 H
36 35 adantr F G GrpHom H z Y F 0 G = 0 H
37 10 adantr F G GrpHom H z Y Y V
38 2 symgid Y V I Y = 0 H
39 37 38 syl F G GrpHom H z Y I Y = 0 H
40 36 39 eqtr4d F G GrpHom H z Y F 0 G = I Y
41 40 fveq1d F G GrpHom H z Y F 0 G z = I Y z
42 fvresi z Y I Y z = z
43 42 adantl F G GrpHom H z Y I Y z = z
44 33 41 43 3eqtrd F G GrpHom H z Y 0 G ˙ z = z
45 12 ad2antrr F G GrpHom H z Y u X v X F : X Base H
46 simprr F G GrpHom H z Y u X v X v X
47 45 46 ffvelrnd F G GrpHom H z Y u X v X F v Base H
48 10 ad2antrr F G GrpHom H z Y u X v X Y V
49 2 11 elsymgbas Y V F v Base H F v : Y 1-1 onto Y
50 48 49 syl F G GrpHom H z Y u X v X F v Base H F v : Y 1-1 onto Y
51 47 50 mpbid F G GrpHom H z Y u X v X F v : Y 1-1 onto Y
52 f1of F v : Y 1-1 onto Y F v : Y Y
53 51 52 syl F G GrpHom H z Y u X v X F v : Y Y
54 simplr F G GrpHom H z Y u X v X z Y
55 fvco3 F v : Y Y z Y F u F v z = F u F v z
56 53 54 55 syl2anc F G GrpHom H z Y u X v X F u F v z = F u F v z
57 simpll F G GrpHom H z Y u X v X F G GrpHom H
58 simprl F G GrpHom H z Y u X v X u X
59 eqid + G = + G
60 eqid + H = + H
61 1 59 60 ghmlin F G GrpHom H u X v X F u + G v = F u + H F v
62 57 58 46 61 syl3anc F G GrpHom H z Y u X v X F u + G v = F u + H F v
63 45 58 ffvelrnd F G GrpHom H z Y u X v X F u Base H
64 2 11 60 symgov F u Base H F v Base H F u + H F v = F u F v
65 63 47 64 syl2anc F G GrpHom H z Y u X v X F u + H F v = F u F v
66 62 65 eqtrd F G GrpHom H z Y u X v X F u + G v = F u F v
67 66 fveq1d F G GrpHom H z Y u X v X F u + G v z = F u F v z
68 53 54 ffvelrnd F G GrpHom H z Y u X v X F v z Y
69 fveq2 x = u F x = F u
70 69 fveq1d x = u F x y = F u y
71 fveq2 y = F v z F u y = F u F v z
72 fvex F u F v z V
73 70 71 3 72 ovmpo u X F v z Y u ˙ F v z = F u F v z
74 58 68 73 syl2anc F G GrpHom H z Y u X v X u ˙ F v z = F u F v z
75 56 67 74 3eqtr4d F G GrpHom H z Y u X v X F u + G v z = u ˙ F v z
76 4 ad2antrr F G GrpHom H z Y u X v X G Grp
77 1 59 grpcl G Grp u X v X u + G v X
78 76 58 46 77 syl3anc F G GrpHom H z Y u X v X u + G v X
79 fveq2 x = u + G v F x = F u + G v
80 79 fveq1d x = u + G v F x y = F u + G v y
81 fveq2 y = z F u + G v y = F u + G v z
82 fvex F u + G v z V
83 80 81 3 82 ovmpo u + G v X z Y u + G v ˙ z = F u + G v z
84 78 54 83 syl2anc F G GrpHom H z Y u X v X u + G v ˙ z = F u + G v z
85 fveq2 x = v F x = F v
86 85 fveq1d x = v F x y = F v y
87 fveq2 y = z F v y = F v z
88 fvex F v z V
89 86 87 3 88 ovmpo v X z Y v ˙ z = F v z
90 46 54 89 syl2anc F G GrpHom H z Y u X v X v ˙ z = F v z
91 90 oveq2d F G GrpHom H z Y u X v X u ˙ v ˙ z = u ˙ F v z
92 75 84 91 3eqtr4d F G GrpHom H z Y u X v X u + G v ˙ z = u ˙ v ˙ z
93 92 ralrimivva F G GrpHom H z Y u X v X u + G v ˙ z = u ˙ v ˙ z
94 44 93 jca F G GrpHom H z Y 0 G ˙ z = z u X v X u + G v ˙ z = u ˙ v ˙ z
95 94 ralrimiva F G GrpHom H z Y 0 G ˙ z = z u X v X u + G v ˙ z = u ˙ v ˙ z
96 24 95 jca F G GrpHom H ˙ : X × Y Y z Y 0 G ˙ z = z u X v X u + G v ˙ z = u ˙ v ˙ z
97 1 59 25 isga ˙ G GrpAct Y G Grp Y V ˙ : X × Y Y z Y 0 G ˙ z = z u X v X u + G v ˙ z = u ˙ v ˙ z
98 4 10 96 97 syl21anbrc F G GrpHom H ˙ G GrpAct Y