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 36107

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 36136.) (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 36104	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
4		mrsubcn.v	. . . . 5 ⊢ 𝑉 = (mVR‘𝑇)
5		mrsubcn.c	. . . . 5 ⊢ 𝐶 = (mCN‘𝑇)
6	1, 2, 4, 5	mrsubcn 36106	. . . 4 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
7	6	ralrimiva 3156	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
8	1, 2	mrsubccat 36105	. . . . 5 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
9	8	3expb 1138	. . . 4 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
10	9	ralrimivva 3207	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
11	3, 7, 10	3jca 1146	. 2 ⊢ (𝐹 ∈ ran 𝑆 → (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
12	5, 4, 2	mrexval 36088	. . . . . . 7 ⊢ (𝑇 ∈ 𝑊 → 𝑅 = Word (𝐶 ∪ 𝑉))
13	12	adantr 486	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑅 = Word (𝐶 ∪ 𝑉))
14		s1eq 14671	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑣 → ⟨“𝑤”⟩ = ⟨“𝑣”⟩)
15	14	fveq2d 6886	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝐹‘⟨“𝑤”⟩) = (𝐹‘⟨“𝑣”⟩))
16		eqid 2762	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))
17		fvex 6895	. . . . . . . . . . . 12 ⊢ (𝐹‘⟨“𝑣”⟩) ∈ V
18	15, 16, 17	fvmpt 6990	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑉 → ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
19	18	adantl 487	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝑉) → ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
20		difun2 4440	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∪ 𝑉) ∖ 𝑉) = (𝐶 ∖ 𝑉)
21	20	eleq2i 2854	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ 𝑣 ∈ (𝐶 ∖ 𝑉))
22		eldif 3912	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉))
23	21, 22	bitr3i 280	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝐶 ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉))
24		simpr2 1214	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
25		s1eq 14671	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑣 → ⟨“𝑐”⟩ = ⟨“𝑣”⟩)
26	25	fveq2d 6886	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑣 → (𝐹‘⟨“𝑐”⟩) = (𝐹‘⟨“𝑣”⟩))
27	26, 25	eqeq12d 2778	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑣 → ((𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ↔ (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩))
28	27	rspccva 3578	. . . . . . . . . . . . . 14 ⊢ ((∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
29	24, 28	sylan 592	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
30	23, 29	sylan2br 607	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
31	30	anassrs 473	. . . . . . . . . . 11 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
32	31	eqcomd 2768	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → ⟨“𝑣”⟩ = (𝐹‘⟨“𝑣”⟩))
33	19, 32	ifeqda 4522	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩) = (𝐹‘⟨“𝑣”⟩))
34	33	mpteq2dva 5202	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
35	34	coeq1d 5845	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟) = ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))
36	35	oveq2d 7433	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟)) = ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟)))
37	13, 36	mpteq12dv 5196	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))) = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
38		elun2 4132	. . . . . . . 8 ⊢ (𝑣 ∈ 𝑉 → 𝑣 ∈ (𝐶 ∪ 𝑉))
39		simplr1 1234	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝐹:𝑅⟶𝑅)
40		simpr 490	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑣 ∈ (𝐶 ∪ 𝑉))
41	40	s1cld 14674	. . . . . . . . . 10 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ⟨“𝑣”⟩ ∈ Word (𝐶 ∪ 𝑉))
42	12	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑅 = Word (𝐶 ∪ 𝑉))
43	41, 42	eleqtrrd 2865	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ⟨“𝑣”⟩ ∈ 𝑅)
44	39, 43	ffvelcdmd 7082	. . . . . . . 8 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
45	38, 44	sylan2 605	. . . . . . 7 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
46	15	cbvmptv 5213	. . . . . . 7 ⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑣 ∈ 𝑉 ↦ (𝐹‘⟨“𝑣”⟩))
47	45, 46	fmptd 7111	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅)
48		ssid 3956	. . . . . 6 ⊢ 𝑉 ⊆ 𝑉
49		eqid 2762	. . . . . . 7 ⊢ (freeMnd‘(𝐶 ∪ 𝑉)) = (freeMnd‘(𝐶 ∪ 𝑉))
50	5, 4, 2, 1, 49	mrsubfval 36095	. . . . . 6 ⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
51	47, 48, 50	sylancl 598	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
52	5	fvexi 6896	. . . . . . . . 9 ⊢ 𝐶 ∈ V
53	4	fvexi 6896	. . . . . . . . 9 ⊢ 𝑉 ∈ V
54	52, 53	unex 7750	. . . . . . . 8 ⊢ (𝐶 ∪ 𝑉) ∈ V
55	49	frmdmnd 18974	. . . . . . . 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 2864	. . . . . . 7 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ Word (𝐶 ∪ 𝑉))
60	59	fmpttd 7112	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
61		simpr1 1213	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:𝑅⟶𝑅)
62	13, 13	feq23d 6701	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹:𝑅⟶𝑅 ↔ 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)))
63	61, 62	mpbid 235	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
64		simpr3 1215	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
65		simprl 783	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ 𝑅)
66	12	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → 𝑅 = Word (𝐶 ∪ 𝑉))
67	66	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑅 = Word (𝐶 ∪ 𝑉))
68	65, 67	eleqtrd 2864	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ Word (𝐶 ∪ 𝑉))
69		simprr 785	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ 𝑅)
70	69, 67	eleqtrd 2864	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ Word (𝐶 ∪ 𝑉))
71		eqid 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉)))
72	49, 71	frmdbas 18967	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∪ 𝑉) ∈ V → (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉))
73	54, 72	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉)
74	73	eqcomi 2771	. . . . . . . . . . . . . . 15 ⊢ Word (𝐶 ∪ 𝑉) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉)))
75		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (+_g‘(freeMnd‘(𝐶 ∪ 𝑉))) = (+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))
76	49, 74, 75	frmdadd 18970	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Word (𝐶 ∪ 𝑉) ∧ 𝑦 ∈ Word (𝐶 ∪ 𝑉)) → (𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦))
77	68, 70, 76	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦))
78	77	fveq2d 6886	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = (𝐹‘(𝑥 ++ 𝑦)))
79		ffvelcdm 7078	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑥 ∈ 𝑅) → (𝐹‘𝑥) ∈ 𝑅)
80	79	ad2ant2lr 761	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ 𝑅)
81	80, 67	eleqtrd 2864	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉))
82		ffvelcdm 7078	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘𝑦) ∈ 𝑅)
83	82	ad2ant2l 759	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ 𝑅)
84	83, 67	eleqtrd 2864	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉))
85	49, 74, 75	frmdadd 18970	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) → ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
86	81, 84, 85	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
87	78, 86	eqeq12d 2778	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
88	87	2ralbidva 3226	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
89	66	raleqdv 3321	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
90	66, 89	raleqbidv 3336	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
91	88, 90	bitr3d 284	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
92	91	3ad2antr1 1207	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
93	64, 92	mpbid 235	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))
94		wrd0 14608	. . . . . . . . . . . 12 ⊢ ∅ ∈ Word (𝐶 ∪ 𝑉)
95		ffvelcdm 7078	. . . . . . . . . . . 12 ⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∅ ∈ Word (𝐶 ∪ 𝑉)) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉))
96	63, 94, 95	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉))
97		lencl 14602	. . . . . . . . . . 11 ⊢ ((𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉) → (♯‘(𝐹‘∅)) ∈ ℕ₀)
98	96, 97	syl 18	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℕ₀)
99	98	nn0cnd 12595	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℂ)
100		0cnd 11227	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 0 ∈ ℂ)
101	99	addridd 11438	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + 0) = (♯‘(𝐹‘∅)))
102	94, 13	eleqtrrid 2869	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∅ ∈ 𝑅)
103		fvoveq1 7440	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (𝐹‘(𝑥 ++ 𝑦)) = (𝐹‘(∅ ++ 𝑦)))
104		fveq2 6882	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → (𝐹‘𝑥) = (𝐹‘∅))
105	104	oveq1d 7432	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → ((𝐹‘𝑥) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)))
106	103, 105	eqeq12d 2778	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → ((𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ (𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦))))
107		oveq2 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (∅ ++ 𝑦) = (∅ ++ ∅))
108		ccatidid 14661	. . . . . . . . . . . . . . . 16 ⊢ (∅ ++ ∅) = ∅
109	107, 108	eqtrdi 2813	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (∅ ++ 𝑦) = ∅)
110	109	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → (𝐹‘(∅ ++ 𝑦)) = (𝐹‘∅))
111		fveq2 6882	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (𝐹‘𝑦) = (𝐹‘∅))
112	111	oveq2d 7433	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ((𝐹‘∅) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘∅)))
113	110, 112	eqeq12d 2778	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → ((𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)) ↔ (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))))
114	106, 113	rspc2va 3591	. . . . . . . . . . . 12 ⊢ (((∅ ∈ 𝑅 ∧ ∅ ∈ 𝑅) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
115	102, 102, 64, 114	syl21anc 851	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
116	115	fveq2d 6886	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = (♯‘((𝐹‘∅) ++ (𝐹‘∅))))
117		ccatlen 14644	. . . . . . . . . . 11 ⊢ (((𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
118	96, 96, 117	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
119	101, 116, 118	3eqtrrd 2802	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))) = ((♯‘(𝐹‘∅)) + 0))
120	99, 99, 100, 119	addcanad 11443	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = 0)
121		fvex 6895	. . . . . . . . 9 ⊢ (𝐹‘∅) ∈ V
122		hasheq0 14431	. . . . . . . . 9 ⊢ ((𝐹‘∅) ∈ V → ((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) = ∅))
123	121, 122	ax-mp 5	. . . . . . . 8 ⊢ ((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) = ∅)
124	120, 123	sylib 221	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ∅)
125	56, 56	pm3.2i 476	. . . . . . . 8 ⊢ ((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd)
126	49	frmd0 18975	. . . . . . . . 9 ⊢ ∅ = (0_g‘(freeMnd‘(𝐶 ∪ 𝑉)))
127	74, 74, 75, 75, 126, 126	ismhm 18899	. . . . . . . 8 ⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) ∧ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) = ∅)))
128	125, 127	mpbiran 722	. . . . . . 7 ⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) = ∅))
129	63, 93, 124, 128	syl3anbrc 1362	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))))
130		eqid 2762	. . . . . . . . . 10 ⊢ (var_FMnd‘(𝐶 ∪ 𝑉)) = (var_FMnd‘(𝐶 ∪ 𝑉))
131	130	vrmdf 18973	. . . . . . . . 9 ⊢ ((𝐶 ∪ 𝑉) ∈ V → (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
132	54, 131	ax-mp 5	. . . . . . . 8 ⊢ (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)
133		fcompt 7131	. . . . . . . 8 ⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))))
134	63, 132, 133	sylancl 598	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))))
135	130	vrmdval 18972	. . . . . . . . . 10 ⊢ (((𝐶 ∪ 𝑉) ∈ V ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣) = ⟨“𝑣”⟩)
136	54, 135	mpan 703	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) → ((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣) = ⟨“𝑣”⟩)
137	136	fveq2d 6886	. . . . . . . 8 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) → (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣)) = (𝐹‘⟨“𝑣”⟩))
138	137	mpteq2ia 5204	. . . . . . 7 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩))
139	134, 138	eqtrdi 2813	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
140	49, 74, 130	frmdup3lem 18981	. . . . . 6 ⊢ ((((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (𝐶 ∪ 𝑉) ∈ V ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) ∧ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ∧ (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
141	57, 58, 60, 129, 139, 140	syl32anc 1405	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
142	37, 51, 141	3eqtr4rd 2808	. . . 4 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))))
143	4, 2, 1	mrsubff 36099	. . . . . . 7 ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑_pm 𝑉)⟶(𝑅 ↑_m 𝑅))
144	143	ffnd 6707	. . . . . 6 ⊢ (𝑇 ∈ 𝑊 → 𝑆 Fn (𝑅 ↑_pm 𝑉))
145	144	adantr 486	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑆 Fn (𝑅 ↑_pm 𝑉))
146	2	fvexi 6896	. . . . . . 7 ⊢ 𝑅 ∈ V
147		elpm2r 8848	. . . . . . 7 ⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉)) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
148	146, 53, 147	mpanl12 715	. . . . . 6 ⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
149	47, 48, 148	sylancl 598	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
150		fnfvelrn 7077	. . . . 5 ⊢ ((𝑆 Fn (𝑅 ↑_pm 𝑉) ∧ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉)) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
151	145, 149, 150	syl2anc 596	. . . 4 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
152	142, 151	eqeltrd 2862	. . 3 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ran 𝑆)
153	152	ex 418	. 2 ⊢ (𝑇 ∈ 𝑊 → ((𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → 𝐹 ∈ ran 𝑆))
154	11, 153	impbid2 229	1 ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3078 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ⊆ wss 3902 ∅c0 4282 ifcif 4485 ↦ cmpt 5190 ran crn 5660 ∘ ccom 5663 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7417 ↑_m cmap 8830 ↑_pm cpm 8831 0cc0 11128 + caddc 11131 ℕ₀cn0 12532 ♯chash 14398 Word cword 14582 ++ cconcat 14639 ⟨“cs1 14666 Basecbs 17307 +_gcplusg 17348 Σ_g cgsu 17531 Mndcmnd 18842 MndHom cmhm 18895 freeMndcfrmd 18962 var_FMndcvrmd 18963 mCNcmcn 36047 mVRcmvar 36048 mRExcmrex 36053 mRSubstcmrsub 36057

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-map 8832 df-pm 8833 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-2 12331 df-n0 12533 df-xnn0 12606 df-z 12620 df-uz 12892 df-fz 13566 df-fzo 13714 df-seq 14070 df-hash 14399 df-word 14583 df-lsw 14632 df-concat 14640 df-s1 14667 df-substr 14713 df-pfx 14745 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-0g 17532 df-gsum 17533 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-mhm 18897 df-submnd 18898 df-frmd 18964 df-vrmd 18965 df-mrex 36073 df-mrsub 36077

This theorem is used by: mrsubco 36108

W3C validator