Step | Hyp | Ref
| Expression |
1 | | n0i 3879 |
. . . . . 6
⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅) |
2 | | mrsubccat.s |
. . . . . . . . 9
⊢ 𝑆 = (mRSubst‘𝑇) |
3 | | fvprc 6097 |
. . . . . . . . 9
⊢ (¬
𝑇 ∈ V →
(mRSubst‘𝑇) =
∅) |
4 | 2, 3 | syl5eq 2656 |
. . . . . . . 8
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
5 | 4 | rneqd 5274 |
. . . . . . 7
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ran ∅) |
6 | | rn0 5298 |
. . . . . . 7
⊢ ran
∅ = ∅ |
7 | 5, 6 | syl6eq 2660 |
. . . . . 6
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
8 | 1, 7 | nsyl2 141 |
. . . . 5
⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V) |
9 | | eqid 2610 |
. . . . . 6
⊢
(mVR‘𝑇) =
(mVR‘𝑇) |
10 | | mrsubccat.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
11 | 9, 10, 2 | mrsubff 30663 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆:(𝑅 ↑pm (mVR‘𝑇))⟶(𝑅 ↑𝑚 𝑅)) |
12 | | ffun 5961 |
. . . . 5
⊢ (𝑆:(𝑅 ↑pm (mVR‘𝑇))⟶(𝑅 ↑𝑚 𝑅) → Fun 𝑆) |
13 | 8, 11, 12 | 3syl 18 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 → Fun 𝑆) |
14 | 9, 10, 2 | mrsubrn 30664 |
. . . . . 6
⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑𝑚 (mVR‘𝑇))) |
15 | 14 | eleq2i 2680 |
. . . . 5
⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ (𝑆 “ (𝑅 ↑𝑚 (mVR‘𝑇)))) |
16 | 15 | biimpi 205 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 → 𝐹 ∈ (𝑆 “ (𝑅 ↑𝑚 (mVR‘𝑇)))) |
17 | | fvelima 6158 |
. . . 4
⊢ ((Fun
𝑆 ∧ 𝐹 ∈ (𝑆 “ (𝑅 ↑𝑚 (mVR‘𝑇)))) → ∃𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇))(𝑆‘𝑓) = 𝐹) |
18 | 13, 16, 17 | syl2anc 691 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → ∃𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇))(𝑆‘𝑓) = 𝐹) |
19 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ 𝑅) |
20 | | elfvex 6131 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ (mREx‘𝑇) → 𝑇 ∈ V) |
21 | 20, 10 | eleq2s 2706 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑅 → 𝑇 ∈ V) |
22 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
23 | 22, 9, 10 | mrexval 30652 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
24 | 19, 21, 23 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
25 | 19, 24 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
26 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅) |
27 | 26, 24 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
28 | | elmapi 7765 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) → 𝑓:(mVR‘𝑇)⟶𝑅) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑓:(mVR‘𝑇)⟶𝑅) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) → 𝑓:(mVR‘𝑇)⟶𝑅) |
31 | 30 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → (𝑓‘𝑣) ∈ 𝑅) |
32 | 24 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
33 | 31, 32 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → (𝑓‘𝑣) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
34 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ ¬ 𝑣 ∈ (mVR‘𝑇)) → 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
35 | 34 | s1cld 13236 |
. . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ ¬ 𝑣 ∈ (mVR‘𝑇)) → 〈“𝑣”〉 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
36 | 33, 35 | ifclda 4070 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) → if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
37 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) = (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) |
38 | 36, 37 | fmptd 6292 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
39 | | ccatco 13432 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)) = (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) |
40 | 25, 27, 38, 39 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)) = (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) |
41 | 40 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌))) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
(((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
42 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(mCN‘𝑇) ∈
V |
43 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(mVR‘𝑇) ∈
V |
44 | 42, 43 | unex 6854 |
. . . . . . . . . . 11
⊢
((mCN‘𝑇) ∪
(mVR‘𝑇)) ∈
V |
45 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) = (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) |
46 | 45 | frmdmnd 17219 |
. . . . . . . . . . 11
⊢
(((mCN‘𝑇)
∪ (mVR‘𝑇)) ∈
V → (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd) |
47 | 44, 46 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd) |
48 | | wrdco 13428 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
49 | 25, 38, 48 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
50 | | wrdco 13428 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
51 | 27, 38, 50 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
52 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) =
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) |
53 | 45, 52 | frmdbas 17212 |
. . . . . . . . . . . . 13
⊢
(((mCN‘𝑇)
∪ (mVR‘𝑇)) ∈
V → (Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
54 | 44, 53 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) |
55 | 54 | eqcomi 2619 |
. . . . . . . . . . 11
⊢ Word
((mCN‘𝑇) ∪
(mVR‘𝑇)) =
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) |
56 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) =
(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) |
57 | 55, 56 | gsumccat 17201 |
. . . . . . . . . 10
⊢
(((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) →
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
58 | 47, 49, 51, 57 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
(((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
59 | 55 | gsumwcl 17200 |
. . . . . . . . . . 11
⊢
(((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) →
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
60 | 47, 49, 59 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
61 | 55 | gsumwcl 17200 |
. . . . . . . . . . 11
⊢
(((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) →
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
62 | 47, 51, 61 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
63 | 45, 55, 56 | frmdadd 17215 |
. . . . . . . . . 10
⊢
((((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) →
(((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
64 | 60, 62, 63 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
65 | 41, 58, 64 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
66 | | ssid 3587 |
. . . . . . . . . 10
⊢
(mVR‘𝑇)
⊆ (mVR‘𝑇) |
67 | 66 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (mVR‘𝑇) ⊆ (mVR‘𝑇)) |
68 | | ccatcl 13212 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → (𝑋 ++ 𝑌) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
69 | 25, 27, 68 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (𝑋 ++ 𝑌) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
70 | 69, 24 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (𝑋 ++ 𝑌) ∈ 𝑅) |
71 | 22, 9, 10, 2, 45 | mrsubval 30660 |
. . . . . . . . 9
⊢ ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ (𝑋 ++ 𝑌) ∈ 𝑅) → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)))) |
72 | 29, 67, 70, 71 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)))) |
73 | 22, 9, 10, 2, 45 | mrsubval 30660 |
. . . . . . . . . 10
⊢ ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ 𝑋 ∈ 𝑅) → ((𝑆‘𝑓)‘𝑋) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))) |
74 | 29, 67, 19, 73 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘𝑋) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))) |
75 | 22, 9, 10, 2, 45 | mrsubval 30660 |
. . . . . . . . . 10
⊢ ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ 𝑌 ∈ 𝑅) → ((𝑆‘𝑓)‘𝑌) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) |
76 | 29, 67, 26, 75 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘𝑌) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) |
77 | 74, 76 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌)) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
78 | 65, 72, 77 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌))) |
79 | | fveq1 6102 |
. . . . . . . 8
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = (𝐹‘(𝑋 ++ 𝑌))) |
80 | | fveq1 6102 |
. . . . . . . . 9
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘𝑋) = (𝐹‘𝑋)) |
81 | | fveq1 6102 |
. . . . . . . . 9
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘𝑌) = (𝐹‘𝑌)) |
82 | 80, 81 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑆‘𝑓) = 𝐹 → (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))) |
83 | 79, 82 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝑆‘𝑓) = 𝐹 → (((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌)) ↔ (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) |
84 | 78, 83 | syl5ibcom 234 |
. . . . . 6
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓) = 𝐹 → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) |
85 | 84 | ex 449 |
. . . . 5
⊢ (𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → ((𝑆‘𝑓) = 𝐹 → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))))) |
86 | 85 | com23 84 |
. . . 4
⊢ (𝑓 ∈ (𝑅 ↑𝑚 (mVR‘𝑇)) → ((𝑆‘𝑓) = 𝐹 → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))))) |
87 | 86 | rexlimiv 3009 |
. . 3
⊢
(∃𝑓 ∈
(𝑅
↑𝑚 (mVR‘𝑇))(𝑆‘𝑓) = 𝐹 → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) |
88 | 18, 87 | syl 17 |
. 2
⊢ (𝐹 ∈ ran 𝑆 → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) |
89 | 88 | 3impib 1254 |
1
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))) |