elmrsubrn - Mathbox for Mario Carneiro

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

Theorem elmrsubrn 35718

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 35747.) (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.

Step	Hyp	Ref	Expression
1		mrsubccat.s	. . . 4 ⊢ 𝑆 = (mRSubst‘𝑇)
2		mrsubccat.r	. . . 4 ⊢ 𝑅 = (mREx‘𝑇)
3	1, 2	mrsubf 35715	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
4		mrsubcn.v	. . . . 5 ⊢ 𝑉 = (mVR‘𝑇)
5		mrsubcn.c	. . . . 5 ⊢ 𝐶 = (mCN‘𝑇)
6	1, 2, 4, 5	mrsubcn 35717	. . . 4 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
7	6	ralrimiva 3130	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
8	1, 2	mrsubccat 35716	. . . . 5 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
9	8	3expb 1121	. . . 4 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
10	9	ralrimivva 3181	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
11	3, 7, 10	3jca 1129	. 2 ⊢ (𝐹 ∈ ran 𝑆 → (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
12	5, 4, 2	mrexval 35699	. . . . . . 7 ⊢ (𝑇 ∈ 𝑊 → 𝑅 = Word (𝐶 ∪ 𝑉))
13	12	adantr 480	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑅 = Word (𝐶 ∪ 𝑉))
14		s1eq 14554	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑣 → ⟨“𝑤”⟩ = ⟨“𝑣”⟩)
15	14	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝐹‘⟨“𝑤”⟩) = (𝐹‘⟨“𝑣”⟩))
16		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))
17		fvex 6847	. . . . . . . . . . . 12 ⊢ (𝐹‘⟨“𝑣”⟩) ∈ V
18	15, 16, 17	fvmpt 6941	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑉 → ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
19	18	adantl 481	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝑉) → ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
20		difun2 4422	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∪ 𝑉) ∖ 𝑉) = (𝐶 ∖ 𝑉)
21	20	eleq2i 2829	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ 𝑣 ∈ (𝐶 ∖ 𝑉))
22		eldif 3900	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉))
23	21, 22	bitr3i 277	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝐶 ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉))
24		simpr2 1197	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
25		s1eq 14554	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑣 → ⟨“𝑐”⟩ = ⟨“𝑣”⟩)
26	25	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑣 → (𝐹‘⟨“𝑐”⟩) = (𝐹‘⟨“𝑣”⟩))
27	26, 25	eqeq12d 2753	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑣 → ((𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ↔ (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩))
28	27	rspccva 3564	. . . . . . . . . . . . . 14 ⊢ ((∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
29	24, 28	sylan 581	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
30	23, 29	sylan2br 596	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
31	30	anassrs 467	. . . . . . . . . . 11 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
32	31	eqcomd 2743	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → ⟨“𝑣”⟩ = (𝐹‘⟨“𝑣”⟩))
33	19, 32	ifeqda 4504	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩) = (𝐹‘⟨“𝑣”⟩))
34	33	mpteq2dva 5179	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
35	34	coeq1d 5810	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟) = ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))
36	35	oveq2d 7376	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟)) = ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟)))
37	13, 36	mpteq12dv 5173	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))) = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
38		elun2 4124	. . . . . . . 8 ⊢ (𝑣 ∈ 𝑉 → 𝑣 ∈ (𝐶 ∪ 𝑉))
39		simplr1 1217	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝐹:𝑅⟶𝑅)
40		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑣 ∈ (𝐶 ∪ 𝑉))
41	40	s1cld 14557	. . . . . . . . . 10 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ⟨“𝑣”⟩ ∈ Word (𝐶 ∪ 𝑉))
42	12	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑅 = Word (𝐶 ∪ 𝑉))
43	41, 42	eleqtrrd 2840	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ⟨“𝑣”⟩ ∈ 𝑅)
44	39, 43	ffvelcdmd 7031	. . . . . . . 8 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
45	38, 44	sylan2 594	. . . . . . 7 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
46	15	cbvmptv 5190	. . . . . . 7 ⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑣 ∈ 𝑉 ↦ (𝐹‘⟨“𝑣”⟩))
47	45, 46	fmptd 7060	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅)
48		ssid 3945	. . . . . 6 ⊢ 𝑉 ⊆ 𝑉
49		eqid 2737	. . . . . . 7 ⊢ (freeMnd‘(𝐶 ∪ 𝑉)) = (freeMnd‘(𝐶 ∪ 𝑉))
50	5, 4, 2, 1, 49	mrsubfval 35706	. . . . . 6 ⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
51	47, 48, 50	sylancl 587	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
52	5	fvexi 6848	. . . . . . . . 9 ⊢ 𝐶 ∈ V
53	4	fvexi 6848	. . . . . . . . 9 ⊢ 𝑉 ∈ V
54	52, 53	unex 7691	. . . . . . . 8 ⊢ (𝐶 ∪ 𝑉) ∈ V
55	49	frmdmnd 18818	. . . . . . . 8 ⊢ ((𝐶 ∪ 𝑉) ∈ V → (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd)
56	54, 55	ax-mp 5	. . . . . . 7 ⊢ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd
57	56	a1i 11	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd)
58	54	a1i 11	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐶 ∪ 𝑉) ∈ V)
59	44, 42	eleqtrd 2839	. . . . . . 7 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ Word (𝐶 ∪ 𝑉))
60	59	fmpttd 7061	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
61		simpr1 1196	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:𝑅⟶𝑅)
62	13, 13	feq23d 6657	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹:𝑅⟶𝑅 ↔ 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)))
63	61, 62	mpbid 232	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
64		simpr3 1198	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
65		simprl 771	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ 𝑅)
66	12	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → 𝑅 = Word (𝐶 ∪ 𝑉))
67	66	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑅 = Word (𝐶 ∪ 𝑉))
68	65, 67	eleqtrd 2839	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ Word (𝐶 ∪ 𝑉))
69		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ 𝑅)
70	69, 67	eleqtrd 2839	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ Word (𝐶 ∪ 𝑉))
71		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉)))
72	49, 71	frmdbas 18811	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∪ 𝑉) ∈ V → (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉))
73	54, 72	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉)
74	73	eqcomi 2746	. . . . . . . . . . . . . . 15 ⊢ Word (𝐶 ∪ 𝑉) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉)))
75		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (+_g‘(freeMnd‘(𝐶 ∪ 𝑉))) = (+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))
76	49, 74, 75	frmdadd 18814	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Word (𝐶 ∪ 𝑉) ∧ 𝑦 ∈ Word (𝐶 ∪ 𝑉)) → (𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦))
77	68, 70, 76	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦))
78	77	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = (𝐹‘(𝑥 ++ 𝑦)))
79		ffvelcdm 7027	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑥 ∈ 𝑅) → (𝐹‘𝑥) ∈ 𝑅)
80	79	ad2ant2lr 749	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ 𝑅)
81	80, 67	eleqtrd 2839	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉))
82		ffvelcdm 7027	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘𝑦) ∈ 𝑅)
83	82	ad2ant2l 747	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ 𝑅)
84	83, 67	eleqtrd 2839	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉))
85	49, 74, 75	frmdadd 18814	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) → ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
86	81, 84, 85	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
87	78, 86	eqeq12d 2753	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
88	87	2ralbidva 3200	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
89	66	raleqdv 3296	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
90	66, 89	raleqbidv 3312	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
91	88, 90	bitr3d 281	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
92	91	3ad2antr1 1190	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
93	64, 92	mpbid 232	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))
94		wrd0 14492	. . . . . . . . . . . 12 ⊢ ∅ ∈ Word (𝐶 ∪ 𝑉)
95		ffvelcdm 7027	. . . . . . . . . . . 12 ⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∅ ∈ Word (𝐶 ∪ 𝑉)) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉))
96	63, 94, 95	sylancl 587	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉))
97		lencl 14486	. . . . . . . . . . 11 ⊢ ((𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉) → (♯‘(𝐹‘∅)) ∈ ℕ₀)
98	96, 97	syl 17	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℕ₀)
99	98	nn0cnd 12491	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℂ)
100		0cnd 11128	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 0 ∈ ℂ)
101	99	addridd 11337	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + 0) = (♯‘(𝐹‘∅)))
102	94, 13	eleqtrrid 2844	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∅ ∈ 𝑅)
103		fvoveq1 7383	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (𝐹‘(𝑥 ++ 𝑦)) = (𝐹‘(∅ ++ 𝑦)))
104		fveq2 6834	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → (𝐹‘𝑥) = (𝐹‘∅))
105	104	oveq1d 7375	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → ((𝐹‘𝑥) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)))
106	103, 105	eqeq12d 2753	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → ((𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ (𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦))))
107		oveq2 7368	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (∅ ++ 𝑦) = (∅ ++ ∅))
108		ccatidid 14544	. . . . . . . . . . . . . . . 16 ⊢ (∅ ++ ∅) = ∅
109	107, 108	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (∅ ++ 𝑦) = ∅)
110	109	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → (𝐹‘(∅ ++ 𝑦)) = (𝐹‘∅))
111		fveq2 6834	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (𝐹‘𝑦) = (𝐹‘∅))
112	111	oveq2d 7376	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ((𝐹‘∅) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘∅)))
113	110, 112	eqeq12d 2753	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → ((𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)) ↔ (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))))
114	106, 113	rspc2va 3577	. . . . . . . . . . . 12 ⊢ (((∅ ∈ 𝑅 ∧ ∅ ∈ 𝑅) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
115	102, 102, 64, 114	syl21anc 838	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
116	115	fveq2d 6838	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = (♯‘((𝐹‘∅) ++ (𝐹‘∅))))
117		ccatlen 14528	. . . . . . . . . . 11 ⊢ (((𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
118	96, 96, 117	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
119	101, 116, 118	3eqtrrd 2777	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))) = ((♯‘(𝐹‘∅)) + 0))
120	99, 99, 100, 119	addcanad 11342	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = 0)
121		fvex 6847	. . . . . . . . 9 ⊢ (𝐹‘∅) ∈ V
122		hasheq0 14316	. . . . . . . . 9 ⊢ ((𝐹‘∅) ∈ V → ((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) = ∅))
123	121, 122	ax-mp 5	. . . . . . . 8 ⊢ ((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) = ∅)
124	120, 123	sylib 218	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ∅)
125	56, 56	pm3.2i 470	. . . . . . . 8 ⊢ ((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd)
126	49	frmd0 18819	. . . . . . . . 9 ⊢ ∅ = (0_g‘(freeMnd‘(𝐶 ∪ 𝑉)))
127	74, 74, 75, 75, 126, 126	ismhm 18744	. . . . . . . 8 ⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) ∧ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) = ∅)))
128	125, 127	mpbiran 710	. . . . . . 7 ⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) = ∅))
129	63, 93, 124, 128	syl3anbrc 1345	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))))
130		eqid 2737	. . . . . . . . . 10 ⊢ (var_FMnd‘(𝐶 ∪ 𝑉)) = (var_FMnd‘(𝐶 ∪ 𝑉))
131	130	vrmdf 18817	. . . . . . . . 9 ⊢ ((𝐶 ∪ 𝑉) ∈ V → (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
132	54, 131	ax-mp 5	. . . . . . . 8 ⊢ (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)
133		fcompt 7080	. . . . . . . 8 ⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))))
134	63, 132, 133	sylancl 587	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))))
135	130	vrmdval 18816	. . . . . . . . . 10 ⊢ (((𝐶 ∪ 𝑉) ∈ V ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣) = ⟨“𝑣”⟩)
136	54, 135	mpan 691	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) → ((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣) = ⟨“𝑣”⟩)
137	136	fveq2d 6838	. . . . . . . 8 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) → (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣)) = (𝐹‘⟨“𝑣”⟩))
138	137	mpteq2ia 5181	. . . . . . 7 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩))
139	134, 138	eqtrdi 2788	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
140	49, 74, 130	frmdup3lem 18825	. . . . . 6 ⊢ ((((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (𝐶 ∪ 𝑉) ∈ V ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) ∧ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ∧ (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
141	57, 58, 60, 129, 139, 140	syl32anc 1381	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
142	37, 51, 141	3eqtr4rd 2783	. . . 4 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))))
143	4, 2, 1	mrsubff 35710	. . . . . . 7 ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑_pm 𝑉)⟶(𝑅 ↑_m 𝑅))
144	143	ffnd 6663	. . . . . 6 ⊢ (𝑇 ∈ 𝑊 → 𝑆 Fn (𝑅 ↑_pm 𝑉))
145	144	adantr 480	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑆 Fn (𝑅 ↑_pm 𝑉))
146	2	fvexi 6848	. . . . . . 7 ⊢ 𝑅 ∈ V
147		elpm2r 8785	. . . . . . 7 ⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉)) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
148	146, 53, 147	mpanl12 703	. . . . . 6 ⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
149	47, 48, 148	sylancl 587	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
150		fnfvelrn 7026	. . . . 5 ⊢ ((𝑆 Fn (𝑅 ↑_pm 𝑉) ∧ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉)) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
151	145, 149, 150	syl2anc 585	. . . 4 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
152	142, 151	eqeltrd 2837	. . 3 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ran 𝑆)
153	152	ex 412	. 2 ⊢ (𝑇 ∈ 𝑊 → ((𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → 𝐹 ∈ ran 𝑆))
154	11, 153	impbid2 226	1 ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 Vcvv 3430 ∖ cdif 3887 ∪ cun 3888 ⊆ wss 3890 ∅c0 4274 ifcif 4467 ↦ cmpt 5167 ran crn 5625 ∘ ccom 5628 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 (class class class)co 7360 ↑_m cmap 8766 ↑_pm cpm 8767 0cc0 11029 + caddc 11032 ℕ₀cn0 12428 ♯chash 14283 Word cword 14466 ++ cconcat 14523 ⟨“cs1 14549 Basecbs 17170 +_gcplusg 17211 Σ_g cgsu 17394 Mndcmnd 18693 MndHom cmhm 18740 freeMndcfrmd 18806 var_FMndcvrmd 18807 mCNcmcn 35658 mVRcmvar 35659 mRExcmrex 35664 mRSubstcmrsub 35668

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-er 8636 df-map 8768 df-pm 8769 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-n0 12429 df-xnn0 12502 df-z 12516 df-uz 12780 df-fz 13453 df-fzo 13600 df-seq 13955 df-hash 14284 df-word 14467 df-lsw 14516 df-concat 14524 df-s1 14550 df-substr 14595 df-pfx 14625 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-0g 17395 df-gsum 17396 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-mhm 18742 df-submnd 18743 df-frmd 18808 df-vrmd 18809 df-mrex 35684 df-mrsub 35688

This theorem is referenced by: mrsubco 35719

W3C validator