Metamath Proof Explorer

Theorem elmrsubrn

Description: Characterization of the substitutions as functions from expressions to expressions that distribute under concatenation and map constants to themselves. (The constant part uses ( C \ V ) because we don't know that C and V are disjoint until we get to ismfs .) (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubccat.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
mrsubccat.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
mrsubcn.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
mrsubcn.c ⊢ 𝐶 = ( mCN ‘ 𝑇 )
Assertion elmrsubrn ( 𝑇 ∈ 𝑊 → ( 𝐹 ∈ ran 𝑆 ↔ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mrsubccat.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
2 mrsubccat.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
3 mrsubcn.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
4 mrsubcn.c ⊢ 𝐶 = ( mCN ‘ 𝑇 )
5 1 2 mrsubf ⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 : 𝑅 ⟶ 𝑅 )
6 1 2 3 4 mrsubcn ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ) → ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ )
7 6 ralrimiva ⊢ ( 𝐹 ∈ ran 𝑆 → ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ )
8 1 2 mrsubccat ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) )
9 8 3expb ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) )
10 9 ralrimivva ⊢ ( 𝐹 ∈ ran 𝑆 → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) )
11 5 7 10 3jca ⊢ ( 𝐹 ∈ ran 𝑆 → ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) )
12 4 3 2 mrexval ⊢ ( 𝑇 ∈ 𝑊 → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )
13 12 adantr ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )
14 s1eq ⊢ ( 𝑤 = 𝑣 → ⟨“ 𝑤 ”⟩ = ⟨“ 𝑣 ”⟩ )
15 14 fveq2d ⊢ ( 𝑤 = 𝑣 → ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) = ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) )
16 eqid ⊢ ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) = ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) )
17 fvex ⊢ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ∈ V
18 15 16 17 fvmpt ⊢ ( 𝑣 ∈ 𝑉 → ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ‘ 𝑣 ) = ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) )
19 18 adantl ⊢ ( ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ‘ 𝑣 ) = ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) )
20 difun2 ⊢ ( ( 𝐶 ∪ 𝑉 ) ∖ 𝑉 ) = ( 𝐶 ∖ 𝑉 )
21 20 eleq2i ⊢ ( 𝑣 ∈ ( ( 𝐶 ∪ 𝑉 ) ∖ 𝑉 ) ↔ 𝑣 ∈ ( 𝐶 ∖ 𝑉 ) )
22 eldif ⊢ ( 𝑣 ∈ ( ( 𝐶 ∪ 𝑉 ) ∖ 𝑉 ) ↔ ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ∧ ¬ 𝑣 ∈ 𝑉 ) )
23 21 22 bitr3i ⊢ ( 𝑣 ∈ ( 𝐶 ∖ 𝑉 ) ↔ ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ∧ ¬ 𝑣 ∈ 𝑉 ) )
24 simpr2 ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ )
25 s1eq ⊢ ( 𝑐 = 𝑣 → ⟨“ 𝑐 ”⟩ = ⟨“ 𝑣 ”⟩ )
26 25 fveq2d ⊢ ( 𝑐 = 𝑣 → ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) )
27 26 25 eqeq12d ⊢ ( 𝑐 = 𝑣 → ( ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ↔ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) = ⟨“ 𝑣 ”⟩ ) )
28 27 rspccva ⊢ ( ( ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ 𝑣 ∈ ( 𝐶 ∖ 𝑉 ) ) → ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) = ⟨“ 𝑣 ”⟩ )
29 24 28 sylan ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∖ 𝑉 ) ) → ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) = ⟨“ 𝑣 ”⟩ )
30 23 29 sylan2br ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ∧ ¬ 𝑣 ∈ 𝑉 ) ) → ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) = ⟨“ 𝑣 ”⟩ )
31 30 anassrs ⊢ ( ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ ¬ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) = ⟨“ 𝑣 ”⟩ )
32 31 eqcomd ⊢ ( ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ ¬ 𝑣 ∈ 𝑉 ) → ⟨“ 𝑣 ”⟩ = ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) )
33 19 32 ifeqda ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → if ( 𝑣 ∈ 𝑉 , ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) = ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) )
34 33 mpteq2dva ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) = ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) )
35 34 coeq1d ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) = ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) )
36 35 oveq2d ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) ) = ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) ) )
37 13 36 mpteq12dv ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑟 ∈ 𝑅 ↦ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) ) ) = ( 𝑟 ∈ Word ( 𝐶 ∪ 𝑉 ) ↦ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) ) ) )
38 elun2 ⊢ ( 𝑣 ∈ 𝑉 → 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) )
39 simplr1 ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → 𝐹 : 𝑅 ⟶ 𝑅 )
40 simpr ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) )
41 40 s1cld ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → ⟨“ 𝑣 ”⟩ ∈ Word ( 𝐶 ∪ 𝑉 ) )
42 12 ad2antrr ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )
43 41 42 eleqtrrd ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → ⟨“ 𝑣 ”⟩ ∈ 𝑅 )
44 39 43 ffvelrnd ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ∈ 𝑅 )
45 38 44 sylan2 ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ∈ 𝑅 )
46 15 cbvmptv ⊢ ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) = ( 𝑣 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) )
47 45 46 fmptd ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) : 𝑉 ⟶ 𝑅 )
48 ssid ⊢ 𝑉 ⊆ 𝑉
49 eqid ⊢ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) = ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) )
50 4 3 2 1 49 mrsubfval ⊢ ( ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ) → ( 𝑆 ‘ ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ) = ( 𝑟 ∈ 𝑅 ↦ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) ) ) )
51 47 48 50 sylancl ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑆 ‘ ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ) = ( 𝑟 ∈ 𝑅 ↦ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) ) ) )
52 4 fvexi ⊢ 𝐶 ∈ V
53 3 fvexi ⊢ 𝑉 ∈ V
54 52 53 unex ⊢ ( 𝐶 ∪ 𝑉 ) ∈ V
55 49 frmdmnd ⊢ ( ( 𝐶 ∪ 𝑉 ) ∈ V → ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ∈ Mnd )
56 54 55 ax-mp ⊢ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ∈ Mnd
57 56 a1i ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ∈ Mnd )
58 54 a1i ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝐶 ∪ 𝑉 ) ∈ V )
59 44 42 eleqtrd ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ∈ Word ( 𝐶 ∪ 𝑉 ) )
60 59 fmpttd ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) : ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) )
61 simpr1 ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 : 𝑅 ⟶ 𝑅 )
62 13 13 feq23d ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝐹 : 𝑅 ⟶ 𝑅 ↔ 𝐹 : Word ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) ) )
63 61 62 mpbid ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 : Word ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) )
64 simpr3 ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) )
65 simprl ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑅 )
66 12 adantr ⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )
67 66 adantr ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )
68 65 67 eleqtrd ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑥 ∈ Word ( 𝐶 ∪ 𝑉 ) )
69 simprr ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑅 )
70 69 67 eleqtrd ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑦 ∈ Word ( 𝐶 ∪ 𝑉 ) )
71 eqid ⊢ ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) )
72 49 71 frmdbas ⊢ ( ( 𝐶 ∪ 𝑉 ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = Word ( 𝐶 ∪ 𝑉 ) )
73 54 72 ax-mp ⊢ ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = Word ( 𝐶 ∪ 𝑉 )
74 73 eqcomi ⊢ Word ( 𝐶 ∪ 𝑉 ) = ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) )
75 eqid ⊢ ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) )
76 49 74 75 frmdadd ⊢ ( ( 𝑥 ∈ Word ( 𝐶 ∪ 𝑉 ) ∧ 𝑦 ∈ Word ( 𝐶 ∪ 𝑉 ) ) → ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) = ( 𝑥 ++ 𝑦 ) )
77 68 70 76 syl2anc ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) = ( 𝑥 ++ 𝑦 ) )
78 77 fveq2d ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) )
79 ffvelrn ⊢ ( ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ 𝑥 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑅 )
80 79 ad2ant2lr ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑅 )
81 80 67 eleqtrd ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ Word ( 𝐶 ∪ 𝑉 ) )
82 ffvelrn ⊢ ( ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑅 )
83 82 ad2ant2l ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑅 )
84 83 67 eleqtrd ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ Word ( 𝐶 ∪ 𝑉 ) )
85 49 74 75 frmdadd ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ Word ( 𝐶 ∪ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ Word ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) )
86 81 84 85 syl2anc ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) )
87 78 86 eqeq12d ⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) )
88 87 2ralbidva ⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) )
89 66 raleqdv ⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) → ( ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ Word ( 𝐶 ∪ 𝑉 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
90 66 89 raleqbidv ⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ Word ( 𝐶 ∪ 𝑉 ) ∀ 𝑦 ∈ Word ( 𝐶 ∪ 𝑉 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
91 88 90 bitr3d ⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝐹 : 𝑅 ⟶ 𝑅 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ Word ( 𝐶 ∪ 𝑉 ) ∀ 𝑦 ∈ Word ( 𝐶 ∪ 𝑉 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
92 91 3ad2antr1 ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ Word ( 𝐶 ∪ 𝑉 ) ∀ 𝑦 ∈ Word ( 𝐶 ∪ 𝑉 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
93 64 92 mpbid ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑥 ∈ Word ( 𝐶 ∪ 𝑉 ) ∀ 𝑦 ∈ Word ( 𝐶 ∪ 𝑉 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) )
94 wrd0 ⊢ ∅ ∈ Word ( 𝐶 ∪ 𝑉 )
95 ffvelrn ⊢ ( ( 𝐹 : Word ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) ∧ ∅ ∈ Word ( 𝐶 ∪ 𝑉 ) ) → ( 𝐹 ‘ ∅ ) ∈ Word ( 𝐶 ∪ 𝑉 ) )
96 63 94 95 sylancl ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝐹 ‘ ∅ ) ∈ Word ( 𝐶 ∪ 𝑉 ) )
97 lencl ⊢ ( ( 𝐹 ‘ ∅ ) ∈ Word ( 𝐶 ∪ 𝑉 ) → ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) ∈ ℕ0 )
98 96 97 syl ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) ∈ ℕ0 )
99 98 nn0cnd ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) ∈ ℂ )
100 0cnd ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → 0 ∈ ℂ )
101 99 addid1d ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) + 0 ) = ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) )
102 94 13 eleqtrrid ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ∅ ∈ 𝑅 )
103 fvoveq1 ⊢ ( 𝑥 = ∅ → ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( 𝐹 ‘ ( ∅ ++ 𝑦 ) ) )
104 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ∅ ) )
105 104 oveq1d ⊢ ( 𝑥 = ∅ → ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ 𝑦 ) ) )
106 103 105 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( ∅ ++ 𝑦 ) ) = ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ 𝑦 ) ) ) )
107 oveq2 ⊢ ( 𝑦 = ∅ → ( ∅ ++ 𝑦 ) = ( ∅ ++ ∅ ) )
108 ccatidid ⊢ ( ∅ ++ ∅ ) = ∅
109 107 108 eqtrdi ⊢ ( 𝑦 = ∅ → ( ∅ ++ 𝑦 ) = ∅ )
110 109 fveq2d ⊢ ( 𝑦 = ∅ → ( 𝐹 ‘ ( ∅ ++ 𝑦 ) ) = ( 𝐹 ‘ ∅ ) )
111 fveq2 ⊢ ( 𝑦 = ∅ → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ∅ ) )
112 111 oveq2d ⊢ ( 𝑦 = ∅ → ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ ∅ ) ) )
113 110 112 eqeq12d ⊢ ( 𝑦 = ∅ → ( ( 𝐹 ‘ ( ∅ ++ 𝑦 ) ) = ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ∅ ) = ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ ∅ ) ) ) )
114 106 113 rspc2va ⊢ ( ( ( ∅ ∈ 𝑅 ∧ ∅ ∈ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ∅ ) = ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ ∅ ) ) )
115 102 102 64 114 syl21anc ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝐹 ‘ ∅ ) = ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ ∅ ) ) )
116 115 fveq2d ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) = ( ♯ ‘ ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ ∅ ) ) ) )
117 ccatlen ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ Word ( 𝐶 ∪ 𝑉 ) ∧ ( 𝐹 ‘ ∅ ) ∈ Word ( 𝐶 ∪ 𝑉 ) ) → ( ♯ ‘ ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ ∅ ) ) ) = ( ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) + ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) ) )
118 96 96 117 syl2anc ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ♯ ‘ ( ( 𝐹 ‘ ∅ ) ++ ( 𝐹 ‘ ∅ ) ) ) = ( ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) + ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) ) )
119 101 116 118 3eqtrrd ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) + ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) ) = ( ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) + 0 ) )
120 99 99 100 119 addcanad ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) = 0 )
121 fvex ⊢ ( 𝐹 ‘ ∅ ) ∈ V
122 hasheq0 ⊢ ( ( 𝐹 ‘ ∅ ) ∈ V → ( ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) = 0 ↔ ( 𝐹 ‘ ∅ ) = ∅ ) )
123 121 122 ax-mp ⊢ ( ( ♯ ‘ ( 𝐹 ‘ ∅ ) ) = 0 ↔ ( 𝐹 ‘ ∅ ) = ∅ )
124 120 123 sylib ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝐹 ‘ ∅ ) = ∅ )
125 56 56 pm3.2i ⊢ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ∈ Mnd ∧ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ∈ Mnd )
126 49 frmd0 ⊢ ∅ = ( 0g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) )
127 74 74 75 75 126 126 ismhm ⊢ ( 𝐹 ∈ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) MndHom ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ↔ ( ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ∈ Mnd ∧ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ∈ Mnd ) ∧ ( 𝐹 : Word ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) ∧ ∀ 𝑥 ∈ Word ( 𝐶 ∪ 𝑉 ) ∀ 𝑦 ∈ Word ( 𝐶 ∪ 𝑉 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ∅ ) = ∅ ) ) )
128 125 127 mpbiran ⊢ ( 𝐹 ∈ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) MndHom ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ↔ ( 𝐹 : Word ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) ∧ ∀ 𝑥 ∈ Word ( 𝐶 ∪ 𝑉 ) ∀ 𝑦 ∈ Word ( 𝐶 ∪ 𝑉 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ∅ ) = ∅ ) )
129 63 93 124 128 syl3anbrc ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 ∈ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) MndHom ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) )
130 eqid ⊢ ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) = ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) )
131 130 vrmdf ⊢ ( ( 𝐶 ∪ 𝑉 ) ∈ V → ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) : ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) )
132 54 131 ax-mp ⊢ ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) : ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 )
133 fcompt ⊢ ( ( 𝐹 : Word ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) ∧ ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) : ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) ) → ( 𝐹 ∘ ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ( ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ‘ 𝑣 ) ) ) )
134 63 132 133 sylancl ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝐹 ∘ ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ( ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ‘ 𝑣 ) ) ) )
135 130 vrmdval ⊢ ( ( ( 𝐶 ∪ 𝑉 ) ∈ V ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ‘ 𝑣 ) = ⟨“ 𝑣 ”⟩ )
136 54 135 mpan ⊢ ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) → ( ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ‘ 𝑣 ) = ⟨“ 𝑣 ”⟩ )
137 136 fveq2d ⊢ ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) → ( 𝐹 ‘ ( ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ‘ 𝑣 ) ) = ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) )
138 137 mpteq2ia ⊢ ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ( ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ‘ 𝑣 ) ) ) = ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) )
139 134 138 eqtrdi ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝐹 ∘ ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) )
140 49 74 130 frmdup3lem ⊢ ( ( ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ∈ Mnd ∧ ( 𝐶 ∪ 𝑉 ) ∈ V ∧ ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) : ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) ) ∧ ( 𝐹 ∈ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) MndHom ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) ∧ ( 𝐹 ∘ ( varFMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) ) ) → 𝐹 = ( 𝑟 ∈ Word ( 𝐶 ∪ 𝑉 ) ↦ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) ) ) )
141 57 58 60 129 139 140 syl32anc ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 = ( 𝑟 ∈ Word ( 𝐶 ∪ 𝑉 ) ↦ ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ ( 𝐹 ‘ ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑟 ) ) ) )
142 37 51 141 3eqtr4rd ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 = ( 𝑆 ‘ ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ) )
143 3 2 1 mrsubff ⊢ ( 𝑇 ∈ 𝑊 → 𝑆 : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) )
144 143 ffnd ⊢ ( 𝑇 ∈ 𝑊 → 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) )
145 144 adantr ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) )
146 2 fvexi ⊢ 𝑅 ∈ V
147 elpm2r ⊢ ( ( ( 𝑅 ∈ V ∧ 𝑉 ∈ V ) ∧ ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ) ) → ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ∈ ( 𝑅 ↑pm 𝑉 ) )
148 146 53 147 mpanl12 ⊢ ( ( ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ) → ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ∈ ( 𝑅 ↑pm 𝑉 ) )
149 47 48 148 sylancl ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ∈ ( 𝑅 ↑pm 𝑉 ) )
150 fnfvelrn ⊢ ( ( 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) ∧ ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑆 ‘ ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ) ∈ ran 𝑆 )
151 145 149 150 syl2anc ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑆 ‘ ( 𝑤 ∈ 𝑉 ↦ ( 𝐹 ‘ ⟨“ 𝑤 ”⟩ ) ) ) ∈ ran 𝑆 )
152 142 151 eqeltrd ⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 ∈ ran 𝑆 )
153 152 ex ⊢ ( 𝑇 ∈ 𝑊 → ( ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 ∈ ran 𝑆 ) )
154 11 153 impbid2 ⊢ ( 𝑇 ∈ 𝑊 → ( 𝐹 ∈ ran 𝑆 ↔ ( 𝐹 : 𝑅 ⟶ 𝑅 ∧ ∀ 𝑐 ∈ ( 𝐶 ∖ 𝑉 ) ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝐹 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ++ ( 𝐹 ‘ 𝑦 ) ) ) ) )