# 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 ${⊢}{S}=\mathrm{mRSubst}\left({T}\right)$
mrsubccat.r ${⊢}{R}=\mathrm{mREx}\left({T}\right)$
mrsubcn.v ${⊢}{V}=\mathrm{mVR}\left({T}\right)$
mrsubcn.c ${⊢}{C}=\mathrm{mCN}\left({T}\right)$
Assertion elmrsubrn ${⊢}{T}\in {W}\to \left({F}\in \mathrm{ran}{S}↔\left({F}:{R}⟶{R}\wedge \forall {c}\in \left({C}\setminus {V}\right)\phantom{\rule{.4em}{0ex}}{F}\left(⟨“{c}”⟩\right)=⟨“{c}”⟩\wedge \forall {x}\in {R}\phantom{\rule{.4em}{0ex}}\forall {y}\in {R}\phantom{\rule{.4em}{0ex}}{F}\left({x}\mathrm{++}{y}\right)={F}\left({x}\right)\mathrm{++}{F}\left({y}\right)\right)\right)$

### Proof

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