Step | Hyp | Ref
| Expression |
1 | | mrsubccat.s |
. . . 4
⊢ 𝑆 = (mRSubst‘𝑇) |
2 | | mrsubccat.r |
. . . 4
⊢ 𝑅 = (mREx‘𝑇) |
3 | 1, 2 | mrsubf 31414 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅) |
4 | | mrsubcn.v |
. . . . 5
⊢ 𝑉 = (mVR‘𝑇) |
5 | | mrsubcn.c |
. . . . 5
⊢ 𝐶 = (mCN‘𝑇) |
6 | 1, 2, 4, 5 | mrsubcn 31416 |
. . . 4
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) |
7 | 6 | ralrimiva 2966 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) |
8 | 1, 2 | mrsubccat 31415 |
. . . . 5
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
9 | 8 | 3expb 1266 |
. . . 4
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
10 | 9 | ralrimivva 2971 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
11 | 3, 7, 10 | 3jca 1242 |
. 2
⊢ (𝐹 ∈ ran 𝑆 → (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) |
12 | 5, 4, 2 | mrexval 31398 |
. . . . . . 7
⊢ (𝑇 ∈ 𝑊 → 𝑅 = Word (𝐶 ∪ 𝑉)) |
13 | 12 | adantr 481 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
14 | | s1eq 13380 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑣 → 〈“𝑤”〉 = 〈“𝑣”〉) |
15 | 14 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑣 → (𝐹‘〈“𝑤”〉) = (𝐹‘〈“𝑣”〉)) |
16 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) = (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) |
17 | | fvex 6201 |
. . . . . . . . . . . 12
⊢ (𝐹‘〈“𝑣”〉) ∈
V |
18 | 15, 16, 17 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑉 → ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣) = (𝐹‘〈“𝑣”〉)) |
19 | 18 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝑉) → ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣) = (𝐹‘〈“𝑣”〉)) |
20 | | difun2 4048 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∪ 𝑉) ∖ 𝑉) = (𝐶 ∖ 𝑉) |
21 | 20 | eleq2i 2693 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ 𝑣 ∈ (𝐶 ∖ 𝑉)) |
22 | | eldif 3584 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) |
23 | 21, 22 | bitr3i 266 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (𝐶 ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) |
24 | | simpr2 1068 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) |
25 | | s1eq 13380 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 𝑣 → 〈“𝑐”〉 = 〈“𝑣”〉) |
26 | 25 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑣 → (𝐹‘〈“𝑐”〉) = (𝐹‘〈“𝑣”〉)) |
27 | 26, 25 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑣 → ((𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ↔ (𝐹‘〈“𝑣”〉) =
〈“𝑣”〉)) |
28 | 27 | rspccva 3308 |
. . . . . . . . . . . . . 14
⊢
((∀𝑐 ∈
(𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) |
29 | 24, 28 | sylan 488 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) |
30 | 23, 29 | sylan2br 493 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) |
31 | 30 | anassrs 680 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → (𝐹‘〈“𝑣”〉) = 〈“𝑣”〉) |
32 | 31 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → 〈“𝑣”〉 = (𝐹‘〈“𝑣”〉)) |
33 | 19, 32 | ifeqda 4121 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉) = (𝐹‘〈“𝑣”〉)) |
34 | 33 | mpteq2dva 4744 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉))) |
35 | 34 | coeq1d 5283 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟) = ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)) |
36 | 35 | oveq2d 6666 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟)) = ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟))) |
37 | 13, 36 | mpteq12dv 4733 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟))) = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)))) |
38 | | elun2 3781 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝑉 → 𝑣 ∈ (𝐶 ∪ 𝑉)) |
39 | | simpr1 1067 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:𝑅⟶𝑅) |
40 | 39 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝐹:𝑅⟶𝑅) |
41 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑣 ∈ (𝐶 ∪ 𝑉)) |
42 | 41 | s1cld 13383 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 〈“𝑣”〉 ∈ Word (𝐶 ∪ 𝑉)) |
43 | 12 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
44 | 42, 43 | eleqtrrd 2704 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 〈“𝑣”〉 ∈ 𝑅) |
45 | 40, 44 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘〈“𝑣”〉) ∈ 𝑅) |
46 | 38, 45 | sylan2 491 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘〈“𝑣”〉) ∈ 𝑅) |
47 | 15 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) = (𝑣 ∈ 𝑉 ↦ (𝐹‘〈“𝑣”〉)) |
48 | 46, 47 | fmptd 6385 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅) |
49 | | ssid 3624 |
. . . . . 6
⊢ 𝑉 ⊆ 𝑉 |
50 | | eqid 2622 |
. . . . . . 7
⊢
(freeMnd‘(𝐶
∪ 𝑉)) =
(freeMnd‘(𝐶 ∪
𝑉)) |
51 | 5, 4, 2, 1, 50 | mrsubfval 31405 |
. . . . . 6
⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟)))) |
52 | 48, 49, 51 | sylancl 694 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑟)))) |
53 | | fvex 6201 |
. . . . . . . . . 10
⊢
(mCN‘𝑇) ∈
V |
54 | 5, 53 | eqeltri 2697 |
. . . . . . . . 9
⊢ 𝐶 ∈ V |
55 | | fvex 6201 |
. . . . . . . . . 10
⊢
(mVR‘𝑇) ∈
V |
56 | 4, 55 | eqeltri 2697 |
. . . . . . . . 9
⊢ 𝑉 ∈ V |
57 | 54, 56 | unex 6956 |
. . . . . . . 8
⊢ (𝐶 ∪ 𝑉) ∈ V |
58 | 50 | frmdmnd 17396 |
. . . . . . . 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 2703 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘〈“𝑣”〉) ∈ Word (𝐶 ∪ 𝑉)) |
63 | | eqid 2622 |
. . . . . . 7
⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) |
64 | 62, 63 | fmptd 6385 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) |
65 | 13, 13 | feq23d 6040 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹:𝑅⟶𝑅 ↔ 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))) |
66 | 39, 65 | mpbid 222 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) |
67 | | simpr3 1069 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
68 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ 𝑅) |
69 | 12 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
71 | 68, 70 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ Word (𝐶 ∪ 𝑉)) |
72 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ 𝑅) |
73 | 72, 70 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ Word (𝐶 ∪ 𝑉)) |
74 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) |
75 | 50, 74 | frmdbas 17389 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∪ 𝑉) ∈ V →
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉)) |
76 | 57, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉) |
77 | 76 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
⊢ Word
(𝐶 ∪ 𝑉) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) |
78 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(+g‘(freeMnd‘(𝐶 ∪ 𝑉))) =
(+g‘(freeMnd‘(𝐶 ∪ 𝑉))) |
79 | 50, 77, 78 | frmdadd 17392 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word (𝐶 ∪ 𝑉) ∧ 𝑦 ∈ Word (𝐶 ∪ 𝑉)) → (𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦)) |
80 | 71, 73, 79 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦)) |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = (𝐹‘(𝑥 ++ 𝑦))) |
82 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑥 ∈ 𝑅) → (𝐹‘𝑥) ∈ 𝑅) |
83 | 82 | ad2ant2lr 784 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ 𝑅) |
84 | 83, 70 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉)) |
85 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘𝑦) ∈ 𝑅) |
86 | 85 | ad2ant2l 782 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ 𝑅) |
87 | 86, 70 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) |
88 | 50, 77, 78 | frmdadd 17392 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) → ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
89 | 84, 87, 88 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) |
90 | 81, 89 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) |
91 | 90 | 2ralbidva 2988 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) |
92 | 69 | raleqdv 3144 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) |
93 | 69, 92 | raleqbidv 3152 |
. . . . . . . . . 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 1226 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))) |
96 | 67, 95 | mpbid 222 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))) |
97 | | wrd0 13330 |
. . . . . . . . . . . 12
⊢ ∅
∈ Word (𝐶 ∪ 𝑉) |
98 | | ffvelrn 6357 |
. . . . . . . . . . . 12
⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∅ ∈ Word (𝐶 ∪ 𝑉)) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) |
99 | 66, 97, 98 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) |
100 | | lencl 13324 |
. . . . . . . . . . 11
⊢ ((𝐹‘∅) ∈ Word
(𝐶 ∪ 𝑉) → (#‘(𝐹‘∅)) ∈
ℕ0) |
101 | 99, 100 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (#‘(𝐹‘∅)) ∈
ℕ0) |
102 | 101 | nn0cnd 11353 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (#‘(𝐹‘∅)) ∈
ℂ) |
103 | | 0cnd 10033 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 0 ∈
ℂ) |
104 | 102 | addid1d 10236 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((#‘(𝐹‘∅)) + 0) = (#‘(𝐹‘∅))) |
105 | 97, 13 | syl5eleqr 2708 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∅ ∈ 𝑅) |
106 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → (𝑥 ++ 𝑦) = (∅ ++ 𝑦)) |
107 | 106 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → (𝐹‘(𝑥 ++ 𝑦)) = (𝐹‘(∅ ++ 𝑦))) |
108 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → (𝐹‘𝑥) = (𝐹‘∅)) |
109 | 108 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → ((𝐹‘𝑥) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦))) |
110 | 107, 109 | eqeq12d 2637 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → ((𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ (𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)))) |
111 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ∅ → (∅ ++
𝑦) = (∅ ++
∅)) |
112 | | ccatlid 13369 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∈ Word (𝐶 ∪ 𝑉) → (∅ ++ ∅) =
∅) |
113 | 97, 112 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (∅
++ ∅) = ∅ |
114 | 111, 113 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (∅ ++
𝑦) =
∅) |
115 | 114 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → (𝐹‘(∅ ++ 𝑦)) = (𝐹‘∅)) |
116 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (𝐹‘𝑦) = (𝐹‘∅)) |
117 | 116 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → ((𝐹‘∅) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘∅))) |
118 | 115, 117 | eqeq12d 2637 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → ((𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)) ↔ (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))) |
119 | 110, 118 | rspc2va 3323 |
. . . . . . . . . . . 12
⊢
(((∅ ∈ 𝑅
∧ ∅ ∈ 𝑅)
∧ ∀𝑥 ∈
𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))) |
120 | 105, 105,
67, 119 | syl21anc 1325 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))) |
121 | 120 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (#‘(𝐹‘∅)) = (#‘((𝐹‘∅) ++ (𝐹‘∅)))) |
122 | | ccatlen 13360 |
. . . . . . . . . . 11
⊢ (((𝐹‘∅) ∈ Word
(𝐶 ∪ 𝑉) ∧ (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) → (#‘((𝐹‘∅) ++ (𝐹‘∅))) = ((#‘(𝐹‘∅)) +
(#‘(𝐹‘∅)))) |
123 | 99, 99, 122 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (#‘((𝐹‘∅) ++ (𝐹‘∅))) = ((#‘(𝐹‘∅)) +
(#‘(𝐹‘∅)))) |
124 | 104, 121,
123 | 3eqtrrd 2661 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((#‘(𝐹‘∅)) + (#‘(𝐹‘∅))) =
((#‘(𝐹‘∅)) + 0)) |
125 | 102, 102,
103, 124 | addcanad 10241 |
. . . . . . . 8
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (#‘(𝐹‘∅)) = 0) |
126 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝐹‘∅) ∈
V |
127 | | hasheq0 13154 |
. . . . . . . . 9
⊢ ((𝐹‘∅) ∈ V →
((#‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) =
∅)) |
128 | 126, 127 | ax-mp 5 |
. . . . . . . 8
⊢
((#‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) =
∅) |
129 | 125, 128 | sylib 208 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ∅) |
130 | 59, 59 | pm3.2i 471 |
. . . . . . . 8
⊢
((freeMnd‘(𝐶
∪ 𝑉)) ∈ Mnd ∧
(freeMnd‘(𝐶 ∪
𝑉)) ∈
Mnd) |
131 | 50 | frmd0 17397 |
. . . . . . . . 9
⊢ ∅ =
(0g‘(freeMnd‘(𝐶 ∪ 𝑉))) |
132 | 77, 77, 78, 78, 131, 131 | ismhm 17337 |
. . . . . . . 8
⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) ∧ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) =
∅))) |
133 | 130, 132 | mpbiran 953 |
. . . . . . 7
⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) = ∅)) |
134 | 66, 96, 129, 133 | syl3anbrc 1246 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉)))) |
135 | | eqid 2622 |
. . . . . . . . . 10
⊢
(varFMnd‘(𝐶 ∪ 𝑉)) = (varFMnd‘(𝐶 ∪ 𝑉)) |
136 | 135 | vrmdf 17395 |
. . . . . . . . 9
⊢ ((𝐶 ∪ 𝑉) ∈ V →
(varFMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) |
137 | 57, 136 | ax-mp 5 |
. . . . . . . 8
⊢
(varFMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) |
138 | | fcompt 6400 |
. . . . . . . 8
⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧
(varFMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) → (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣)))) |
139 | 66, 137, 138 | sylancl 694 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣)))) |
140 | 135 | vrmdval 17394 |
. . . . . . . . . 10
⊢ (((𝐶 ∪ 𝑉) ∈ V ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) →
((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣) = 〈“𝑣”〉) |
141 | 61, 140 | sylan 488 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) →
((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣) = 〈“𝑣”〉) |
142 | 141 | fveq2d 6195 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣)) = (𝐹‘〈“𝑣”〉)) |
143 | 142 | mpteq2dva 4744 |
. . . . . . 7
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((varFMnd‘(𝐶 ∪ 𝑉))‘𝑣))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉))) |
144 | 139, 143 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉))) |
145 | 50, 77, 135 | frmdup3lem 17403 |
. . . . . 6
⊢
((((freeMnd‘(𝐶
∪ 𝑉)) ∈ Mnd ∧
(𝐶 ∪ 𝑉) ∈ V ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) ∧ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ∧ (𝐹 ∘
(varFMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)))) |
146 | 60, 61, 64, 134, 144, 145 | syl32anc 1334 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘〈“𝑣”〉)) ∘ 𝑟)))) |
147 | 37, 52, 146 | 3eqtr4rd 2667 |
. . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)))) |
148 | 4, 2, 1 | mrsubff 31409 |
. . . . . . 7
⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅)) |
149 | | ffn 6045 |
. . . . . . 7
⊢ (𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
150 | 148, 149 | syl 17 |
. . . . . 6
⊢ (𝑇 ∈ 𝑊 → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
151 | 150 | adantr 481 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
152 | | fvex 6201 |
. . . . . . . 8
⊢
(mREx‘𝑇)
∈ V |
153 | 2, 152 | eqeltri 2697 |
. . . . . . 7
⊢ 𝑅 ∈ V |
154 | | elpm2r 7875 |
. . . . . . 7
⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ ((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉)) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) |
155 | 153, 56, 154 | mpanl12 718 |
. . . . . 6
⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) |
156 | 48, 49, 155 | sylancl 694 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) |
157 | | fnfvelrn 6356 |
. . . . 5
⊢ ((𝑆 Fn (𝑅 ↑pm 𝑉) ∧ (𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉)) ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) ∈ ran 𝑆) |
158 | 151, 156,
157 | syl2anc 693 |
. . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘〈“𝑤”〉))) ∈ ran 𝑆) |
159 | 147, 158 | eqeltrd 2701 |
. . 3
⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ran 𝑆) |
160 | 159 | ex 450 |
. 2
⊢ (𝑇 ∈ 𝑊 → ((𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → 𝐹 ∈ ran 𝑆)) |
161 | 11, 160 | impbid2 216 |
1
⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))) |