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 ) )