Step | Hyp | Ref
| Expression |
1 | | mrsubccat.s |
. . . 4
⊢ 𝑆 = (mRSubst‘𝑇) |
2 | | mrsubccat.r |
. . . 4
⊢ 𝑅 = (mREx‘𝑇) |
3 | 1, 2 | mrsubf 31753 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅) |
4 | | mrsubcn.v |
. . . . 5
⊢ 𝑉 = (mVR‘𝑇) |
5 | | mrsubcn.c |
. . . . 5
⊢ 𝐶 = (mCN‘𝑇) |
6 | 1, 2, 4, 5 | mrsubcn 31755 |
. . . 4
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) |
7 | 6 | ralrimiva 3115 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) |
8 | 1, 2 | mrsubccat 31754 |
. . . . 5
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
9 | 8 | 3expb 1113 |
. . . 4
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
10 | 9 | ralrimivva 3120 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
11 | 3, 7, 10 | 3jca 1122 |
. 2
⊢ (𝐹 ∈ ran 𝑆 → (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) |
12 | 5, 4, 2 | mrexval 31737 |
. . . . . . 7
⊢ (𝑇 ∈ 𝑊 → 𝑅 = Word (𝐶 ∪ 𝑉)) |
13 | 12 | adantr 466 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
14 | | s1eq 13581 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑣 → 〈“𝑤”〉 = 〈“𝑣”〉) |
15 | 14 | fveq2d 6337 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑣 → (𝐹‘〈“𝑤”〉) = (𝐹‘〈“𝑣”〉)) |
16 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) = (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) |
17 | | fvex 6343 |
. . . . . . . . . . . 12
⊢ (𝐹‘〈“𝑣”〉) ∈
V |
18 | 15, 16, 17 | fvmpt 6425 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑉 → ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣) = (𝐹‘〈“𝑣”〉)) |
19 | 18 | adantl 467 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝑉) → ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣) = (𝐹‘〈“𝑣”〉)) |
20 | | difun2 4191 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∪ 𝑉) ∖ 𝑉) = (𝐶 ∖ 𝑉) |
21 | 20 | eleq2i 2842 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ 𝑣 ∈ (𝐶 ∖ 𝑉)) |
22 | | eldif 3734 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) |
23 | 21, 22 | bitr3i 266 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (𝐶 ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) |
24 | | simpr2 1235 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) |
25 | | s1eq 13581 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 𝑣 → 〈“𝑐”〉 = 〈“𝑣”〉) |
26 | 25 | fveq2d 6337 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑣 → (𝐹‘〈“𝑐”〉) = (𝐹‘〈“𝑣”〉)) |
27 | 26, 25 | eqeq12d 2786 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑣 → ((𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ↔ (𝐹‘〈“𝑣”〉) =
〈“𝑣”〉)) |
28 | 27 | rspccva 3460 |
. . . . . . . . . . . . . 14
⊢
((∀𝑐 ∈
(𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) |
29 | 24, 28 | sylan 563 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) |
30 | 23, 29 | sylan2br 576 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) |
31 | 30 | anassrs 458 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) |
32 | 31 | eqcomd 2777 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → 〈“𝑣”〉 = (𝐹‘〈“𝑣”〉)) |
33 | 19, 32 | ifeqda 4261 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉) = (𝐹‘〈“𝑣”〉)) |
34 | 33 | mpteq2dva 4879 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉))) |
35 | 34 | coeq1d 5423 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟) = ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)) |
36 | 35 | oveq2d 6810 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟)) = ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟))) |
37 | 13, 36 | mpteq12dv 4868 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟))) = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)))) |
38 | | elun2 3933 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝑉 → 𝑣 ∈ (𝐶 ∪ 𝑉)) |
39 | | simpr1 1233 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:𝑅⟶𝑅) |
40 | 39 | adantr 466 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝐹:𝑅⟶𝑅) |
41 | | simpr 471 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑣 ∈ (𝐶 ∪ 𝑉)) |
42 | 41 | s1cld 13584 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 〈“𝑣”〉 ∈ Word (𝐶 ∪ 𝑉)) |
43 | 12 | ad2antrr 699 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
44 | 42, 43 | eleqtrrd 2853 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 〈“𝑣”〉 ∈ 𝑅) |
45 | 40, 44 | ffvelrnd 6504 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘〈“𝑣”〉) ∈ 𝑅) |
46 | 38, 45 | sylan2 574 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘〈“𝑣”〉) ∈ 𝑅) |
47 | 15 | cbvmptv 4885 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) = (𝑣 ∈ 𝑉 ↦ (𝐹‘〈“𝑣”〉)) |
48 | 46, 47 | fmptd 6528 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅) |
49 | | ssid 3774 |
. . . . . 6
⊢ 𝑉 ⊆ 𝑉 |
50 | | eqid 2771 |
. . . . . . 7
⊢
(freeMnd‘(𝐶
∪ 𝑉)) =
(freeMnd‘(𝐶 ∪
𝑉)) |
51 | 5, 4, 2, 1, 50 | mrsubfval 31744 |
. . . . . 6
⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟)))) |
52 | 48, 49, 51 | sylancl 568 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟)))) |
53 | | fvex 6343 |
. . . . . . . . . 10
⊢
(mCN‘𝑇) ∈
V |
54 | 5, 53 | eqeltri 2846 |
. . . . . . . . 9
⊢ 𝐶 ∈ V |
55 | | fvex 6343 |
. . . . . . . . . 10
⊢
(mVR‘𝑇) ∈
V |
56 | 4, 55 | eqeltri 2846 |
. . . . . . . . 9
⊢ 𝑉 ∈ V |
57 | 54, 56 | unex 7104 |
. . . . . . . 8
⊢ (𝐶 ∪ 𝑉) ∈ V |
58 | 50 | frmdmnd 17605 |
. . . . . . . 8
⊢ ((𝐶 ∪ 𝑉) ∈ V → (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) |
59 | 57, 58 | ax-mp 5 |
. . . . . . 7
⊢
(freeMnd‘(𝐶
∪ 𝑉)) ∈
Mnd |
60 | 59 | a1i 11 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) |
61 | 57 | a1i 11 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐶 ∪ 𝑉) ∈ V) |
62 | 45, 43 | eleqtrd 2852 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘〈“𝑣”〉) ∈ Word (𝐶 ∪ 𝑉)) |
63 | | eqid 2771 |
. . . . . . 7
⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) |
64 | 62, 63 | fmptd 6528 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) |
65 | 13, 13 | feq23d 6181 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹:𝑅⟶𝑅 ↔ 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))) |
66 | 39, 65 | mpbid 222 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) |
67 | | simpr3 1237 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
68 | | simprl 748 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ 𝑅) |
69 | 12 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
70 | 69 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
71 | 68, 70 | eleqtrd 2852 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ Word (𝐶 ∪ 𝑉)) |
72 | | simprr 750 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ 𝑅) |
73 | 72, 70 | eleqtrd 2852 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ Word (𝐶 ∪ 𝑉)) |
74 | | eqid 2771 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) |
75 | 50, 74 | frmdbas 17598 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∪ 𝑉) ∈ V →
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉)) |
76 | 57, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉) |
77 | 76 | eqcomi 2780 |
. . . . . . . . . . . . . . 15
⊢ Word
(𝐶 ∪ 𝑉) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) |
78 | | eqid 2771 |
. . . . . . . . . . . . . . 15
⊢
(+g‘(freeMnd‘(𝐶 ∪ 𝑉))) =
(+g‘(freeMnd‘(𝐶 ∪ 𝑉))) |
79 | 50, 77, 78 | frmdadd 17601 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word (𝐶 ∪ 𝑉) ∧ 𝑦 ∈ Word (𝐶 ∪ 𝑉)) → (𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦)) |
80 | 71, 73, 79 | syl2anc 567 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦)) |
81 | 80 | fveq2d 6337 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = (𝐹‘(𝑥 ++ 𝑦))) |
82 | | ffvelrn 6501 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑥 ∈ 𝑅) → (𝐹‘𝑥) ∈ 𝑅) |
83 | 82 | ad2ant2lr 736 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ 𝑅) |
84 | 83, 70 | eleqtrd 2852 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉)) |
85 | | ffvelrn 6501 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘𝑦) ∈ 𝑅) |
86 | 85 | ad2ant2l 734 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ 𝑅) |
87 | 86, 70 | eleqtrd 2852 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) |
88 | 50, 77, 78 | frmdadd 17601 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) → ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
89 | 84, 87, 88 | syl2anc 567 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
90 | 81, 89 | eqeq12d 2786 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) |
91 | 90 | 2ralbidva 3137 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) |
92 | 69 | raleqdv 3293 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) |
93 | 69, 92 | raleqbidv 3301 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) |
94 | 91, 93 | bitr3d 270 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) |
95 | 94 | 3ad2antr1 1203 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) |
96 | 67, 95 | mpbid 222 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))) |
97 | | wrd0 13527 |
. . . . . . . . . . . 12
⊢ ∅
∈ Word (𝐶 ∪ 𝑉) |
98 | | ffvelrn 6501 |
. . . . . . . . . . . 12
⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∅ ∈ Word (𝐶 ∪ 𝑉)) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) |
99 | 66, 97, 98 | sylancl 568 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) |
100 | | lencl 13521 |
. . . . . . . . . . 11
⊢ ((𝐹‘∅) ∈ Word
(𝐶 ∪ 𝑉) → (♯‘(𝐹‘∅)) ∈
ℕ0) |
101 | 99, 100 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈
ℕ0) |
102 | 101 | nn0cnd 11556 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈
ℂ) |
103 | | 0cnd 10236 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 0 ∈
ℂ) |
104 | 102 | addid1d 10439 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + 0) =
(♯‘(𝐹‘∅))) |
105 | 97, 13 | syl5eleqr 2857 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∅ ∈ 𝑅) |
106 | | fvoveq1 6817 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → (𝐹‘(𝑥 ++ 𝑦)) = (𝐹‘(∅ ++ 𝑦))) |
107 | | fveq2 6333 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → (𝐹‘𝑥) = (𝐹‘∅)) |
108 | 107 | oveq1d 6809 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → ((𝐹‘𝑥) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦))) |
109 | 106, 108 | eqeq12d 2786 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → ((𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ (𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)))) |
110 | | oveq2 6802 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ∅ → (∅ ++
𝑦) = (∅ ++
∅)) |
111 | | ccatlid 13569 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∈ Word (𝐶 ∪ 𝑉) → (∅ ++ ∅) =
∅) |
112 | 97, 111 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (∅
++ ∅) = ∅ |
113 | 110, 112 | syl6eq 2821 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (∅ ++
𝑦) =
∅) |
114 | 113 | fveq2d 6337 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → (𝐹‘(∅ ++ 𝑦)) = (𝐹‘∅)) |
115 | | fveq2 6333 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (𝐹‘𝑦) = (𝐹‘∅)) |
116 | 115 | oveq2d 6810 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → ((𝐹‘∅) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘∅))) |
117 | 114, 116 | eqeq12d 2786 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → ((𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)) ↔ (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))) |
118 | 109, 117 | rspc2va 3474 |
. . . . . . . . . . . 12
⊢
(((∅ ∈ 𝑅
∧ ∅ ∈ 𝑅)
∧ ∀𝑥 ∈
𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))) |
119 | 105, 105,
67, 118 | syl21anc 1475 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))) |
120 | 119 | fveq2d 6337 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = (♯‘((𝐹‘∅) ++ (𝐹‘∅)))) |
121 | | ccatlen 13558 |
. . . . . . . . . . 11
⊢ (((𝐹‘∅) ∈ Word
(𝐶 ∪ 𝑉) ∧ (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) +
(♯‘(𝐹‘∅)))) |
122 | 99, 99, 121 | syl2anc 567 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) =
((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅)))) |
123 | 104, 120,
122 | 3eqtrrd 2810 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) +
(♯‘(𝐹‘∅))) = ((♯‘(𝐹‘∅)) +
0)) |
124 | 102, 102,
103, 123 | addcanad 10444 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = 0) |
125 | | fvex 6343 |
. . . . . . . . 9
⊢ (𝐹‘∅) ∈
V |
126 | | hasheq0 13357 |
. . . . . . . . 9
⊢ ((𝐹‘∅) ∈ V →
((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) =
∅)) |
127 | 125, 126 | ax-mp 5 |
. . . . . . . 8
⊢
((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) =
∅) |
128 | 124, 127 | sylib 208 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ∅) |
129 | 59, 59 | pm3.2i 447 |
. . . . . . . 8
⊢
((freeMnd‘(𝐶
∪ 𝑉)) ∈ Mnd ∧
(freeMnd‘(𝐶 ∪
𝑉)) ∈
Mnd) |
130 | 50 | frmd0 17606 |
. . . . . . . . 9
⊢ ∅ =
(0g‘(freeMnd‘(𝐶 ∪ 𝑉))) |
131 | 77, 77, 78, 78, 130, 130 | ismhm 17546 |
. . . . . . . 8
⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) ∧ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) =
∅))) |
132 | 129, 131 | mpbiran 682 |
. . . . . . 7
⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) = ∅)) |
133 | 66, 96, 128, 132 | syl3anbrc 1428 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉)))) |
134 | | eqid 2771 |
. . . . . . . . . 10
⊢
(varFMnd‘(𝐶 ∪ 𝑉)) = (varFMnd‘(𝐶 ∪ 𝑉)) |
135 | 134 | vrmdf 17604 |
. . . . . . . . 9
⊢ ((𝐶 ∪ 𝑉) ∈ V →
(varFMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) |
136 | 57, 135 | ax-mp 5 |
. . . . . . . 8
⊢
(varFMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) |
137 | | fcompt 6544 |
. . . . . . . 8
⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧
(varFMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) → (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣)))) |
138 | 66, 136, 137 | sylancl 568 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣)))) |
139 | 134 | vrmdval 17603 |
. . . . . . . . . 10
⊢ (((𝐶 ∪ 𝑉) ∈ V ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) →
((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣) = 〈“𝑣”〉) |
140 | 61, 139 | sylan 563 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) →
((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣) = 〈“𝑣”〉) |
141 | 140 | fveq2d 6337 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣)) = (𝐹‘〈“𝑣”〉)) |
142 | 141 | mpteq2dva 4879 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉))) |
143 | 138, 142 | eqtrd 2805 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉))) |
144 | 50, 77, 134 | frmdup3lem 17612 |
. . . . . 6
⊢
((((freeMnd‘(𝐶
∪ 𝑉)) ∈ Mnd ∧
(𝐶 ∪ 𝑉) ∈ V ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) ∧ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ∧ (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)))) |
145 | 60, 61, 64, 133, 143, 144 | syl32anc 1484 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)))) |
146 | 37, 52, 145 | 3eqtr4rd 2816 |
. . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)))) |
147 | 4, 2, 1 | mrsubff 31748 |
. . . . . . 7
⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅)) |
148 | | ffn 6186 |
. . . . . . 7
⊢ (𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
149 | 147, 148 | syl 17 |
. . . . . 6
⊢ (𝑇 ∈ 𝑊 → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
150 | 149 | adantr 466 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
151 | | fvex 6343 |
. . . . . . . 8
⊢
(mREx‘𝑇)
∈ V |
152 | 2, 151 | eqeltri 2846 |
. . . . . . 7
⊢ 𝑅 ∈ V |
153 | | elpm2r 8028 |
. . . . . . 7
⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉)) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) |
154 | 152, 56, 153 | mpanl12 676 |
. . . . . 6
⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) |
155 | 48, 49, 154 | sylancl 568 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) |
156 | | fnfvelrn 6500 |
. . . . 5
⊢ ((𝑆 Fn (𝑅 ↑pm 𝑉) ∧ (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) ∈ ran 𝑆) |
157 | 150, 155,
156 | syl2anc 567 |
. . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) ∈ ran 𝑆) |
158 | 146, 157 | eqeltrd 2850 |
. . 3
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ran 𝑆) |
159 | 158 | ex 397 |
. 2
⊢ (𝑇 ∈ 𝑊 → ((𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → 𝐹 ∈ ran 𝑆)) |
160 | 11, 159 | impbid2 216 |
1
⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))) |