| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ghmgrp1 19237 | . 2
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp) | 
| 2 |  | ghmgrp2 19238 | . . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp) | 
| 3 |  | grpn0 18990 | . . 3
⊢ (𝐻 ∈ Grp → 𝐻 ≠ ∅) | 
| 4 |  | lactghmga.h | . . . . 5
⊢ 𝐻 = (SymGrp‘𝑌) | 
| 5 |  | fvprc 6897 | . . . . 5
⊢ (¬
𝑌 ∈ V →
(SymGrp‘𝑌) =
∅) | 
| 6 | 4, 5 | eqtrid 2788 | . . . 4
⊢ (¬
𝑌 ∈ V → 𝐻 = ∅) | 
| 7 | 6 | necon1ai 2967 | . . 3
⊢ (𝐻 ≠ ∅ → 𝑌 ∈ V) | 
| 8 | 2, 3, 7 | 3syl 18 | . 2
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝑌 ∈ V) | 
| 9 |  | lactghmga.x | . . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝐺) | 
| 10 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 11 | 9, 10 | ghmf 19239 | . . . . . . . . . 10
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐹:𝑋⟶(Base‘𝐻)) | 
| 12 | 11 | ffvelcdmda 7103 | . . . . . . . . 9
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (Base‘𝐻)) | 
| 13 | 8 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → 𝑌 ∈ V) | 
| 14 | 4, 10 | elsymgbas 19392 | . . . . . . . . . 10
⊢ (𝑌 ∈ V → ((𝐹‘𝑥) ∈ (Base‘𝐻) ↔ (𝐹‘𝑥):𝑌–1-1-onto→𝑌)) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . 9
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) ∈ (Base‘𝐻) ↔ (𝐹‘𝑥):𝑌–1-1-onto→𝑌)) | 
| 16 | 12, 15 | mpbid 232 | . . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥):𝑌–1-1-onto→𝑌) | 
| 17 |  | f1of 6847 | . . . . . . . 8
⊢ ((𝐹‘𝑥):𝑌–1-1-onto→𝑌 → (𝐹‘𝑥):𝑌⟶𝑌) | 
| 18 | 16, 17 | syl 17 | . . . . . . 7
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥):𝑌⟶𝑌) | 
| 19 | 18 | ffvelcdmda 7103 | . . . . . 6
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → ((𝐹‘𝑥)‘𝑦) ∈ 𝑌) | 
| 20 | 19 | ralrimiva 3145 | . . . . 5
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ((𝐹‘𝑥)‘𝑦) ∈ 𝑌) | 
| 21 | 20 | ralrimiva 3145 | . . . 4
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝐹‘𝑥)‘𝑦) ∈ 𝑌) | 
| 22 |  | lactghmga.f | . . . . 5
⊢  ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝐹‘𝑥)‘𝑦)) | 
| 23 | 22 | fmpo 8094 | . . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 ((𝐹‘𝑥)‘𝑦) ∈ 𝑌 ↔ ⊕ :(𝑋 × 𝑌)⟶𝑌) | 
| 24 | 21, 23 | sylib 218 | . . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ⊕ :(𝑋 × 𝑌)⟶𝑌) | 
| 25 |  | eqid 2736 | . . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 26 | 9, 25 | grpidcl 18984 | . . . . . . . 8
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) | 
| 27 | 1, 26 | syl 17 | . . . . . . 7
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (0g‘𝐺) ∈ 𝑋) | 
| 28 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑥 = (0g‘𝐺) → (𝐹‘𝑥) = (𝐹‘(0g‘𝐺))) | 
| 29 | 28 | fveq1d 6907 | . . . . . . . 8
⊢ (𝑥 = (0g‘𝐺) → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘(0g‘𝐺))‘𝑦)) | 
| 30 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝐹‘(0g‘𝐺))‘𝑦) = ((𝐹‘(0g‘𝐺))‘𝑧)) | 
| 31 |  | fvex 6918 | . . . . . . . 8
⊢ ((𝐹‘(0g‘𝐺))‘𝑧) ∈ V | 
| 32 | 29, 30, 22, 31 | ovmpo 7594 | . . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = ((𝐹‘(0g‘𝐺))‘𝑧)) | 
| 33 | 27, 32 | sylan 580 | . . . . . 6
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = ((𝐹‘(0g‘𝐺))‘𝑧)) | 
| 34 |  | eqid 2736 | . . . . . . . . . 10
⊢
(0g‘𝐻) = (0g‘𝐻) | 
| 35 | 25, 34 | ghmid 19241 | . . . . . . . . 9
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) | 
| 36 | 35 | adantr 480 | . . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) | 
| 37 | 8 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → 𝑌 ∈ V) | 
| 38 | 4 | symgid 19420 | . . . . . . . . 9
⊢ (𝑌 ∈ V → ( I ↾
𝑌) =
(0g‘𝐻)) | 
| 39 | 37, 38 | syl 17 | . . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ( I ↾ 𝑌) = (0g‘𝐻)) | 
| 40 | 36, 39 | eqtr4d 2779 | . . . . . . 7
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (𝐹‘(0g‘𝐺)) = ( I ↾ 𝑌)) | 
| 41 | 40 | fveq1d 6907 | . . . . . 6
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ((𝐹‘(0g‘𝐺))‘𝑧) = (( I ↾ 𝑌)‘𝑧)) | 
| 42 |  | fvresi 7194 | . . . . . . 7
⊢ (𝑧 ∈ 𝑌 → (( I ↾ 𝑌)‘𝑧) = 𝑧) | 
| 43 | 42 | adantl 481 | . . . . . 6
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (( I ↾ 𝑌)‘𝑧) = 𝑧) | 
| 44 | 33, 41, 43 | 3eqtrd 2780 | . . . . 5
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = 𝑧) | 
| 45 | 11 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐹:𝑋⟶(Base‘𝐻)) | 
| 46 |  | simprr 772 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑣 ∈ 𝑋) | 
| 47 | 45, 46 | ffvelcdmd 7104 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑣) ∈ (Base‘𝐻)) | 
| 48 | 8 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑌 ∈ V) | 
| 49 | 4, 10 | elsymgbas 19392 | . . . . . . . . . . . 12
⊢ (𝑌 ∈ V → ((𝐹‘𝑣) ∈ (Base‘𝐻) ↔ (𝐹‘𝑣):𝑌–1-1-onto→𝑌)) | 
| 50 | 48, 49 | syl 17 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘𝑣) ∈ (Base‘𝐻) ↔ (𝐹‘𝑣):𝑌–1-1-onto→𝑌)) | 
| 51 | 47, 50 | mpbid 232 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑣):𝑌–1-1-onto→𝑌) | 
| 52 |  | f1of 6847 | . . . . . . . . . 10
⊢ ((𝐹‘𝑣):𝑌–1-1-onto→𝑌 → (𝐹‘𝑣):𝑌⟶𝑌) | 
| 53 | 51, 52 | syl 17 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑣):𝑌⟶𝑌) | 
| 54 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑧 ∈ 𝑌) | 
| 55 |  | fvco3 7007 | . . . . . . . . 9
⊢ (((𝐹‘𝑣):𝑌⟶𝑌 ∧ 𝑧 ∈ 𝑌) → (((𝐹‘𝑢) ∘ (𝐹‘𝑣))‘𝑧) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) | 
| 56 | 53, 54, 55 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (((𝐹‘𝑢) ∘ (𝐹‘𝑣))‘𝑧) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) | 
| 57 |  | simpll 766 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | 
| 58 |  | simprl 770 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑢 ∈ 𝑋) | 
| 59 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 60 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(+g‘𝐻) = (+g‘𝐻) | 
| 61 | 9, 59, 60 | ghmlin 19240 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝐹‘(𝑢(+g‘𝐺)𝑣)) = ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣))) | 
| 62 | 57, 58, 46, 61 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘(𝑢(+g‘𝐺)𝑣)) = ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣))) | 
| 63 | 45, 58 | ffvelcdmd 7104 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑢) ∈ (Base‘𝐻)) | 
| 64 | 4, 10, 60 | symgov 19402 | . . . . . . . . . . 11
⊢ (((𝐹‘𝑢) ∈ (Base‘𝐻) ∧ (𝐹‘𝑣) ∈ (Base‘𝐻)) → ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣)) = ((𝐹‘𝑢) ∘ (𝐹‘𝑣))) | 
| 65 | 63, 47, 64 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣)) = ((𝐹‘𝑢) ∘ (𝐹‘𝑣))) | 
| 66 | 62, 65 | eqtrd 2776 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘(𝑢(+g‘𝐺)𝑣)) = ((𝐹‘𝑢) ∘ (𝐹‘𝑣))) | 
| 67 | 66 | fveq1d 6907 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧) = (((𝐹‘𝑢) ∘ (𝐹‘𝑣))‘𝑧)) | 
| 68 | 53, 54 | ffvelcdmd 7104 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘𝑣)‘𝑧) ∈ 𝑌) | 
| 69 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝐹‘𝑥) = (𝐹‘𝑢)) | 
| 70 | 69 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝑥 = 𝑢 → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘𝑢)‘𝑦)) | 
| 71 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑦 = ((𝐹‘𝑣)‘𝑧) → ((𝐹‘𝑢)‘𝑦) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) | 
| 72 |  | fvex 6918 | . . . . . . . . . 10
⊢ ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧)) ∈ V | 
| 73 | 70, 71, 22, 72 | ovmpo 7594 | . . . . . . . . 9
⊢ ((𝑢 ∈ 𝑋 ∧ ((𝐹‘𝑣)‘𝑧) ∈ 𝑌) → (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧)) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) | 
| 74 | 58, 68, 73 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧)) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) | 
| 75 | 56, 67, 74 | 3eqtr4d 2786 | . . . . . . 7
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧) = (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧))) | 
| 76 | 1 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐺 ∈ Grp) | 
| 77 | 9, 59 | grpcl 18960 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋) | 
| 78 | 76, 58, 46, 77 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋) | 
| 79 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = (𝑢(+g‘𝐺)𝑣) → (𝐹‘𝑥) = (𝐹‘(𝑢(+g‘𝐺)𝑣))) | 
| 80 | 79 | fveq1d 6907 | . . . . . . . . 9
⊢ (𝑥 = (𝑢(+g‘𝐺)𝑣) → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑦)) | 
| 81 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑦) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧)) | 
| 82 |  | fvex 6918 | . . . . . . . . 9
⊢ ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧) ∈ V | 
| 83 | 80, 81, 22, 82 | ovmpo 7594 | . . . . . . . 8
⊢ (((𝑢(+g‘𝐺)𝑣) ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧)) | 
| 84 | 78, 54, 83 | syl2anc 584 | . . . . . . 7
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧)) | 
| 85 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣)) | 
| 86 | 85 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘𝑣)‘𝑦)) | 
| 87 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝐹‘𝑣)‘𝑦) = ((𝐹‘𝑣)‘𝑧)) | 
| 88 |  | fvex 6918 | . . . . . . . . . 10
⊢ ((𝐹‘𝑣)‘𝑧) ∈ V | 
| 89 | 86, 87, 22, 88 | ovmpo 7594 | . . . . . . . . 9
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → (𝑣 ⊕ 𝑧) = ((𝐹‘𝑣)‘𝑧)) | 
| 90 | 46, 54, 89 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑣 ⊕ 𝑧) = ((𝐹‘𝑣)‘𝑧)) | 
| 91 | 90 | oveq2d 7448 | . . . . . . 7
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢 ⊕ (𝑣 ⊕ 𝑧)) = (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧))) | 
| 92 | 75, 84, 91 | 3eqtr4d 2786 | . . . . . 6
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) | 
| 93 | 92 | ralrimivva 3201 | . . . . 5
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) | 
| 94 | 44, 93 | jca 511 | . . . 4
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))) | 
| 95 | 94 | ralrimiva 3145 | . . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ∀𝑧 ∈ 𝑌 (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))) | 
| 96 | 24, 95 | jca 511 | . 2
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑧 ∈ 𝑌 (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))))) | 
| 97 | 9, 59, 25 | isga 19310 | . 2
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑧 ∈ 𝑌 (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))))) | 
| 98 | 1, 8, 96, 97 | syl21anbrc 1344 | 1
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |