| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | coeq2 5868 | . . . . . . 7
⊢ (𝑥 = ∅ → (𝑈 ∘ 𝑥) = (𝑈 ∘ ∅)) | 
| 2 |  | co02 6279 | . . . . . . 7
⊢ (𝑈 ∘ ∅) =
∅ | 
| 3 | 1, 2 | eqtrdi 2792 | . . . . . 6
⊢ (𝑥 = ∅ → (𝑈 ∘ 𝑥) = ∅) | 
| 4 | 3 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = ∅ → (𝑀 Σg
(𝑈 ∘ 𝑥)) = (𝑀 Σg
∅)) | 
| 5 |  | id 22 | . . . . 5
⊢ (𝑥 = ∅ → 𝑥 = ∅) | 
| 6 | 4, 5 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = ∅ → ((𝑀 Σg
(𝑈 ∘ 𝑥)) = 𝑥 ↔ (𝑀 Σg ∅) =
∅)) | 
| 7 | 6 | imbi2d 340 | . . 3
⊢ (𝑥 = ∅ → ((𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ 𝑥)) = 𝑥) ↔ (𝐼 ∈ 𝑉 → (𝑀 Σg ∅) =
∅))) | 
| 8 |  | coeq2 5868 | . . . . . 6
⊢ (𝑥 = 𝑦 → (𝑈 ∘ 𝑥) = (𝑈 ∘ 𝑦)) | 
| 9 | 8 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝑀 Σg (𝑈 ∘ 𝑥)) = (𝑀 Σg (𝑈 ∘ 𝑦))) | 
| 10 |  | id 22 | . . . . 5
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) | 
| 11 | 9, 10 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝑀 Σg (𝑈 ∘ 𝑥)) = 𝑥 ↔ (𝑀 Σg (𝑈 ∘ 𝑦)) = 𝑦)) | 
| 12 | 11 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑦 → ((𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ 𝑥)) = 𝑥) ↔ (𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ 𝑦)) = 𝑦))) | 
| 13 |  | coeq2 5868 | . . . . . 6
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → (𝑈 ∘ 𝑥) = (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉))) | 
| 14 | 13 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → (𝑀 Σg (𝑈 ∘ 𝑥)) = (𝑀 Σg (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉)))) | 
| 15 |  | id 22 | . . . . 5
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → 𝑥 = (𝑦 ++ 〈“𝑧”〉)) | 
| 16 | 14, 15 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → ((𝑀 Σg (𝑈 ∘ 𝑥)) = 𝑥 ↔ (𝑀 Σg (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉))) = (𝑦 ++ 〈“𝑧”〉))) | 
| 17 | 16 | imbi2d 340 | . . 3
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → ((𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ 𝑥)) = 𝑥) ↔ (𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉))) = (𝑦 ++ 〈“𝑧”〉)))) | 
| 18 |  | coeq2 5868 | . . . . . 6
⊢ (𝑥 = 𝑊 → (𝑈 ∘ 𝑥) = (𝑈 ∘ 𝑊)) | 
| 19 | 18 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝑊 → (𝑀 Σg (𝑈 ∘ 𝑥)) = (𝑀 Σg (𝑈 ∘ 𝑊))) | 
| 20 |  | id 22 | . . . . 5
⊢ (𝑥 = 𝑊 → 𝑥 = 𝑊) | 
| 21 | 19, 20 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝑊 → ((𝑀 Σg (𝑈 ∘ 𝑥)) = 𝑥 ↔ (𝑀 Σg (𝑈 ∘ 𝑊)) = 𝑊)) | 
| 22 | 21 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑊 → ((𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ 𝑥)) = 𝑥) ↔ (𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ 𝑊)) = 𝑊))) | 
| 23 |  | frmdmnd.m | . . . . . 6
⊢ 𝑀 = (freeMnd‘𝐼) | 
| 24 | 23 | frmd0 18874 | . . . . 5
⊢ ∅ =
(0g‘𝑀) | 
| 25 | 24 | gsum0 18698 | . . . 4
⊢ (𝑀 Σg
∅) = ∅ | 
| 26 | 25 | a1i 11 | . . 3
⊢ (𝐼 ∈ 𝑉 → (𝑀 Σg ∅) =
∅) | 
| 27 |  | oveq1 7439 | . . . . . 6
⊢ ((𝑀 Σg
(𝑈 ∘ 𝑦)) = 𝑦 → ((𝑀 Σg (𝑈 ∘ 𝑦)) ++ 〈“𝑧”〉) = (𝑦 ++ 〈“𝑧”〉)) | 
| 28 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → 𝑦 ∈ Word 𝐼) | 
| 29 |  | simprr 772 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → 𝑧 ∈ 𝐼) | 
| 30 | 29 | s1cld 14642 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → 〈“𝑧”〉 ∈ Word 𝐼) | 
| 31 |  | frmdgsum.u | . . . . . . . . . . . . 13
⊢ 𝑈 =
(varFMnd‘𝐼) | 
| 32 | 31 | vrmdf 18872 | . . . . . . . . . . . 12
⊢ (𝐼 ∈ 𝑉 → 𝑈:𝐼⟶Word 𝐼) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → 𝑈:𝐼⟶Word 𝐼) | 
| 34 |  | ccatco 14875 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ Word 𝐼 ∧ 〈“𝑧”〉 ∈ Word 𝐼 ∧ 𝑈:𝐼⟶Word 𝐼) → (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉)) = ((𝑈 ∘ 𝑦) ++ (𝑈 ∘ 〈“𝑧”〉))) | 
| 35 | 28, 30, 33, 34 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉)) = ((𝑈 ∘ 𝑦) ++ (𝑈 ∘ 〈“𝑧”〉))) | 
| 36 |  | s1co 14873 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐼 ∧ 𝑈:𝐼⟶Word 𝐼) → (𝑈 ∘ 〈“𝑧”〉) = 〈“(𝑈‘𝑧)”〉) | 
| 37 | 29, 33, 36 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑈 ∘ 〈“𝑧”〉) = 〈“(𝑈‘𝑧)”〉) | 
| 38 | 31 | vrmdval 18871 | . . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐼) → (𝑈‘𝑧) = 〈“𝑧”〉) | 
| 39 | 38 | adantrl 716 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑈‘𝑧) = 〈“𝑧”〉) | 
| 40 | 39 | s1eqd 14640 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → 〈“(𝑈‘𝑧)”〉 =
〈“〈“𝑧”〉”〉) | 
| 41 | 37, 40 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑈 ∘ 〈“𝑧”〉) =
〈“〈“𝑧”〉”〉) | 
| 42 | 41 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → ((𝑈 ∘ 𝑦) ++ (𝑈 ∘ 〈“𝑧”〉)) = ((𝑈 ∘ 𝑦) ++ 〈“〈“𝑧”〉”〉)) | 
| 43 | 35, 42 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉)) = ((𝑈 ∘ 𝑦) ++ 〈“〈“𝑧”〉”〉)) | 
| 44 | 43 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑀 Σg (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉))) = (𝑀 Σg ((𝑈 ∘ 𝑦) ++ 〈“〈“𝑧”〉”〉))) | 
| 45 | 23 | frmdmnd 18873 | . . . . . . . . . . 11
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) | 
| 46 | 45 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → 𝑀 ∈ Mnd) | 
| 47 |  | wrdco 14871 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑈:𝐼⟶Word 𝐼) → (𝑈 ∘ 𝑦) ∈ Word Word 𝐼) | 
| 48 | 28, 33, 47 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑈 ∘ 𝑦) ∈ Word Word 𝐼) | 
| 49 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 50 | 23, 49 | frmdbas 18866 | . . . . . . . . . . . . 13
⊢ (𝐼 ∈ 𝑉 → (Base‘𝑀) = Word 𝐼) | 
| 51 | 50 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (Base‘𝑀) = Word 𝐼) | 
| 52 |  | wrdeq 14575 | . . . . . . . . . . . 12
⊢
((Base‘𝑀) =
Word 𝐼 → Word
(Base‘𝑀) = Word Word
𝐼) | 
| 53 | 51, 52 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → Word (Base‘𝑀) = Word Word 𝐼) | 
| 54 | 48, 53 | eleqtrrd 2843 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑈 ∘ 𝑦) ∈ Word (Base‘𝑀)) | 
| 55 | 30, 51 | eleqtrrd 2843 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → 〈“𝑧”〉 ∈ (Base‘𝑀)) | 
| 56 | 55 | s1cld 14642 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → 〈“〈“𝑧”〉”〉
∈ Word (Base‘𝑀)) | 
| 57 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(+g‘𝑀) = (+g‘𝑀) | 
| 58 | 49, 57 | gsumccat 18855 | . . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ (𝑈 ∘ 𝑦) ∈ Word (Base‘𝑀) ∧ 〈“〈“𝑧”〉”〉
∈ Word (Base‘𝑀))
→ (𝑀
Σg ((𝑈 ∘ 𝑦) ++ 〈“〈“𝑧”〉”〉)) =
((𝑀
Σg (𝑈 ∘ 𝑦))(+g‘𝑀)(𝑀 Σg
〈“〈“𝑧”〉”〉))) | 
| 59 | 46, 54, 56, 58 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑀 Σg ((𝑈 ∘ 𝑦) ++ 〈“〈“𝑧”〉”〉)) =
((𝑀
Σg (𝑈 ∘ 𝑦))(+g‘𝑀)(𝑀 Σg
〈“〈“𝑧”〉”〉))) | 
| 60 | 49 | gsumws1 18852 | . . . . . . . . . . . 12
⊢
(〈“𝑧”〉 ∈ (Base‘𝑀) → (𝑀 Σg
〈“〈“𝑧”〉”〉) =
〈“𝑧”〉) | 
| 61 | 55, 60 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑀 Σg
〈“〈“𝑧”〉”〉) =
〈“𝑧”〉) | 
| 62 | 61 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → ((𝑀 Σg (𝑈 ∘ 𝑦))(+g‘𝑀)(𝑀 Σg
〈“〈“𝑧”〉”〉)) = ((𝑀 Σg
(𝑈 ∘ 𝑦))(+g‘𝑀)〈“𝑧”〉)) | 
| 63 | 49 | gsumwcl 18853 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ Mnd ∧ (𝑈 ∘ 𝑦) ∈ Word (Base‘𝑀)) → (𝑀 Σg (𝑈 ∘ 𝑦)) ∈ (Base‘𝑀)) | 
| 64 | 46, 54, 63 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑀 Σg (𝑈 ∘ 𝑦)) ∈ (Base‘𝑀)) | 
| 65 | 23, 49, 57 | frmdadd 18869 | . . . . . . . . . . 11
⊢ (((𝑀 Σg
(𝑈 ∘ 𝑦)) ∈ (Base‘𝑀) ∧ 〈“𝑧”〉 ∈
(Base‘𝑀)) →
((𝑀
Σg (𝑈 ∘ 𝑦))(+g‘𝑀)〈“𝑧”〉) = ((𝑀 Σg (𝑈 ∘ 𝑦)) ++ 〈“𝑧”〉)) | 
| 66 | 64, 55, 65 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → ((𝑀 Σg (𝑈 ∘ 𝑦))(+g‘𝑀)〈“𝑧”〉) = ((𝑀 Σg (𝑈 ∘ 𝑦)) ++ 〈“𝑧”〉)) | 
| 67 | 62, 66 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → ((𝑀 Σg (𝑈 ∘ 𝑦))(+g‘𝑀)(𝑀 Σg
〈“〈“𝑧”〉”〉)) = ((𝑀 Σg
(𝑈 ∘ 𝑦)) ++ 〈“𝑧”〉)) | 
| 68 | 59, 67 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑀 Σg ((𝑈 ∘ 𝑦) ++ 〈“〈“𝑧”〉”〉)) =
((𝑀
Σg (𝑈 ∘ 𝑦)) ++ 〈“𝑧”〉)) | 
| 69 | 44, 68 | eqtrd 2776 | . . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → (𝑀 Σg (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉))) = ((𝑀 Σg (𝑈 ∘ 𝑦)) ++ 〈“𝑧”〉)) | 
| 70 | 69 | eqeq1d 2738 | . . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → ((𝑀 Σg (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉))) = (𝑦 ++ 〈“𝑧”〉) ↔ ((𝑀 Σg (𝑈 ∘ 𝑦)) ++ 〈“𝑧”〉) = (𝑦 ++ 〈“𝑧”〉))) | 
| 71 | 27, 70 | imbitrrid 246 | . . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼)) → ((𝑀 Σg (𝑈 ∘ 𝑦)) = 𝑦 → (𝑀 Σg (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉))) = (𝑦 ++ 〈“𝑧”〉))) | 
| 72 | 71 | expcom 413 | . . . 4
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝐼 ∈ 𝑉 → ((𝑀 Σg (𝑈 ∘ 𝑦)) = 𝑦 → (𝑀 Σg (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉))) = (𝑦 ++ 〈“𝑧”〉)))) | 
| 73 | 72 | a2d 29 | . . 3
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼) → ((𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ 𝑦)) = 𝑦) → (𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ (𝑦 ++ 〈“𝑧”〉))) = (𝑦 ++ 〈“𝑧”〉)))) | 
| 74 | 7, 12, 17, 22, 26, 73 | wrdind 14761 | . 2
⊢ (𝑊 ∈ Word 𝐼 → (𝐼 ∈ 𝑉 → (𝑀 Σg (𝑈 ∘ 𝑊)) = 𝑊)) | 
| 75 | 74 | impcom 407 | 1
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐼) → (𝑀 Σg (𝑈 ∘ 𝑊)) = 𝑊) |