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 eqtrid ⊢ ( ¬ 𝑌 ∈ 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 𝑌 ) )