Step | Hyp | Ref
| Expression |
1 | | n0i 4220 |
. . . . . 6
⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅) |
2 | | mrsubccat.s |
. . . . . . 7
⊢ 𝑆 = (mRSubst‘𝑇) |
3 | 2 | rnfvprc 6662 |
. . . . . 6
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
4 | 1, 3 | nsyl2 143 |
. . . . 5
⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V) |
5 | | eqid 2738 |
. . . . . 6
⊢
(mVR‘𝑇) =
(mVR‘𝑇) |
6 | | mrsubccat.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
7 | 5, 6, 2 | mrsubff 33037 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆:(𝑅 ↑pm (mVR‘𝑇))⟶(𝑅 ↑m 𝑅)) |
8 | | ffun 6501 |
. . . . 5
⊢ (𝑆:(𝑅 ↑pm (mVR‘𝑇))⟶(𝑅 ↑m 𝑅) → Fun 𝑆) |
9 | 4, 7, 8 | 3syl 18 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 → Fun 𝑆) |
10 | 5, 6, 2 | mrsubrn 33038 |
. . . . . 6
⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑m (mVR‘𝑇))) |
11 | 10 | eleq2i 2824 |
. . . . 5
⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ (𝑆 “ (𝑅 ↑m (mVR‘𝑇)))) |
12 | 11 | biimpi 219 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 → 𝐹 ∈ (𝑆 “ (𝑅 ↑m (mVR‘𝑇)))) |
13 | | fvelima 6729 |
. . . 4
⊢ ((Fun
𝑆 ∧ 𝐹 ∈ (𝑆 “ (𝑅 ↑m (mVR‘𝑇)))) → ∃𝑓 ∈ (𝑅 ↑m (mVR‘𝑇))(𝑆‘𝑓) = 𝐹) |
14 | 9, 12, 13 | syl2anc 587 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → ∃𝑓 ∈ (𝑅 ↑m (mVR‘𝑇))(𝑆‘𝑓) = 𝐹) |
15 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ 𝑅) |
16 | | elfvex 6701 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ (mREx‘𝑇) → 𝑇 ∈ V) |
17 | 16, 6 | eleq2s 2851 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑅 → 𝑇 ∈ V) |
18 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
19 | 18, 5, 6 | mrexval 33026 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
20 | 15, 17, 19 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
21 | 15, 20 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
22 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅) |
23 | 22, 20 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
24 | | elmapi 8452 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) → 𝑓:(mVR‘𝑇)⟶𝑅) |
25 | 24 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑓:(mVR‘𝑇)⟶𝑅) |
26 | 25 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) → 𝑓:(mVR‘𝑇)⟶𝑅) |
27 | 26 | ffvelrnda 6855 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → (𝑓‘𝑣) ∈ 𝑅) |
28 | 20 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
29 | 27, 28 | eleqtrd 2835 |
. . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → (𝑓‘𝑣) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
30 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ ¬ 𝑣 ∈ (mVR‘𝑇)) → 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
31 | 30 | s1cld 14039 |
. . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ ¬ 𝑣 ∈ (mVR‘𝑇)) → 〈“𝑣”〉 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
32 | 29, 31 | ifclda 4446 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) → if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
33 | 32 | fmpttd 6883 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
34 | | ccatco 14279 |
. . . . . . . . . . 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‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) |
35 | 21, 23, 33, 34 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)) = (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) |
36 | 35 | oveq2d 7180 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌))) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
(((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
37 | | fvex 6681 |
. . . . . . . . . . . 12
⊢
(mCN‘𝑇) ∈
V |
38 | | fvex 6681 |
. . . . . . . . . . . 12
⊢
(mVR‘𝑇) ∈
V |
39 | 37, 38 | unex 7481 |
. . . . . . . . . . 11
⊢
((mCN‘𝑇) ∪
(mVR‘𝑇)) ∈
V |
40 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) = (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) |
41 | 40 | frmdmnd 18133 |
. . . . . . . . . . 11
⊢
(((mCN‘𝑇)
∪ (mVR‘𝑇)) ∈
V → (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd) |
42 | 39, 41 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd) |
43 | | wrdco 14275 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
44 | 21, 33, 43 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
45 | | wrdco 14275 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
46 | 23, 33, 45 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
47 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) =
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) |
48 | 40, 47 | frmdbas 18126 |
. . . . . . . . . . . . 13
⊢
(((mCN‘𝑇)
∪ (mVR‘𝑇)) ∈
V → (Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
49 | 39, 48 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) |
50 | 49 | eqcomi 2747 |
. . . . . . . . . . 11
⊢ Word
((mCN‘𝑇) ∪
(mVR‘𝑇)) =
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) |
51 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) =
(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) |
52 | 50, 51 | gsumccat 18115 |
. . . . . . . . . 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‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
53 | 42, 44, 46, 52 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (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‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
54 | 50 | gsumwcl 18112 |
. . . . . . . . . . 11
⊢
(((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) →
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
55 | 42, 44, 54 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
56 | 50 | gsumwcl 18112 |
. . . . . . . . . . 11
⊢
(((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) →
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
57 | 42, 46, 56 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
58 | 40, 50, 51 | frmdadd 18129 |
. . . . . . . . . 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‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
59 | 55, 57, 58 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (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‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
60 | 36, 53, 59 | 3eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 ↑m (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‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
61 | | ssidd 3898 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (mVR‘𝑇) ⊆ (mVR‘𝑇)) |
62 | | ccatcl 14008 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → (𝑋 ++ 𝑌) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
63 | 21, 23, 62 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (𝑋 ++ 𝑌) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
64 | 63, 20 | eleqtrrd 2836 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (𝑋 ++ 𝑌) ∈ 𝑅) |
65 | 18, 5, 6, 2, 40 | mrsubval 33034 |
. . . . . . . . 9
⊢ ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ (𝑋 ++ 𝑌) ∈ 𝑅) → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)))) |
66 | 25, 61, 64, 65 | syl3anc 1372 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)))) |
67 | 18, 5, 6, 2, 40 | mrsubval 33034 |
. . . . . . . . . 10
⊢ ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ 𝑋 ∈ 𝑅) → ((𝑆‘𝑓)‘𝑋) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))) |
68 | 25, 61, 15, 67 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘𝑋) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))) |
69 | 18, 5, 6, 2, 40 | mrsubval 33034 |
. . . . . . . . . 10
⊢ ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ 𝑌 ∈ 𝑅) → ((𝑆‘𝑓)‘𝑌) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) |
70 | 25, 61, 22, 69 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘𝑌) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) |
71 | 68, 70 | oveq12d 7182 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌)) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) |
72 | 60, 66, 71 | 3eqtr4d 2783 |
. . . . . . 7
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌))) |
73 | | fveq1 6667 |
. . . . . . . 8
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = (𝐹‘(𝑋 ++ 𝑌))) |
74 | | fveq1 6667 |
. . . . . . . . 9
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘𝑋) = (𝐹‘𝑋)) |
75 | | fveq1 6667 |
. . . . . . . . 9
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘𝑌) = (𝐹‘𝑌)) |
76 | 74, 75 | oveq12d 7182 |
. . . . . . . 8
⊢ ((𝑆‘𝑓) = 𝐹 → (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))) |
77 | 73, 76 | eqeq12d 2754 |
. . . . . . 7
⊢ ((𝑆‘𝑓) = 𝐹 → (((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌)) ↔ (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) |
78 | 72, 77 | syl5ibcom 248 |
. . . . . 6
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓) = 𝐹 → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) |
79 | 78 | ex 416 |
. . . . 5
⊢ (𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → ((𝑆‘𝑓) = 𝐹 → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))))) |
80 | 79 | com23 86 |
. . . 4
⊢ (𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) → ((𝑆‘𝑓) = 𝐹 → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))))) |
81 | 80 | rexlimiv 3189 |
. . 3
⊢
(∃𝑓 ∈
(𝑅 ↑m
(mVR‘𝑇))(𝑆‘𝑓) = 𝐹 → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) |
82 | 14, 81 | syl 17 |
. 2
⊢ (𝐹 ∈ ran 𝑆 → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) |
83 | 82 | 3impib 1117 |
1
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))) |