| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mrsubccat.s | . . . 4
⊢ 𝑆 = (mRSubst‘𝑇) | 
| 2 |  | mrsubccat.r | . . . 4
⊢ 𝑅 = (mREx‘𝑇) | 
| 3 | 1, 2 | mrsubf 35523 | . . 3
⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅) | 
| 4 |  | mrsubcn.v | . . . . 5
⊢ 𝑉 = (mVR‘𝑇) | 
| 5 |  | mrsubcn.c | . . . . 5
⊢ 𝐶 = (mCN‘𝑇) | 
| 6 | 1, 2, 4, 5 | mrsubcn 35525 | . . . 4
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) | 
| 7 | 6 | ralrimiva 3145 | . . 3
⊢ (𝐹 ∈ ran 𝑆 → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) | 
| 8 | 1, 2 | mrsubccat 35524 | . . . . 5
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) | 
| 9 | 8 | 3expb 1120 | . . . 4
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) | 
| 10 | 9 | ralrimivva 3201 | . . 3
⊢ (𝐹 ∈ ran 𝑆 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) | 
| 11 | 3, 7, 10 | 3jca 1128 | . 2
⊢ (𝐹 ∈ ran 𝑆 → (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) | 
| 12 | 5, 4, 2 | mrexval 35507 | . . . . . . 7
⊢ (𝑇 ∈ 𝑊 → 𝑅 = Word (𝐶 ∪ 𝑉)) | 
| 13 | 12 | adantr 480 | . . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑅 = Word (𝐶 ∪ 𝑉)) | 
| 14 |  | s1eq 14639 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑣 → 〈“𝑤”〉 = 〈“𝑣”〉) | 
| 15 | 14 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑣 → (𝐹‘〈“𝑤”〉) = (𝐹‘〈“𝑣”〉)) | 
| 16 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) = (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) | 
| 17 |  | fvex 6918 | . . . . . . . . . . . 12
⊢ (𝐹‘〈“𝑣”〉) ∈
V | 
| 18 | 15, 16, 17 | fvmpt 7015 | . . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑉 → ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣) = (𝐹‘〈“𝑣”〉)) | 
| 19 | 18 | adantl 481 | . . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝑉) → ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣) = (𝐹‘〈“𝑣”〉)) | 
| 20 |  | difun2 4480 | . . . . . . . . . . . . . . 15
⊢ ((𝐶 ∪ 𝑉) ∖ 𝑉) = (𝐶 ∖ 𝑉) | 
| 21 | 20 | eleq2i 2832 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ 𝑣 ∈ (𝐶 ∖ 𝑉)) | 
| 22 |  | eldif 3960 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) | 
| 23 | 21, 22 | bitr3i 277 | . . . . . . . . . . . . 13
⊢ (𝑣 ∈ (𝐶 ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) | 
| 24 |  | simpr2 1195 | . . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) | 
| 25 |  | s1eq 14639 | . . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 𝑣 → 〈“𝑐”〉 = 〈“𝑣”〉) | 
| 26 | 25 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑣 → (𝐹‘〈“𝑐”〉) = (𝐹‘〈“𝑣”〉)) | 
| 27 | 26, 25 | eqeq12d 2752 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑣 → ((𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ↔ (𝐹‘〈“𝑣”〉) =
〈“𝑣”〉)) | 
| 28 | 27 | rspccva 3620 | . . . . . . . . . . . . . 14
⊢
((∀𝑐 ∈
(𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) | 
| 29 | 24, 28 | sylan 580 | . . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) | 
| 30 | 23, 29 | sylan2br 595 | . . . . . . . . . . . 12
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) | 
| 31 | 30 | anassrs 467 | . . . . . . . . . . 11
⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) | 
| 32 | 31 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → 〈“𝑣”〉 = (𝐹‘〈“𝑣”〉)) | 
| 33 | 19, 32 | ifeqda 4561 | . . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉) = (𝐹‘〈“𝑣”〉)) | 
| 34 | 33 | mpteq2dva 5241 | . . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉))) | 
| 35 | 34 | coeq1d 5871 | . . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟) = ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)) | 
| 36 | 35 | oveq2d 7448 | . . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟)) = ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟))) | 
| 37 | 13, 36 | mpteq12dv 5232 | . . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟))) = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)))) | 
| 38 |  | elun2 4182 | . . . . . . . 8
⊢ (𝑣 ∈ 𝑉 → 𝑣 ∈ (𝐶 ∪ 𝑉)) | 
| 39 |  | simplr1 1215 | . . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝐹:𝑅⟶𝑅) | 
| 40 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑣 ∈ (𝐶 ∪ 𝑉)) | 
| 41 | 40 | s1cld 14642 | . . . . . . . . . 10
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 〈“𝑣”〉 ∈ Word (𝐶 ∪ 𝑉)) | 
| 42 | 12 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑅 = Word (𝐶 ∪ 𝑉)) | 
| 43 | 41, 42 | eleqtrrd 2843 | . . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 〈“𝑣”〉 ∈ 𝑅) | 
| 44 | 39, 43 | ffvelcdmd 7104 | . . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘〈“𝑣”〉) ∈ 𝑅) | 
| 45 | 38, 44 | sylan2 593 | . . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘〈“𝑣”〉) ∈ 𝑅) | 
| 46 | 15 | cbvmptv 5254 | . . . . . . 7
⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) = (𝑣 ∈ 𝑉 ↦ (𝐹‘〈“𝑣”〉)) | 
| 47 | 45, 46 | fmptd 7133 | . . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅) | 
| 48 |  | ssid 4005 | . . . . . 6
⊢ 𝑉 ⊆ 𝑉 | 
| 49 |  | eqid 2736 | . . . . . . 7
⊢
(freeMnd‘(𝐶
∪ 𝑉)) =
(freeMnd‘(𝐶 ∪
𝑉)) | 
| 50 | 5, 4, 2, 1, 49 | mrsubfval 35514 | . . . . . 6
⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟)))) | 
| 51 | 47, 48, 50 | sylancl 586 | . . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟)))) | 
| 52 | 5 | fvexi 6919 | . . . . . . . . 9
⊢ 𝐶 ∈ V | 
| 53 | 4 | fvexi 6919 | . . . . . . . . 9
⊢ 𝑉 ∈ V | 
| 54 | 52, 53 | unex 7765 | . . . . . . . 8
⊢ (𝐶 ∪ 𝑉) ∈ V | 
| 55 | 49 | frmdmnd 18873 | . . . . . . . 8
⊢ ((𝐶 ∪ 𝑉) ∈ V → (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) | 
| 56 | 54, 55 | ax-mp 5 | . . . . . . 7
⊢
(freeMnd‘(𝐶
∪ 𝑉)) ∈
Mnd | 
| 57 | 56 | a1i 11 | . . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) | 
| 58 | 54 | a1i 11 | . . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐶 ∪ 𝑉) ∈ V) | 
| 59 | 44, 42 | eleqtrd 2842 | . . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘〈“𝑣”〉) ∈ Word (𝐶 ∪ 𝑉)) | 
| 60 | 59 | fmpttd 7134 | . . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) | 
| 61 |  | simpr1 1194 | . . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:𝑅⟶𝑅) | 
| 62 | 13, 13 | feq23d 6730 | . . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹:𝑅⟶𝑅 ↔ 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))) | 
| 63 | 61, 62 | mpbid 232 | . . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) | 
| 64 |  | simpr3 1196 | . . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) | 
| 65 |  | simprl 770 | . . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ 𝑅) | 
| 66 | 12 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → 𝑅 = Word (𝐶 ∪ 𝑉)) | 
| 67 | 66 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑅 = Word (𝐶 ∪ 𝑉)) | 
| 68 | 65, 67 | eleqtrd 2842 | . . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ Word (𝐶 ∪ 𝑉)) | 
| 69 |  | simprr 772 | . . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ 𝑅) | 
| 70 | 69, 67 | eleqtrd 2842 | . . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ Word (𝐶 ∪ 𝑉)) | 
| 71 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) | 
| 72 | 49, 71 | frmdbas 18866 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∪ 𝑉) ∈ V →
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉)) | 
| 73 | 54, 72 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉) | 
| 74 | 73 | eqcomi 2745 | . . . . . . . . . . . . . . 15
⊢ Word
(𝐶 ∪ 𝑉) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) | 
| 75 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(+g‘(freeMnd‘(𝐶 ∪ 𝑉))) =
(+g‘(freeMnd‘(𝐶 ∪ 𝑉))) | 
| 76 | 49, 74, 75 | frmdadd 18869 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word (𝐶 ∪ 𝑉) ∧ 𝑦 ∈ Word (𝐶 ∪ 𝑉)) → (𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦)) | 
| 77 | 68, 70, 76 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦)) | 
| 78 | 77 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = (𝐹‘(𝑥 ++ 𝑦))) | 
| 79 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑥 ∈ 𝑅) → (𝐹‘𝑥) ∈ 𝑅) | 
| 80 | 79 | ad2ant2lr 748 | . . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ 𝑅) | 
| 81 | 80, 67 | eleqtrd 2842 | . . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉)) | 
| 82 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘𝑦) ∈ 𝑅) | 
| 83 | 82 | ad2ant2l 746 | . . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ 𝑅) | 
| 84 | 83, 67 | eleqtrd 2842 | . . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) | 
| 85 | 49, 74, 75 | frmdadd 18869 | . . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) → ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) | 
| 86 | 81, 84, 85 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) | 
| 87 | 78, 86 | eqeq12d 2752 | . . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) | 
| 88 | 87 | 2ralbidva 3218 | . . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) | 
| 89 | 66 | raleqdv 3325 | . . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) | 
| 90 | 66, 89 | raleqbidv 3345 | . . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) | 
| 91 | 88, 90 | bitr3d 281 | . . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) | 
| 92 | 91 | 3ad2antr1 1188 | . . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) | 
| 93 | 64, 92 | mpbid 232 | . . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))) | 
| 94 |  | wrd0 14578 | . . . . . . . . . . . 12
⊢ ∅
∈ Word (𝐶 ∪ 𝑉) | 
| 95 |  | ffvelcdm 7100 | . . . . . . . . . . . 12
⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∅ ∈ Word (𝐶 ∪ 𝑉)) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) | 
| 96 | 63, 94, 95 | sylancl 586 | . . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) | 
| 97 |  | lencl 14572 | . . . . . . . . . . 11
⊢ ((𝐹‘∅) ∈ Word
(𝐶 ∪ 𝑉) → (♯‘(𝐹‘∅)) ∈
ℕ0) | 
| 98 | 96, 97 | syl 17 | . . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈
ℕ0) | 
| 99 | 98 | nn0cnd 12591 | . . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈
ℂ) | 
| 100 |  | 0cnd 11255 | . . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 0 ∈
ℂ) | 
| 101 | 99 | addridd 11462 | . . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + 0) =
(♯‘(𝐹‘∅))) | 
| 102 | 94, 13 | eleqtrrid 2847 | . . . . . . . . . . . 12
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∅ ∈ 𝑅) | 
| 103 |  | fvoveq1 7455 | . . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → (𝐹‘(𝑥 ++ 𝑦)) = (𝐹‘(∅ ++ 𝑦))) | 
| 104 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → (𝐹‘𝑥) = (𝐹‘∅)) | 
| 105 | 104 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → ((𝐹‘𝑥) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦))) | 
| 106 | 103, 105 | eqeq12d 2752 | . . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → ((𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ (𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)))) | 
| 107 |  | oveq2 7440 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = ∅ → (∅ ++
𝑦) = (∅ ++
∅)) | 
| 108 |  | ccatidid 14629 | . . . . . . . . . . . . . . . 16
⊢ (∅
++ ∅) = ∅ | 
| 109 | 107, 108 | eqtrdi 2792 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (∅ ++
𝑦) =
∅) | 
| 110 | 109 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → (𝐹‘(∅ ++ 𝑦)) = (𝐹‘∅)) | 
| 111 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (𝐹‘𝑦) = (𝐹‘∅)) | 
| 112 | 111 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → ((𝐹‘∅) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘∅))) | 
| 113 | 110, 112 | eqeq12d 2752 | . . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → ((𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)) ↔ (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))) | 
| 114 | 106, 113 | rspc2va 3633 | . . . . . . . . . . . 12
⊢
(((∅ ∈ 𝑅
∧ ∅ ∈ 𝑅)
∧ ∀𝑥 ∈
𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))) | 
| 115 | 102, 102,
64, 114 | syl21anc 837 | . . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))) | 
| 116 | 115 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = (♯‘((𝐹‘∅) ++ (𝐹‘∅)))) | 
| 117 |  | ccatlen 14614 | . . . . . . . . . . 11
⊢ (((𝐹‘∅) ∈ Word
(𝐶 ∪ 𝑉) ∧ (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) +
(♯‘(𝐹‘∅)))) | 
| 118 | 96, 96, 117 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) =
((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅)))) | 
| 119 | 101, 116,
118 | 3eqtrrd 2781 | . . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) +
(♯‘(𝐹‘∅))) = ((♯‘(𝐹‘∅)) +
0)) | 
| 120 | 99, 99, 100, 119 | addcanad 11467 | . . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = 0) | 
| 121 |  | fvex 6918 | . . . . . . . . 9
⊢ (𝐹‘∅) ∈
V | 
| 122 |  | hasheq0 14403 | . . . . . . . . 9
⊢ ((𝐹‘∅) ∈ V →
((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) =
∅)) | 
| 123 | 121, 122 | ax-mp 5 | . . . . . . . 8
⊢
((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) =
∅) | 
| 124 | 120, 123 | sylib 218 | . . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ∅) | 
| 125 | 56, 56 | pm3.2i 470 | . . . . . . . 8
⊢
((freeMnd‘(𝐶
∪ 𝑉)) ∈ Mnd ∧
(freeMnd‘(𝐶 ∪
𝑉)) ∈
Mnd) | 
| 126 | 49 | frmd0 18874 | . . . . . . . . 9
⊢ ∅ =
(0g‘(freeMnd‘(𝐶 ∪ 𝑉))) | 
| 127 | 74, 74, 75, 75, 126, 126 | ismhm 18799 | . . . . . . . 8
⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) ∧ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) =
∅))) | 
| 128 | 125, 127 | mpbiran 709 | . . . . . . 7
⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) = ∅)) | 
| 129 | 63, 93, 124, 128 | syl3anbrc 1343 | . . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉)))) | 
| 130 |  | eqid 2736 | . . . . . . . . . 10
⊢
(varFMnd‘(𝐶 ∪ 𝑉)) = (varFMnd‘(𝐶 ∪ 𝑉)) | 
| 131 | 130 | vrmdf 18872 | . . . . . . . . 9
⊢ ((𝐶 ∪ 𝑉) ∈ V →
(varFMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) | 
| 132 | 54, 131 | ax-mp 5 | . . . . . . . 8
⊢
(varFMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) | 
| 133 |  | fcompt 7152 | . . . . . . . 8
⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧
(varFMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) → (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣)))) | 
| 134 | 63, 132, 133 | sylancl 586 | . . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣)))) | 
| 135 | 130 | vrmdval 18871 | . . . . . . . . . 10
⊢ (((𝐶 ∪ 𝑉) ∈ V ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) →
((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣) = 〈“𝑣”〉) | 
| 136 | 54, 135 | mpan 690 | . . . . . . . . 9
⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) →
((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣) = 〈“𝑣”〉) | 
| 137 | 136 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) → (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣)) = (𝐹‘〈“𝑣”〉)) | 
| 138 | 137 | mpteq2ia 5244 | . . . . . . 7
⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) | 
| 139 | 134, 138 | eqtrdi 2792 | . . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉))) | 
| 140 | 49, 74, 130 | frmdup3lem 18880 | . . . . . 6
⊢
((((freeMnd‘(𝐶
∪ 𝑉)) ∈ Mnd ∧
(𝐶 ∪ 𝑉) ∈ V ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) ∧ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ∧ (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)))) | 
| 141 | 57, 58, 60, 129, 139, 140 | syl32anc 1379 | . . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)))) | 
| 142 | 37, 51, 141 | 3eqtr4rd 2787 | . . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)))) | 
| 143 | 4, 2, 1 | mrsubff 35518 | . . . . . . 7
⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅)) | 
| 144 | 143 | ffnd 6736 | . . . . . 6
⊢ (𝑇 ∈ 𝑊 → 𝑆 Fn (𝑅 ↑pm 𝑉)) | 
| 145 | 144 | adantr 480 | . . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑆 Fn (𝑅 ↑pm 𝑉)) | 
| 146 | 2 | fvexi 6919 | . . . . . . 7
⊢ 𝑅 ∈ V | 
| 147 |  | elpm2r 8886 | . . . . . . 7
⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉)) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) | 
| 148 | 146, 53, 147 | mpanl12 702 | . . . . . 6
⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) | 
| 149 | 47, 48, 148 | sylancl 586 | . . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) | 
| 150 |  | fnfvelrn 7099 | . . . . 5
⊢ ((𝑆 Fn (𝑅 ↑pm 𝑉) ∧ (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) ∈ ran 𝑆) | 
| 151 | 145, 149,
150 | syl2anc 584 | . . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) ∈ ran 𝑆) | 
| 152 | 142, 151 | eqeltrd 2840 | . . 3
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ran 𝑆) | 
| 153 | 152 | ex 412 | . 2
⊢ (𝑇 ∈ 𝑊 → ((𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → 𝐹 ∈ ran 𝑆)) | 
| 154 | 11, 153 | impbid2 226 | 1
⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))) |