| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frmdup.i | . . 3
⊢ (𝜑 → 𝐼 ∈ 𝑋) | 
| 2 |  | frmdup.m | . . . 4
⊢ 𝑀 = (freeMnd‘𝐼) | 
| 3 | 2 | frmdmnd 18873 | . . 3
⊢ (𝐼 ∈ 𝑋 → 𝑀 ∈ Mnd) | 
| 4 | 1, 3 | syl 17 | . 2
⊢ (𝜑 → 𝑀 ∈ Mnd) | 
| 5 |  | frmdup.g | . 2
⊢ (𝜑 → 𝐺 ∈ Mnd) | 
| 6 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → 𝐺 ∈ Mnd) | 
| 7 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → 𝑥 ∈ Word 𝐼) | 
| 8 |  | frmdup.a | . . . . . . . 8
⊢ (𝜑 → 𝐴:𝐼⟶𝐵) | 
| 9 | 8 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → 𝐴:𝐼⟶𝐵) | 
| 10 |  | wrdco 14871 | . . . . . . 7
⊢ ((𝑥 ∈ Word 𝐼 ∧ 𝐴:𝐼⟶𝐵) → (𝐴 ∘ 𝑥) ∈ Word 𝐵) | 
| 11 | 7, 9, 10 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → (𝐴 ∘ 𝑥) ∈ Word 𝐵) | 
| 12 |  | frmdup.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝐺) | 
| 13 | 12 | gsumwcl 18853 | . . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝐴 ∘ 𝑥) ∈ Word 𝐵) → (𝐺 Σg (𝐴 ∘ 𝑥)) ∈ 𝐵) | 
| 14 | 6, 11, 13 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → (𝐺 Σg (𝐴 ∘ 𝑥)) ∈ 𝐵) | 
| 15 |  | frmdup.e | . . . . 5
⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥))) | 
| 16 | 14, 15 | fmptd 7133 | . . . 4
⊢ (𝜑 → 𝐸:Word 𝐼⟶𝐵) | 
| 17 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 18 | 2, 17 | frmdbas 18866 | . . . . . 6
⊢ (𝐼 ∈ 𝑋 → (Base‘𝑀) = Word 𝐼) | 
| 19 | 1, 18 | syl 17 | . . . . 5
⊢ (𝜑 → (Base‘𝑀) = Word 𝐼) | 
| 20 | 19 | feq2d 6721 | . . . 4
⊢ (𝜑 → (𝐸:(Base‘𝑀)⟶𝐵 ↔ 𝐸:Word 𝐼⟶𝐵)) | 
| 21 | 16, 20 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐸:(Base‘𝑀)⟶𝐵) | 
| 22 | 2, 17 | frmdelbas 18867 | . . . . . . . . 9
⊢ (𝑦 ∈ (Base‘𝑀) → 𝑦 ∈ Word 𝐼) | 
| 23 | 22 | ad2antrl 728 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑦 ∈ Word 𝐼) | 
| 24 | 2, 17 | frmdelbas 18867 | . . . . . . . . 9
⊢ (𝑧 ∈ (Base‘𝑀) → 𝑧 ∈ Word 𝐼) | 
| 25 | 24 | ad2antll 729 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑧 ∈ Word 𝐼) | 
| 26 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝐴:𝐼⟶𝐵) | 
| 27 |  | ccatco 14875 | . . . . . . . 8
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼 ∧ 𝐴:𝐼⟶𝐵) → (𝐴 ∘ (𝑦 ++ 𝑧)) = ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧))) | 
| 28 | 23, 25, 26, 27 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐴 ∘ (𝑦 ++ 𝑧)) = ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧))) | 
| 29 | 28 | oveq2d 7448 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧))) = (𝐺 Σg ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧)))) | 
| 30 | 5 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝐺 ∈ Mnd) | 
| 31 |  | wrdco 14871 | . . . . . . . 8
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝐴:𝐼⟶𝐵) → (𝐴 ∘ 𝑦) ∈ Word 𝐵) | 
| 32 | 23, 26, 31 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐴 ∘ 𝑦) ∈ Word 𝐵) | 
| 33 |  | wrdco 14871 | . . . . . . . 8
⊢ ((𝑧 ∈ Word 𝐼 ∧ 𝐴:𝐼⟶𝐵) → (𝐴 ∘ 𝑧) ∈ Word 𝐵) | 
| 34 | 25, 26, 33 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐴 ∘ 𝑧) ∈ Word 𝐵) | 
| 35 |  | eqid 2736 | . . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 36 | 12, 35 | gsumccat 18855 | . . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝐴 ∘ 𝑦) ∈ Word 𝐵 ∧ (𝐴 ∘ 𝑧) ∈ Word 𝐵) → (𝐺 Σg ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧))) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) | 
| 37 | 30, 32, 34, 36 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐺 Σg ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧))) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) | 
| 38 | 29, 37 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧))) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) | 
| 39 |  | eqid 2736 | . . . . . . . . 9
⊢
(+g‘𝑀) = (+g‘𝑀) | 
| 40 | 2, 17, 39 | frmdadd 18869 | . . . . . . . 8
⊢ ((𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀)) → (𝑦(+g‘𝑀)𝑧) = (𝑦 ++ 𝑧)) | 
| 41 | 40 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑦(+g‘𝑀)𝑧) = (𝑦 ++ 𝑧)) | 
| 42 | 41 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐸‘(𝑦(+g‘𝑀)𝑧)) = (𝐸‘(𝑦 ++ 𝑧))) | 
| 43 |  | ccatcl 14613 | . . . . . . . 8
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼) → (𝑦 ++ 𝑧) ∈ Word 𝐼) | 
| 44 | 23, 25, 43 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑦 ++ 𝑧) ∈ Word 𝐼) | 
| 45 |  | coeq2 5868 | . . . . . . . . 9
⊢ (𝑥 = (𝑦 ++ 𝑧) → (𝐴 ∘ 𝑥) = (𝐴 ∘ (𝑦 ++ 𝑧))) | 
| 46 | 45 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑥 = (𝑦 ++ 𝑧) → (𝐺 Σg (𝐴 ∘ 𝑥)) = (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧)))) | 
| 47 |  | ovex 7465 | . . . . . . . 8
⊢ (𝐺 Σg
(𝐴 ∘ 𝑥)) ∈ V | 
| 48 | 46, 15, 47 | fvmpt3i 7020 | . . . . . . 7
⊢ ((𝑦 ++ 𝑧) ∈ Word 𝐼 → (𝐸‘(𝑦 ++ 𝑧)) = (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧)))) | 
| 49 | 44, 48 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐸‘(𝑦 ++ 𝑧)) = (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧)))) | 
| 50 | 42, 49 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐸‘(𝑦(+g‘𝑀)𝑧)) = (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧)))) | 
| 51 |  | coeq2 5868 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐴 ∘ 𝑥) = (𝐴 ∘ 𝑦)) | 
| 52 | 51 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐴 ∘ 𝑥)) = (𝐺 Σg (𝐴 ∘ 𝑦))) | 
| 53 | 52, 15, 47 | fvmpt3i 7020 | . . . . . . 7
⊢ (𝑦 ∈ Word 𝐼 → (𝐸‘𝑦) = (𝐺 Σg (𝐴 ∘ 𝑦))) | 
| 54 |  | coeq2 5868 | . . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝐴 ∘ 𝑥) = (𝐴 ∘ 𝑧)) | 
| 55 | 54 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐺 Σg (𝐴 ∘ 𝑥)) = (𝐺 Σg (𝐴 ∘ 𝑧))) | 
| 56 | 55, 15, 47 | fvmpt3i 7020 | . . . . . . 7
⊢ (𝑧 ∈ Word 𝐼 → (𝐸‘𝑧) = (𝐺 Σg (𝐴 ∘ 𝑧))) | 
| 57 | 53, 56 | oveqan12d 7451 | . . . . . 6
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼) → ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧)) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) | 
| 58 | 23, 25, 57 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧)) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) | 
| 59 | 38, 50, 58 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐸‘(𝑦(+g‘𝑀)𝑧)) = ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧))) | 
| 60 | 59 | ralrimivva 3201 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ (Base‘𝑀)∀𝑧 ∈ (Base‘𝑀)(𝐸‘(𝑦(+g‘𝑀)𝑧)) = ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧))) | 
| 61 |  | wrd0 14578 | . . . 4
⊢ ∅
∈ Word 𝐼 | 
| 62 |  | coeq2 5868 | . . . . . . . 8
⊢ (𝑥 = ∅ → (𝐴 ∘ 𝑥) = (𝐴 ∘ ∅)) | 
| 63 |  | co02 6279 | . . . . . . . 8
⊢ (𝐴 ∘ ∅) =
∅ | 
| 64 | 62, 63 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑥 = ∅ → (𝐴 ∘ 𝑥) = ∅) | 
| 65 | 64 | oveq2d 7448 | . . . . . 6
⊢ (𝑥 = ∅ → (𝐺 Σg
(𝐴 ∘ 𝑥)) = (𝐺 Σg
∅)) | 
| 66 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 67 | 66 | gsum0 18698 | . . . . . 6
⊢ (𝐺 Σg
∅) = (0g‘𝐺) | 
| 68 | 65, 67 | eqtrdi 2792 | . . . . 5
⊢ (𝑥 = ∅ → (𝐺 Σg
(𝐴 ∘ 𝑥)) = (0g‘𝐺)) | 
| 69 | 68, 15, 47 | fvmpt3i 7020 | . . . 4
⊢ (∅
∈ Word 𝐼 → (𝐸‘∅) =
(0g‘𝐺)) | 
| 70 | 61, 69 | mp1i 13 | . . 3
⊢ (𝜑 → (𝐸‘∅) = (0g‘𝐺)) | 
| 71 | 21, 60, 70 | 3jca 1128 | . 2
⊢ (𝜑 → (𝐸:(Base‘𝑀)⟶𝐵 ∧ ∀𝑦 ∈ (Base‘𝑀)∀𝑧 ∈ (Base‘𝑀)(𝐸‘(𝑦(+g‘𝑀)𝑧)) = ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧)) ∧ (𝐸‘∅) = (0g‘𝐺))) | 
| 72 | 2 | frmd0 18874 | . . 3
⊢ ∅ =
(0g‘𝑀) | 
| 73 | 17, 12, 39, 35, 72, 66 | ismhm 18799 | . 2
⊢ (𝐸 ∈ (𝑀 MndHom 𝐺) ↔ ((𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd) ∧ (𝐸:(Base‘𝑀)⟶𝐵 ∧ ∀𝑦 ∈ (Base‘𝑀)∀𝑧 ∈ (Base‘𝑀)(𝐸‘(𝑦(+g‘𝑀)𝑧)) = ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧)) ∧ (𝐸‘∅) = (0g‘𝐺)))) | 
| 74 | 4, 5, 71, 73 | syl21anbrc 1344 | 1
⊢ (𝜑 → 𝐸 ∈ (𝑀 MndHom 𝐺)) |