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 𝑋 = ( Base ‘ 𝐺 )
lactghmga.h 𝐻 = ( SymGrp ‘ 𝑌 )
lactghmga.f = ( 𝑥𝑋 , 𝑦𝑌 ↦ ( ( 𝐹𝑥 ) ‘ 𝑦 ) )
Assertion lactghmga ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → ∈ ( 𝐺 GrpAct 𝑌 ) )

Proof

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