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 e. X , y e. Y |-> ( ( F ` x ) ` y ) )
Assertion lactghmga 
|- ( F e. ( G GrpHom H ) -> .(+) e. ( G GrpAct Y ) )

Proof

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