| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | n0i 4340 | . . . . . 6
⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅) | 
| 2 |  | mrsubccat.s | . . . . . . 7
⊢ 𝑆 = (mRSubst‘𝑇) | 
| 3 | 2 | rnfvprc 6900 | . . . . . 6
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) | 
| 4 | 1, 3 | nsyl2 141 | . . . . 5
⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V) | 
| 5 |  | eqid 2737 | . . . . . 6
⊢
(mVR‘𝑇) =
(mVR‘𝑇) | 
| 6 |  | mrsubccat.r | . . . . . 6
⊢ 𝑅 = (mREx‘𝑇) | 
| 7 | 5, 6, 2 | mrsubff 35517 | . . . . 5
⊢ (𝑇 ∈ V → 𝑆:(𝑅 ↑pm (mVR‘𝑇))⟶(𝑅 ↑m 𝑅)) | 
| 8 |  | ffun 6739 | . . . . 5
⊢ (𝑆:(𝑅 ↑pm (mVR‘𝑇))⟶(𝑅 ↑m 𝑅) → Fun 𝑆) | 
| 9 | 4, 7, 8 | 3syl 18 | . . . 4
⊢ (𝐹 ∈ ran 𝑆 → Fun 𝑆) | 
| 10 | 5, 6, 2 | mrsubrn 35518 | . . . . . 6
⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑m (mVR‘𝑇))) | 
| 11 | 10 | eleq2i 2833 | . . . . 5
⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ (𝑆 “ (𝑅 ↑m (mVR‘𝑇)))) | 
| 12 | 11 | biimpi 216 | . . . 4
⊢ (𝐹 ∈ ran 𝑆 → 𝐹 ∈ (𝑆 “ (𝑅 ↑m (mVR‘𝑇)))) | 
| 13 |  | fvelima 6974 | . . . 4
⊢ ((Fun
𝑆 ∧ 𝐹 ∈ (𝑆 “ (𝑅 ↑m (mVR‘𝑇)))) → ∃𝑓 ∈ (𝑅 ↑m (mVR‘𝑇))(𝑆‘𝑓) = 𝐹) | 
| 14 | 9, 12, 13 | syl2anc 584 | . . 3
⊢ (𝐹 ∈ ran 𝑆 → ∃𝑓 ∈ (𝑅 ↑m (mVR‘𝑇))(𝑆‘𝑓) = 𝐹) | 
| 15 |  | simprl 771 | . . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ 𝑅) | 
| 16 |  | elfvex 6944 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ (mREx‘𝑇) → 𝑇 ∈ V) | 
| 17 | 16, 6 | eleq2s 2859 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑅 → 𝑇 ∈ V) | 
| 18 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(mCN‘𝑇) =
(mCN‘𝑇) | 
| 19 | 18, 5, 6 | mrexval 35506 | . . . . . . . . . . . . 13
⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 20 | 15, 17, 19 | 3syl 18 | . . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 21 | 15, 20 | eleqtrd 2843 | . . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 22 |  | simprr 773 | . . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅) | 
| 23 | 22, 20 | eleqtrd 2843 | . . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 24 |  | elmapi 8889 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) → 𝑓:(mVR‘𝑇)⟶𝑅) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → 𝑓:(mVR‘𝑇)⟶𝑅) | 
| 26 | 25 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) → 𝑓:(mVR‘𝑇)⟶𝑅) | 
| 27 | 26 | ffvelcdmda 7104 | . . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → (𝑓‘𝑣) ∈ 𝑅) | 
| 28 | 20 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 29 | 27, 28 | eleqtrd 2843 | . . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → (𝑓‘𝑣) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 30 |  | simplr 769 | . . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ ¬ 𝑣 ∈ (mVR‘𝑇)) → 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 31 | 30 | s1cld 14641 | . . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ ¬ 𝑣 ∈ (mVR‘𝑇)) → 〈“𝑣”〉 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 32 | 29, 31 | ifclda 4561 | . . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) → if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 33 | 32 | fmpttd 7135 | . . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 34 |  | ccatco 14874 | . . . . . . . . . . 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 1373 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)) = (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) | 
| 36 | 35 | oveq2d 7447 | . . . . . . . . 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 6919 | . . . . . . . . . . . 12
⊢
(mCN‘𝑇) ∈
V | 
| 38 |  | fvex 6919 | . . . . . . . . . . . 12
⊢
(mVR‘𝑇) ∈
V | 
| 39 | 37, 38 | unex 7764 | . . . . . . . . . . 11
⊢
((mCN‘𝑇) ∪
(mVR‘𝑇)) ∈
V | 
| 40 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) = (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 41 | 40 | frmdmnd 18872 | . . . . . . . . . . 11
⊢
(((mCN‘𝑇)
∪ (mVR‘𝑇)) ∈
V → (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd) | 
| 42 | 39, 41 | mp1i 13 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd) | 
| 43 |  | wrdco 14870 | . . . . . . . . . . 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 584 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 45 |  | wrdco 14870 | . . . . . . . . . . 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 584 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 47 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) =
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) | 
| 48 | 40, 47 | frmdbas 18865 | . . . . . . . . . . . . 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 2746 | . . . . . . . . . . 11
⊢ Word
((mCN‘𝑇) ∪
(mVR‘𝑇)) =
(Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) | 
| 51 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) =
(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) | 
| 52 | 50, 51 | gsumccat 18854 | . . . . . . . . . 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 1373 | . . . . . . . . 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 18852 | . . . . . . . . . . 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 584 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 56 | 50 | gsumwcl 18852 | . . . . . . . . . . 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 584 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 58 | 40, 50, 51 | frmdadd 18868 | . . . . . . . . . 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 584 | . . . . . . . . 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 2781 | . . . . . . . 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 4007 | . . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (mVR‘𝑇) ⊆ (mVR‘𝑇)) | 
| 62 |  | ccatcl 14612 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → (𝑋 ++ 𝑌) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 63 | 21, 23, 62 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (𝑋 ++ 𝑌) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) | 
| 64 | 63, 20 | eleqtrrd 2844 | . . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (𝑋 ++ 𝑌) ∈ 𝑅) | 
| 65 | 18, 5, 6, 2, 40 | mrsubval 35514 | . . . . . . . . 9
⊢ ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ (𝑋 ++ 𝑌) ∈ 𝑅) → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)))) | 
| 66 | 25, 61, 64, 65 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ (𝑋 ++ 𝑌)))) | 
| 67 | 18, 5, 6, 2, 40 | mrsubval 35514 | . . . . . . . . . 10
⊢ ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ 𝑋 ∈ 𝑅) → ((𝑆‘𝑓)‘𝑋) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))) | 
| 68 | 25, 61, 15, 67 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘𝑋) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋))) | 
| 69 | 18, 5, 6, 2, 40 | mrsubval 35514 | . . . . . . . . . 10
⊢ ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ 𝑌 ∈ 𝑅) → ((𝑆‘𝑓)‘𝑌) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) | 
| 70 | 25, 61, 22, 69 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘𝑌) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌))) | 
| 71 | 68, 70 | oveq12d 7449 | . . . . . . . 8
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌)) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
((𝑣 ∈
((mCN‘𝑇) ∪
(mVR‘𝑇)) ↦
if(𝑣 ∈
(mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑌)))) | 
| 72 | 60, 66, 71 | 3eqtr4d 2787 | . . . . . . 7
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌))) | 
| 73 |  | fveq1 6905 | . . . . . . . 8
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = (𝐹‘(𝑋 ++ 𝑌))) | 
| 74 |  | fveq1 6905 | . . . . . . . . 9
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘𝑋) = (𝐹‘𝑋)) | 
| 75 |  | fveq1 6905 | . . . . . . . . 9
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘𝑌) = (𝐹‘𝑌)) | 
| 76 | 74, 75 | oveq12d 7449 | . . . . . . . 8
⊢ ((𝑆‘𝑓) = 𝐹 → (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))) | 
| 77 | 73, 76 | eqeq12d 2753 | . . . . . . 7
⊢ ((𝑆‘𝑓) = 𝐹 → (((𝑆‘𝑓)‘(𝑋 ++ 𝑌)) = (((𝑆‘𝑓)‘𝑋) ++ ((𝑆‘𝑓)‘𝑌)) ↔ (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) | 
| 78 | 72, 77 | syl5ibcom 245 | . . . . . 6
⊢ ((𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) ∧ (𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅)) → ((𝑆‘𝑓) = 𝐹 → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) | 
| 79 | 78 | ex 412 | . . . . 5
⊢ (𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → ((𝑆‘𝑓) = 𝐹 → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))))) | 
| 80 | 79 | com23 86 | . . . 4
⊢ (𝑓 ∈ (𝑅 ↑m (mVR‘𝑇)) → ((𝑆‘𝑓) = 𝐹 → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))))) | 
| 81 | 80 | rexlimiv 3148 | . . 3
⊢
(∃𝑓 ∈
(𝑅 ↑m
(mVR‘𝑇))(𝑆‘𝑓) = 𝐹 → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) | 
| 82 | 14, 81 | syl 17 | . 2
⊢ (𝐹 ∈ ran 𝑆 → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌)))) | 
| 83 | 82 | 3impib 1117 | 1
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹‘𝑋) ++ (𝐹‘𝑌))) |