| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frgpup.x | . 2
⊢ 𝑋 = (Base‘𝐺) | 
| 2 |  | frgpup.b | . 2
⊢ 𝐵 = (Base‘𝐻) | 
| 3 |  | eqid 2736 | . 2
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 4 |  | eqid 2736 | . 2
⊢
(+g‘𝐻) = (+g‘𝐻) | 
| 5 |  | frgpup.i | . . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 6 |  | frgpup.g | . . . 4
⊢ 𝐺 = (freeGrp‘𝐼) | 
| 7 | 6 | frgpgrp 19781 | . . 3
⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp) | 
| 8 | 5, 7 | syl 17 | . 2
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 9 |  | frgpup.h | . 2
⊢ (𝜑 → 𝐻 ∈ Grp) | 
| 10 |  | frgpup.n | . . 3
⊢ 𝑁 = (invg‘𝐻) | 
| 11 |  | frgpup.t | . . 3
⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) | 
| 12 |  | frgpup.a | . . 3
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) | 
| 13 |  | frgpup.w | . . 3
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) | 
| 14 |  | frgpup.r | . . 3
⊢  ∼ = (
~FG ‘𝐼) | 
| 15 |  | frgpup.e | . . 3
⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg
(𝑇 ∘ 𝑔))〉) | 
| 16 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupf 19792 | . 2
⊢ (𝜑 → 𝐸:𝑋⟶𝐵) | 
| 17 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(freeMnd‘(𝐼
× 2o)) = (freeMnd‘(𝐼 × 2o)) | 
| 18 | 6, 17, 14 | frgpval 19777 | . . . . . . . . . 10
⊢ (𝐼 ∈ 𝑉 → 𝐺 = ((freeMnd‘(𝐼 × 2o))
/s ∼ )) | 
| 19 | 5, 18 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐺 = ((freeMnd‘(𝐼 × 2o))
/s ∼ )) | 
| 20 |  | 2on 8521 | . . . . . . . . . . . . 13
⊢
2o ∈ On | 
| 21 |  | xpexg 7771 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 2o ∈ On) →
(𝐼 × 2o)
∈ V) | 
| 22 | 5, 20, 21 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 × 2o) ∈
V) | 
| 23 |  | wrdexg 14563 | . . . . . . . . . . . 12
⊢ ((𝐼 × 2o) ∈ V
→ Word (𝐼 ×
2o) ∈ V) | 
| 24 |  | fvi 6984 | . . . . . . . . . . . 12
⊢ (Word
(𝐼 × 2o)
∈ V → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 ×
2o)) | 
| 25 | 22, 23, 24 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → ( I ‘Word (𝐼 × 2o)) = Word
(𝐼 ×
2o)) | 
| 26 | 13, 25 | eqtrid 2788 | . . . . . . . . . 10
⊢ (𝜑 → 𝑊 = Word (𝐼 × 2o)) | 
| 27 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Base‘(freeMnd‘(𝐼 × 2o))) =
(Base‘(freeMnd‘(𝐼 × 2o))) | 
| 28 | 17, 27 | frmdbas 18866 | . . . . . . . . . . 11
⊢ ((𝐼 × 2o) ∈ V
→ (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 ×
2o)) | 
| 29 | 22, 28 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 →
(Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 ×
2o)) | 
| 30 | 26, 29 | eqtr4d 2779 | . . . . . . . . 9
⊢ (𝜑 → 𝑊 = (Base‘(freeMnd‘(𝐼 ×
2o)))) | 
| 31 | 14 | fvexi 6919 | . . . . . . . . . 10
⊢  ∼ ∈
V | 
| 32 | 31 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ∼ ∈
V) | 
| 33 |  | fvexd 6920 | . . . . . . . . 9
⊢ (𝜑 → (freeMnd‘(𝐼 × 2o)) ∈
V) | 
| 34 | 19, 30, 32, 33 | qusbas 17591 | . . . . . . . 8
⊢ (𝜑 → (𝑊 / ∼ ) =
(Base‘𝐺)) | 
| 35 | 1, 34 | eqtr4id 2795 | . . . . . . 7
⊢ (𝜑 → 𝑋 = (𝑊 / ∼ )) | 
| 36 |  | eqimss 4041 | . . . . . . 7
⊢ (𝑋 = (𝑊 / ∼ ) → 𝑋 ⊆ (𝑊 / ∼ )) | 
| 37 | 35, 36 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑋 ⊆ (𝑊 / ∼ )) | 
| 38 | 37 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → 𝑋 ⊆ (𝑊 / ∼ )) | 
| 39 | 38 | sselda 3982 | . . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋) → 𝑐 ∈ (𝑊 / ∼ )) | 
| 40 |  | eqid 2736 | . . . . 5
⊢ (𝑊 / ∼ ) = (𝑊 / ∼ ) | 
| 41 |  | oveq2 7440 | . . . . . . 7
⊢ ([𝑢] ∼ = 𝑐 → (𝑎(+g‘𝐺)[𝑢] ∼ ) = (𝑎(+g‘𝐺)𝑐)) | 
| 42 | 41 | fveq2d 6909 | . . . . . 6
⊢ ([𝑢] ∼ = 𝑐 → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = (𝐸‘(𝑎(+g‘𝐺)𝑐))) | 
| 43 |  | fveq2 6905 | . . . . . . 7
⊢ ([𝑢] ∼ = 𝑐 → (𝐸‘[𝑢] ∼ ) = (𝐸‘𝑐)) | 
| 44 | 43 | oveq2d 7448 | . . . . . 6
⊢ ([𝑢] ∼ = 𝑐 → ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) | 
| 45 | 42, 44 | eqeq12d 2752 | . . . . 5
⊢ ([𝑢] ∼ = 𝑐 → ((𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) ↔ (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐)))) | 
| 46 | 37 | sselda 3982 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑊 / ∼ )) | 
| 47 | 46 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑊 / ∼ )) | 
| 48 |  | fvoveq1 7455 | . . . . . . . . 9
⊢ ([𝑡] ∼ = 𝑎 → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼
))) | 
| 49 |  | fveq2 6905 | . . . . . . . . . 10
⊢ ([𝑡] ∼ = 𝑎 → (𝐸‘[𝑡] ∼ ) = (𝐸‘𝑎)) | 
| 50 | 49 | oveq1d 7447 | . . . . . . . . 9
⊢ ([𝑡] ∼ = 𝑎 → ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) | 
| 51 | 48, 50 | eqeq12d 2752 | . . . . . . . 8
⊢ ([𝑡] ∼ = 𝑎 → ((𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) ↔ (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
)))) | 
| 52 |  | fviss 6985 | . . . . . . . . . . . . . . . 16
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) | 
| 53 | 13, 52 | eqsstri 4029 | . . . . . . . . . . . . . . 15
⊢ 𝑊 ⊆ Word (𝐼 × 2o) | 
| 54 | 53 | sseli 3978 | . . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝑊 → 𝑡 ∈ Word (𝐼 × 2o)) | 
| 55 | 53 | sseli 3978 | . . . . . . . . . . . . . 14
⊢ (𝑢 ∈ 𝑊 → 𝑢 ∈ Word (𝐼 × 2o)) | 
| 56 |  | ccatcl 14613 | . . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Word (𝐼 × 2o) ∧ 𝑢 ∈ Word (𝐼 × 2o)) → (𝑡 ++ 𝑢) ∈ Word (𝐼 × 2o)) | 
| 57 | 54, 55, 56 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → (𝑡 ++ 𝑢) ∈ Word (𝐼 × 2o)) | 
| 58 | 13 | efgrcl 19734 | . . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) | 
| 59 | 58 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) | 
| 60 | 59 | simprd 495 | . . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → 𝑊 = Word (𝐼 × 2o)) | 
| 61 | 57, 60 | eleqtrrd 2843 | . . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → (𝑡 ++ 𝑢) ∈ 𝑊) | 
| 62 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 19793 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ++ 𝑢) ∈ 𝑊) → (𝐸‘[(𝑡 ++ 𝑢)] ∼ ) = (𝐻 Σg
(𝑇 ∘ (𝑡 ++ 𝑢)))) | 
| 63 | 61, 62 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[(𝑡 ++ 𝑢)] ∼ ) = (𝐻 Σg
(𝑇 ∘ (𝑡 ++ 𝑢)))) | 
| 64 | 54 | ad2antrl 728 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝑡 ∈ Word (𝐼 × 2o)) | 
| 65 | 55 | ad2antll 729 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝑢 ∈ Word (𝐼 × 2o)) | 
| 66 | 2, 10, 11, 9, 5, 12 | frgpuptf 19789 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇:(𝐼 × 2o)⟶𝐵) | 
| 67 | 66 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝑇:(𝐼 × 2o)⟶𝐵) | 
| 68 |  | ccatco 14875 | . . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word (𝐼 × 2o) ∧ 𝑢 ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (𝑡 ++ 𝑢)) = ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) | 
| 69 | 64, 65, 67, 68 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝑇 ∘ (𝑡 ++ 𝑢)) = ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) | 
| 70 | 69 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐻 Σg (𝑇 ∘ (𝑡 ++ 𝑢))) = (𝐻 Σg ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢)))) | 
| 71 | 9 | grpmndd 18965 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ∈ Mnd) | 
| 72 | 71 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝐻 ∈ Mnd) | 
| 73 |  | wrdco 14871 | . . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ 𝑡) ∈ Word 𝐵) | 
| 74 | 54, 66, 73 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑇 ∘ 𝑡) ∈ Word 𝐵) | 
| 75 | 74 | adantrr 717 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝑇 ∘ 𝑡) ∈ Word 𝐵) | 
| 76 |  | wrdco 14871 | . . . . . . . . . . . . 13
⊢ ((𝑢 ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ 𝑢) ∈ Word 𝐵) | 
| 77 | 65, 67, 76 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝑇 ∘ 𝑢) ∈ Word 𝐵) | 
| 78 | 2, 4 | gsumccat 18855 | . . . . . . . . . . . 12
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ 𝑡) ∈ Word 𝐵 ∧ (𝑇 ∘ 𝑢) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) = ((𝐻 Σg (𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) | 
| 79 | 72, 75, 77, 78 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐻 Σg ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) = ((𝐻 Σg (𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) | 
| 80 | 63, 70, 79 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[(𝑡 ++ 𝑢)] ∼ ) = ((𝐻 Σg
(𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) | 
| 81 | 13, 6, 14, 3 | frgpadd 19782 | . . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → ([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ ) = [(𝑡 ++ 𝑢)] ∼ ) | 
| 82 | 81 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → ([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ ) = [(𝑡 ++ 𝑢)] ∼ ) | 
| 83 | 82 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = (𝐸‘[(𝑡 ++ 𝑢)] ∼ )) | 
| 84 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 19793 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐸‘[𝑡] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑡))) | 
| 85 | 84 | adantrr 717 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[𝑡] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑡))) | 
| 86 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 19793 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑊) → (𝐸‘[𝑢] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑢))) | 
| 87 | 86 | adantrl 716 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[𝑢] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑢))) | 
| 88 | 85, 87 | oveq12d 7450 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) = ((𝐻 Σg
(𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) | 
| 89 | 80, 83, 88 | 3eqtr4d 2786 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) | 
| 90 | 89 | anass1rs 655 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑡 ∈ 𝑊) → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) | 
| 91 | 40, 51, 90 | ectocld 8825 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑎 ∈ (𝑊 / ∼ )) → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) | 
| 92 | 47, 91 | syldan 591 | . . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑎 ∈ 𝑋) → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) | 
| 93 | 92 | an32s 652 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑢 ∈ 𝑊) → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) | 
| 94 | 40, 45, 93 | ectocld 8825 | . . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑐 ∈ (𝑊 / ∼ )) → (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) | 
| 95 | 39, 94 | syldan 591 | . . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋) → (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) | 
| 96 | 95 | anasss 466 | . 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) | 
| 97 | 1, 2, 3, 4, 8, 9, 16, 96 | isghmd 19244 | 1
⊢ (𝜑 → 𝐸 ∈ (𝐺 GrpHom 𝐻)) |