Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elmrsubrn Structured version   Visualization version   GIF version

Theorem elmrsubrn 32946
 Description: Characterization of the substitutions as functions from expressions to expressions that distribute under concatenation and map constants to themselves. (The constant part uses (𝐶 ∖ 𝑉) because we don't know that 𝐶 and 𝑉 are disjoint until we get to ismfs 32975.) (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mrsubccat.s 𝑆 = (mRSubst‘𝑇)
mrsubccat.r 𝑅 = (mREx‘𝑇)
mrsubcn.v 𝑉 = (mVR‘𝑇)
mrsubcn.c 𝐶 = (mCN‘𝑇)
Assertion
Ref Expression
elmrsubrn (𝑇𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))))
Distinct variable groups:   𝑥,𝑐,𝑦,𝐶   𝑥,𝑅,𝑦   𝑆,𝑐,𝑥,𝑦   𝑥,𝑇,𝑦   𝐹,𝑐,𝑥,𝑦   𝑉,𝑐,𝑥,𝑦   𝑥,𝑊,𝑦
Allowed substitution hints:   𝑅(𝑐)   𝑇(𝑐)   𝑊(𝑐)

Proof of Theorem elmrsubrn
Dummy variables 𝑟 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mrsubccat.s . . . 4 𝑆 = (mRSubst‘𝑇)
2 mrsubccat.r . . . 4 𝑅 = (mREx‘𝑇)
31, 2mrsubf 32943 . . 3 (𝐹 ∈ ran 𝑆𝐹:𝑅𝑅)
4 mrsubcn.v . . . . 5 𝑉 = (mVR‘𝑇)
5 mrsubcn.c . . . . 5 𝐶 = (mCN‘𝑇)
61, 2, 4, 5mrsubcn 32945 . . . 4 ((𝐹 ∈ ran 𝑆𝑐 ∈ (𝐶𝑉)) → (𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
76ralrimiva 3149 . . 3 (𝐹 ∈ ran 𝑆 → ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
81, 2mrsubccat 32944 . . . . 5 ((𝐹 ∈ ran 𝑆𝑥𝑅𝑦𝑅) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))
983expb 1117 . . . 4 ((𝐹 ∈ ran 𝑆 ∧ (𝑥𝑅𝑦𝑅)) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))
109ralrimivva 3156 . . 3 (𝐹 ∈ ran 𝑆 → ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))
113, 7, 103jca 1125 . 2 (𝐹 ∈ ran 𝑆 → (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦))))
125, 4, 2mrexval 32927 . . . . . . 7 (𝑇𝑊𝑅 = Word (𝐶𝑉))
1312adantr 484 . . . . . 6 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → 𝑅 = Word (𝐶𝑉))
14 s1eq 13965 . . . . . . . . . . . . 13 (𝑤 = 𝑣 → ⟨“𝑤”⟩ = ⟨“𝑣”⟩)
1514fveq2d 6659 . . . . . . . . . . . 12 (𝑤 = 𝑣 → (𝐹‘⟨“𝑤”⟩) = (𝐹‘⟨“𝑣”⟩))
16 eqid 2798 . . . . . . . . . . . 12 (𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))
17 fvex 6668 . . . . . . . . . . . 12 (𝐹‘⟨“𝑣”⟩) ∈ V
1815, 16, 17fvmpt 6755 . . . . . . . . . . 11 (𝑣𝑉 → ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
1918adantl 485 . . . . . . . . . 10 ((((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) ∧ 𝑣𝑉) → ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
20 difun2 4390 . . . . . . . . . . . . . . 15 ((𝐶𝑉) ∖ 𝑉) = (𝐶𝑉)
2120eleq2i 2881 . . . . . . . . . . . . . 14 (𝑣 ∈ ((𝐶𝑉) ∖ 𝑉) ↔ 𝑣 ∈ (𝐶𝑉))
22 eldif 3893 . . . . . . . . . . . . . 14 (𝑣 ∈ ((𝐶𝑉) ∖ 𝑉) ↔ (𝑣 ∈ (𝐶𝑉) ∧ ¬ 𝑣𝑉))
2321, 22bitr3i 280 . . . . . . . . . . . . 13 (𝑣 ∈ (𝐶𝑉) ↔ (𝑣 ∈ (𝐶𝑉) ∧ ¬ 𝑣𝑉))
24 simpr2 1192 . . . . . . . . . . . . . 14 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
25 s1eq 13965 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑣 → ⟨“𝑐”⟩ = ⟨“𝑣”⟩)
2625fveq2d 6659 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑣 → (𝐹‘⟨“𝑐”⟩) = (𝐹‘⟨“𝑣”⟩))
2726, 25eqeq12d 2814 . . . . . . . . . . . . . . 15 (𝑐 = 𝑣 → ((𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ↔ (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩))
2827rspccva 3571 . . . . . . . . . . . . . 14 ((∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ 𝑣 ∈ (𝐶𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
2924, 28sylan 583 . . . . . . . . . . . . 13 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
3023, 29sylan2br 597 . . . . . . . . . . . 12 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ (𝑣 ∈ (𝐶𝑉) ∧ ¬ 𝑣𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
3130anassrs 471 . . . . . . . . . . 11 ((((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) ∧ ¬ 𝑣𝑉) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
3231eqcomd 2804 . . . . . . . . . 10 ((((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) ∧ ¬ 𝑣𝑉) → ⟨“𝑣”⟩ = (𝐹‘⟨“𝑣”⟩))
3319, 32ifeqda 4463 . . . . . . . . 9 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) → if(𝑣𝑉, ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩) = (𝐹‘⟨“𝑣”⟩))
3433mpteq2dva 5129 . . . . . . . 8 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝑉, ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) = (𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
3534coeq1d 5700 . . . . . . 7 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝑉, ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟) = ((𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))
3635oveq2d 7161 . . . . . 6 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → ((freeMnd‘(𝐶𝑉)) Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝑉, ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟)) = ((freeMnd‘(𝐶𝑉)) Σg ((𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟)))
3713, 36mpteq12dv 5119 . . . . 5 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝑟𝑅 ↦ ((freeMnd‘(𝐶𝑉)) Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝑉, ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))) = (𝑟 ∈ Word (𝐶𝑉) ↦ ((freeMnd‘(𝐶𝑉)) Σg ((𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
38 elun2 4107 . . . . . . . 8 (𝑣𝑉𝑣 ∈ (𝐶𝑉))
39 simplr1 1212 . . . . . . . . 9 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) → 𝐹:𝑅𝑅)
40 simpr 488 . . . . . . . . . . 11 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) → 𝑣 ∈ (𝐶𝑉))
4140s1cld 13968 . . . . . . . . . 10 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) → ⟨“𝑣”⟩ ∈ Word (𝐶𝑉))
4212ad2antrr 725 . . . . . . . . . 10 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) → 𝑅 = Word (𝐶𝑉))
4341, 42eleqtrrd 2893 . . . . . . . . 9 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) → ⟨“𝑣”⟩ ∈ 𝑅)
4439, 43ffvelrnd 6839 . . . . . . . 8 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
4538, 44sylan2 595 . . . . . . 7 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣𝑉) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
4615cbvmptv 5137 . . . . . . 7 (𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑣𝑉 ↦ (𝐹‘⟨“𝑣”⟩))
4745, 46fmptd 6865 . . . . . 6 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉𝑅)
48 ssid 3939 . . . . . 6 𝑉𝑉
49 eqid 2798 . . . . . . 7 (freeMnd‘(𝐶𝑉)) = (freeMnd‘(𝐶𝑉))
505, 4, 2, 1, 49mrsubfval 32934 . . . . . 6 (((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉𝑅𝑉𝑉) → (𝑆‘(𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟𝑅 ↦ ((freeMnd‘(𝐶𝑉)) Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝑉, ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
5147, 48, 50sylancl 589 . . . . 5 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝑆‘(𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟𝑅 ↦ ((freeMnd‘(𝐶𝑉)) Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝑉, ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
525fvexi 6669 . . . . . . . . 9 𝐶 ∈ V
534fvexi 6669 . . . . . . . . 9 𝑉 ∈ V
5452, 53unex 7462 . . . . . . . 8 (𝐶𝑉) ∈ V
5549frmdmnd 18036 . . . . . . . 8 ((𝐶𝑉) ∈ V → (freeMnd‘(𝐶𝑉)) ∈ Mnd)
5654, 55ax-mp 5 . . . . . . 7 (freeMnd‘(𝐶𝑉)) ∈ Mnd
5756a1i 11 . . . . . 6 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (freeMnd‘(𝐶𝑉)) ∈ Mnd)
5854a1i 11 . . . . . 6 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝐶𝑉) ∈ V)
5944, 42eleqtrd 2892 . . . . . . 7 (((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) ∧ 𝑣 ∈ (𝐶𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ Word (𝐶𝑉))
6059fmpttd 6866 . . . . . 6 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶𝑉)⟶Word (𝐶𝑉))
61 simpr1 1191 . . . . . . . 8 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → 𝐹:𝑅𝑅)
6213, 13feq23d 6490 . . . . . . . 8 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝐹:𝑅𝑅𝐹:Word (𝐶𝑉)⟶Word (𝐶𝑉)))
6361, 62mpbid 235 . . . . . . 7 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → 𝐹:Word (𝐶𝑉)⟶Word (𝐶𝑉))
64 simpr3 1193 . . . . . . . 8 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))
65 simprl 770 . . . . . . . . . . . . . . 15 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → 𝑥𝑅)
6612adantr 484 . . . . . . . . . . . . . . . 16 ((𝑇𝑊𝐹:𝑅𝑅) → 𝑅 = Word (𝐶𝑉))
6766adantr 484 . . . . . . . . . . . . . . 15 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → 𝑅 = Word (𝐶𝑉))
6865, 67eleqtrd 2892 . . . . . . . . . . . . . 14 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → 𝑥 ∈ Word (𝐶𝑉))
69 simprr 772 . . . . . . . . . . . . . . 15 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → 𝑦𝑅)
7069, 67eleqtrd 2892 . . . . . . . . . . . . . 14 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → 𝑦 ∈ Word (𝐶𝑉))
71 eqid 2798 . . . . . . . . . . . . . . . . . 18 (Base‘(freeMnd‘(𝐶𝑉))) = (Base‘(freeMnd‘(𝐶𝑉)))
7249, 71frmdbas 18029 . . . . . . . . . . . . . . . . 17 ((𝐶𝑉) ∈ V → (Base‘(freeMnd‘(𝐶𝑉))) = Word (𝐶𝑉))
7354, 72ax-mp 5 . . . . . . . . . . . . . . . 16 (Base‘(freeMnd‘(𝐶𝑉))) = Word (𝐶𝑉)
7473eqcomi 2807 . . . . . . . . . . . . . . 15 Word (𝐶𝑉) = (Base‘(freeMnd‘(𝐶𝑉)))
75 eqid 2798 . . . . . . . . . . . . . . 15 (+g‘(freeMnd‘(𝐶𝑉))) = (+g‘(freeMnd‘(𝐶𝑉)))
7649, 74, 75frmdadd 18032 . . . . . . . . . . . . . 14 ((𝑥 ∈ Word (𝐶𝑉) ∧ 𝑦 ∈ Word (𝐶𝑉)) → (𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦) = (𝑥 ++ 𝑦))
7768, 70, 76syl2anc 587 . . . . . . . . . . . . 13 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → (𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦) = (𝑥 ++ 𝑦))
7877fveq2d 6659 . . . . . . . . . . . 12 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = (𝐹‘(𝑥 ++ 𝑦)))
79 ffvelrn 6836 . . . . . . . . . . . . . . 15 ((𝐹:𝑅𝑅𝑥𝑅) → (𝐹𝑥) ∈ 𝑅)
8079ad2ant2lr 747 . . . . . . . . . . . . . 14 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → (𝐹𝑥) ∈ 𝑅)
8180, 67eleqtrd 2892 . . . . . . . . . . . . 13 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → (𝐹𝑥) ∈ Word (𝐶𝑉))
82 ffvelrn 6836 . . . . . . . . . . . . . . 15 ((𝐹:𝑅𝑅𝑦𝑅) → (𝐹𝑦) ∈ 𝑅)
8382ad2ant2l 745 . . . . . . . . . . . . . 14 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → (𝐹𝑦) ∈ 𝑅)
8483, 67eleqtrd 2892 . . . . . . . . . . . . 13 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → (𝐹𝑦) ∈ Word (𝐶𝑉))
8549, 74, 75frmdadd 18032 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ Word (𝐶𝑉) ∧ (𝐹𝑦) ∈ Word (𝐶𝑉)) → ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))
8681, 84, 85syl2anc 587 . . . . . . . . . . . 12 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))
8778, 86eqeq12d 2814 . . . . . . . . . . 11 (((𝑇𝑊𝐹:𝑅𝑅) ∧ (𝑥𝑅𝑦𝑅)) → ((𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦)) ↔ (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦))))
88872ralbidva 3163 . . . . . . . . . 10 ((𝑇𝑊𝐹:𝑅𝑅) → (∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦)) ↔ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦))))
8966raleqdv 3365 . . . . . . . . . . 11 ((𝑇𝑊𝐹:𝑅𝑅) → (∀𝑦𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦)) ↔ ∀𝑦 ∈ Word (𝐶𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦))))
9066, 89raleqbidv 3355 . . . . . . . . . 10 ((𝑇𝑊𝐹:𝑅𝑅) → (∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦)) ↔ ∀𝑥 ∈ Word (𝐶𝑉)∀𝑦 ∈ Word (𝐶𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦))))
9188, 90bitr3d 284 . . . . . . . . 9 ((𝑇𝑊𝐹:𝑅𝑅) → (∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)) ↔ ∀𝑥 ∈ Word (𝐶𝑉)∀𝑦 ∈ Word (𝐶𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦))))
92913ad2antr1 1185 . . . . . . . 8 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)) ↔ ∀𝑥 ∈ Word (𝐶𝑉)∀𝑦 ∈ Word (𝐶𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦))))
9364, 92mpbid 235 . . . . . . 7 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → ∀𝑥 ∈ Word (𝐶𝑉)∀𝑦 ∈ Word (𝐶𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦)))
94 wrd0 13902 . . . . . . . . . . . 12 ∅ ∈ Word (𝐶𝑉)
95 ffvelrn 6836 . . . . . . . . . . . 12 ((𝐹:Word (𝐶𝑉)⟶Word (𝐶𝑉) ∧ ∅ ∈ Word (𝐶𝑉)) → (𝐹‘∅) ∈ Word (𝐶𝑉))
9663, 94, 95sylancl 589 . . . . . . . . . . 11 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝐹‘∅) ∈ Word (𝐶𝑉))
97 lencl 13896 . . . . . . . . . . 11 ((𝐹‘∅) ∈ Word (𝐶𝑉) → (♯‘(𝐹‘∅)) ∈ ℕ0)
9896, 97syl 17 . . . . . . . . . 10 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℕ0)
9998nn0cnd 11965 . . . . . . . . 9 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℂ)
100 0cnd 10641 . . . . . . . . 9 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → 0 ∈ ℂ)
10199addid1d 10847 . . . . . . . . . 10 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → ((♯‘(𝐹‘∅)) + 0) = (♯‘(𝐹‘∅)))
10294, 13eleqtrrid 2897 . . . . . . . . . . . 12 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → ∅ ∈ 𝑅)
103 fvoveq1 7168 . . . . . . . . . . . . . 14 (𝑥 = ∅ → (𝐹‘(𝑥 ++ 𝑦)) = (𝐹‘(∅ ++ 𝑦)))
104 fveq2 6655 . . . . . . . . . . . . . . 15 (𝑥 = ∅ → (𝐹𝑥) = (𝐹‘∅))
105104oveq1d 7160 . . . . . . . . . . . . . 14 (𝑥 = ∅ → ((𝐹𝑥) ++ (𝐹𝑦)) = ((𝐹‘∅) ++ (𝐹𝑦)))
106103, 105eqeq12d 2814 . . . . . . . . . . . . 13 (𝑥 = ∅ → ((𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)) ↔ (𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹𝑦))))
107 oveq2 7153 . . . . . . . . . . . . . . . 16 (𝑦 = ∅ → (∅ ++ 𝑦) = (∅ ++ ∅))
108 ccatidid 13955 . . . . . . . . . . . . . . . 16 (∅ ++ ∅) = ∅
109107, 108eqtrdi 2849 . . . . . . . . . . . . . . 15 (𝑦 = ∅ → (∅ ++ 𝑦) = ∅)
110109fveq2d 6659 . . . . . . . . . . . . . 14 (𝑦 = ∅ → (𝐹‘(∅ ++ 𝑦)) = (𝐹‘∅))
111 fveq2 6655 . . . . . . . . . . . . . . 15 (𝑦 = ∅ → (𝐹𝑦) = (𝐹‘∅))
112111oveq2d 7161 . . . . . . . . . . . . . 14 (𝑦 = ∅ → ((𝐹‘∅) ++ (𝐹𝑦)) = ((𝐹‘∅) ++ (𝐹‘∅)))
113110, 112eqeq12d 2814 . . . . . . . . . . . . 13 (𝑦 = ∅ → ((𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹𝑦)) ↔ (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))))
114106, 113rspc2va 3583 . . . . . . . . . . . 12 (((∅ ∈ 𝑅 ∧ ∅ ∈ 𝑅) ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
115102, 102, 64, 114syl21anc 836 . . . . . . . . . . 11 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
116115fveq2d 6659 . . . . . . . . . 10 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (♯‘(𝐹‘∅)) = (♯‘((𝐹‘∅) ++ (𝐹‘∅))))
117 ccatlen 13938 . . . . . . . . . . 11 (((𝐹‘∅) ∈ Word (𝐶𝑉) ∧ (𝐹‘∅) ∈ Word (𝐶𝑉)) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
11896, 96, 117syl2anc 587 . . . . . . . . . 10 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
119101, 116, 1183eqtrrd 2838 . . . . . . . . 9 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))) = ((♯‘(𝐹‘∅)) + 0))
12099, 99, 100, 119addcanad 10852 . . . . . . . 8 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (♯‘(𝐹‘∅)) = 0)
121 fvex 6668 . . . . . . . . 9 (𝐹‘∅) ∈ V
122 hasheq0 13740 . . . . . . . . 9 ((𝐹‘∅) ∈ V → ((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) = ∅))
123121, 122ax-mp 5 . . . . . . . 8 ((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) = ∅)
124120, 123sylib 221 . . . . . . 7 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝐹‘∅) = ∅)
12556, 56pm3.2i 474 . . . . . . . 8 ((freeMnd‘(𝐶𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶𝑉)) ∈ Mnd)
12649frmd0 18037 . . . . . . . . 9 ∅ = (0g‘(freeMnd‘(𝐶𝑉)))
12774, 74, 75, 75, 126, 126ismhm 17970 . . . . . . . 8 (𝐹 ∈ ((freeMnd‘(𝐶𝑉)) MndHom (freeMnd‘(𝐶𝑉))) ↔ (((freeMnd‘(𝐶𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶𝑉)) ∈ Mnd) ∧ (𝐹:Word (𝐶𝑉)⟶Word (𝐶𝑉) ∧ ∀𝑥 ∈ Word (𝐶𝑉)∀𝑦 ∈ Word (𝐶𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦)) ∧ (𝐹‘∅) = ∅)))
128125, 127mpbiran 708 . . . . . . 7 (𝐹 ∈ ((freeMnd‘(𝐶𝑉)) MndHom (freeMnd‘(𝐶𝑉))) ↔ (𝐹:Word (𝐶𝑉)⟶Word (𝐶𝑉) ∧ ∀𝑥 ∈ Word (𝐶𝑉)∀𝑦 ∈ Word (𝐶𝑉)(𝐹‘(𝑥(+g‘(freeMnd‘(𝐶𝑉)))𝑦)) = ((𝐹𝑥)(+g‘(freeMnd‘(𝐶𝑉)))(𝐹𝑦)) ∧ (𝐹‘∅) = ∅))
12963, 93, 124, 128syl3anbrc 1340 . . . . . 6 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → 𝐹 ∈ ((freeMnd‘(𝐶𝑉)) MndHom (freeMnd‘(𝐶𝑉))))
130 eqid 2798 . . . . . . . . . 10 (varFMnd‘(𝐶𝑉)) = (varFMnd‘(𝐶𝑉))
131130vrmdf 18035 . . . . . . . . 9 ((𝐶𝑉) ∈ V → (varFMnd‘(𝐶𝑉)):(𝐶𝑉)⟶Word (𝐶𝑉))
13254, 131ax-mp 5 . . . . . . . 8 (varFMnd‘(𝐶𝑉)):(𝐶𝑉)⟶Word (𝐶𝑉)
133 fcompt 6882 . . . . . . . 8 ((𝐹:Word (𝐶𝑉)⟶Word (𝐶𝑉) ∧ (varFMnd‘(𝐶𝑉)):(𝐶𝑉)⟶Word (𝐶𝑉)) → (𝐹 ∘ (varFMnd‘(𝐶𝑉))) = (𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘((varFMnd‘(𝐶𝑉))‘𝑣))))
13463, 132, 133sylancl 589 . . . . . . 7 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝐹 ∘ (varFMnd‘(𝐶𝑉))) = (𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘((varFMnd‘(𝐶𝑉))‘𝑣))))
135130vrmdval 18034 . . . . . . . . . 10 (((𝐶𝑉) ∈ V ∧ 𝑣 ∈ (𝐶𝑉)) → ((varFMnd‘(𝐶𝑉))‘𝑣) = ⟨“𝑣”⟩)
13654, 135mpan 689 . . . . . . . . 9 (𝑣 ∈ (𝐶𝑉) → ((varFMnd‘(𝐶𝑉))‘𝑣) = ⟨“𝑣”⟩)
137136fveq2d 6659 . . . . . . . 8 (𝑣 ∈ (𝐶𝑉) → (𝐹‘((varFMnd‘(𝐶𝑉))‘𝑣)) = (𝐹‘⟨“𝑣”⟩))
138137mpteq2ia 5125 . . . . . . 7 (𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘((varFMnd‘(𝐶𝑉))‘𝑣))) = (𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩))
139134, 138eqtrdi 2849 . . . . . 6 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝐹 ∘ (varFMnd‘(𝐶𝑉))) = (𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
14049, 74, 130frmdup3lem 18043 . . . . . 6 ((((freeMnd‘(𝐶𝑉)) ∈ Mnd ∧ (𝐶𝑉) ∈ V ∧ (𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶𝑉)⟶Word (𝐶𝑉)) ∧ (𝐹 ∈ ((freeMnd‘(𝐶𝑉)) MndHom (freeMnd‘(𝐶𝑉))) ∧ (𝐹 ∘ (varFMnd‘(𝐶𝑉))) = (𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))) → 𝐹 = (𝑟 ∈ Word (𝐶𝑉) ↦ ((freeMnd‘(𝐶𝑉)) Σg ((𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
14157, 58, 60, 129, 139, 140syl32anc 1375 . . . . 5 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → 𝐹 = (𝑟 ∈ Word (𝐶𝑉) ↦ ((freeMnd‘(𝐶𝑉)) Σg ((𝑣 ∈ (𝐶𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
14237, 51, 1413eqtr4rd 2844 . . . 4 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → 𝐹 = (𝑆‘(𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))))
1434, 2, 1mrsubff 32938 . . . . . . 7 (𝑇𝑊𝑆:(𝑅pm 𝑉)⟶(𝑅m 𝑅))
144143ffnd 6496 . . . . . 6 (𝑇𝑊𝑆 Fn (𝑅pm 𝑉))
145144adantr 484 . . . . 5 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → 𝑆 Fn (𝑅pm 𝑉))
1462fvexi 6669 . . . . . . 7 𝑅 ∈ V
147 elpm2r 8425 . . . . . . 7 (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ ((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉𝑅𝑉𝑉)) → (𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅pm 𝑉))
148146, 53, 147mpanl12 701 . . . . . 6 (((𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉𝑅𝑉𝑉) → (𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅pm 𝑉))
14947, 48, 148sylancl 589 . . . . 5 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅pm 𝑉))
150 fnfvelrn 6835 . . . . 5 ((𝑆 Fn (𝑅pm 𝑉) ∧ (𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅pm 𝑉)) → (𝑆‘(𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
151145, 149, 150syl2anc 587 . . . 4 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → (𝑆‘(𝑤𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
152142, 151eqeltrd 2890 . . 3 ((𝑇𝑊 ∧ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))) → 𝐹 ∈ ran 𝑆)
153152ex 416 . 2 (𝑇𝑊 → ((𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦))) → 𝐹 ∈ ran 𝑆))
15411, 153impbid2 229 1 (𝑇𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅𝑅 ∧ ∀𝑐 ∈ (𝐶𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥𝑅𝑦𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹𝑥) ++ (𝐹𝑦)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3442   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  ∅c0 4246  ifcif 4428   ↦ cmpt 5114  ran crn 5524   ∘ ccom 5527   Fn wfn 6327  ⟶wf 6328  ‘cfv 6332  (class class class)co 7145   ↑m cmap 8407   ↑pm cpm 8408  0cc0 10544   + caddc 10547  ℕ0cn0 11903  ♯chash 13706  Word cword 13877   ++ cconcat 13933  ⟨“cs1 13960  Basecbs 16495  +gcplusg 16577   Σg cgsu 16726  Mndcmnd 17923   MndHom cmhm 17966  freeMndcfrmd 18024  varFMndcvrmd 18025  mCNcmcn 32886  mVRcmvar 32887  mRExcmrex 32892  mRSubstcmrsub 32896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-oadd 8107  df-er 8290  df-map 8409  df-pm 8410  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-card 9370  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-nn 11644  df-2 11706  df-n0 11904  df-xnn0 11976  df-z 11990  df-uz 12252  df-fz 12906  df-fzo 13049  df-seq 13385  df-hash 13707  df-word 13878  df-lsw 13926  df-concat 13934  df-s1 13961  df-substr 14014  df-pfx 14044  df-struct 16497  df-ndx 16498  df-slot 16499  df-base 16501  df-sets 16502  df-ress 16503  df-plusg 16590  df-0g 16727  df-gsum 16728  df-mgm 17864  df-sgrp 17913  df-mnd 17924  df-mhm 17968  df-submnd 17969  df-frmd 18026  df-vrmd 18027  df-mrex 32912  df-mrsub 32916 This theorem is referenced by:  mrsubco  32947
 Copyright terms: Public domain W3C validator