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 35830

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 35859.) (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 35827	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
4		mrsubcn.v	. . . . 5 ⊢ 𝑉 = (mVR‘𝑇)
5		mrsubcn.c	. . . . 5 ⊢ 𝐶 = (mCN‘𝑇)
6	1, 2, 4, 5	mrsubcn 35829	. . . 4 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
7	6	ralrimiva 3153	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
8	1, 2	mrsubccat 35828	. . . . 5 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
9	8	3expb 1132	. . . 4 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
10	9	ralrimivva 3204	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
11	3, 7, 10	3jca 1140	. 2 ⊢ (𝐹 ∈ ran 𝑆 → (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
12	5, 4, 2	mrexval 35811	. . . . . . 7 ⊢ (𝑇 ∈ 𝑊 → 𝑅 = Word (𝐶 ∪ 𝑉))
13	12	adantr 484	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑅 = Word (𝐶 ∪ 𝑉))
14		s1eq 14607	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑣 → ⟨“𝑤”⟩ = ⟨“𝑣”⟩)
15	14	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝐹‘⟨“𝑤”⟩) = (𝐹‘⟨“𝑣”⟩))
16		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))
17		fvex 6874	. . . . . . . . . . . 12 ⊢ (𝐹‘⟨“𝑣”⟩) ∈ V
18	15, 16, 17	fvmpt 6969	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑉 → ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
19	18	adantl 485	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝑉) → ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
20		difun2 4432	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∪ 𝑉) ∖ 𝑉) = (𝐶 ∖ 𝑉)
21	20	eleq2i 2853	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ 𝑣 ∈ (𝐶 ∖ 𝑉))
22		eldif 3912	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉))
23	21, 22	bitr3i 279	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝐶 ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉))
24		simpr2 1208	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
25		s1eq 14607	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑣 → ⟨“𝑐”⟩ = ⟨“𝑣”⟩)
26	25	fveq2d 6865	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑣 → (𝐹‘⟨“𝑐”⟩) = (𝐹‘⟨“𝑣”⟩))
27	26, 25	eqeq12d 2777	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑣 → ((𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ↔ (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩))
28	27	rspccva 3579	. . . . . . . . . . . . . 14 ⊢ ((∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
29	24, 28	sylan 589	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
30	23, 29	sylan2br 604	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
31	30	anassrs 471	. . . . . . . . . . 11 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
32	31	eqcomd 2767	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → ⟨“𝑣”⟩ = (𝐹‘⟨“𝑣”⟩))
33	19, 32	ifeqda 4514	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩) = (𝐹‘⟨“𝑣”⟩))
34	33	mpteq2dva 5190	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
35	34	coeq1d 5829	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟) = ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))
36	35	oveq2d 7406	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟)) = ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟)))
37	13, 36	mpteq12dv 5184	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))) = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
38		elun2 4133	. . . . . . . 8 ⊢ (𝑣 ∈ 𝑉 → 𝑣 ∈ (𝐶 ∪ 𝑉))
39		simplr1 1228	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝐹:𝑅⟶𝑅)
40		simpr 488	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑣 ∈ (𝐶 ∪ 𝑉))
41	40	s1cld 14610	. . . . . . . . . 10 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ⟨“𝑣”⟩ ∈ Word (𝐶 ∪ 𝑉))
42	12	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑅 = Word (𝐶 ∪ 𝑉))
43	41, 42	eleqtrrd 2864	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ⟨“𝑣”⟩ ∈ 𝑅)
44	39, 43	ffvelcdmd 7060	. . . . . . . 8 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
45	38, 44	sylan2 602	. . . . . . 7 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
46	15	cbvmptv 5201	. . . . . . 7 ⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑣 ∈ 𝑉 ↦ (𝐹‘⟨“𝑣”⟩))
47	45, 46	fmptd 7089	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅)
48		ssid 3956	. . . . . 6 ⊢ 𝑉 ⊆ 𝑉
49		eqid 2761	. . . . . . 7 ⊢ (freeMnd‘(𝐶 ∪ 𝑉)) = (freeMnd‘(𝐶 ∪ 𝑉))
50	5, 4, 2, 1, 49	mrsubfval 35818	. . . . . 6 ⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
51	47, 48, 50	sylancl 595	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
52	5	fvexi 6875	. . . . . . . . 9 ⊢ 𝐶 ∈ V
53	4	fvexi 6875	. . . . . . . . 9 ⊢ 𝑉 ∈ V
54	52, 53	unex 7721	. . . . . . . 8 ⊢ (𝐶 ∪ 𝑉) ∈ V
55	49	frmdmnd 18883	. . . . . . . 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 2863	. . . . . . 7 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ Word (𝐶 ∪ 𝑉))
60	59	fmpttd 7090	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
61		simpr1 1207	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:𝑅⟶𝑅)
62	13, 13	feq23d 6680	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹:𝑅⟶𝑅 ↔ 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)))
63	61, 62	mpbid 234	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
64		simpr3 1209	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
65		simprl 780	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ 𝑅)
66	12	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → 𝑅 = Word (𝐶 ∪ 𝑉))
67	66	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑅 = Word (𝐶 ∪ 𝑉))
68	65, 67	eleqtrd 2863	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ Word (𝐶 ∪ 𝑉))
69		simprr 782	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ 𝑅)
70	69, 67	eleqtrd 2863	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ Word (𝐶 ∪ 𝑉))
71		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉)))
72	49, 71	frmdbas 18876	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∪ 𝑉) ∈ V → (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉))
73	54, 72	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉)
74	73	eqcomi 2770	. . . . . . . . . . . . . . 15 ⊢ Word (𝐶 ∪ 𝑉) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉)))
75		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (+_g‘(freeMnd‘(𝐶 ∪ 𝑉))) = (+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))
76	49, 74, 75	frmdadd 18879	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Word (𝐶 ∪ 𝑉) ∧ 𝑦 ∈ Word (𝐶 ∪ 𝑉)) → (𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦))
77	68, 70, 76	syl2anc 593	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦))
78	77	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = (𝐹‘(𝑥 ++ 𝑦)))
79		ffvelcdm 7056	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑥 ∈ 𝑅) → (𝐹‘𝑥) ∈ 𝑅)
80	79	ad2ant2lr 758	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ 𝑅)
81	80, 67	eleqtrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉))
82		ffvelcdm 7056	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘𝑦) ∈ 𝑅)
83	82	ad2ant2l 756	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ 𝑅)
84	83, 67	eleqtrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉))
85	49, 74, 75	frmdadd 18879	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) → ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
86	81, 84, 85	syl2anc 593	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
87	78, 86	eqeq12d 2777	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
88	87	2ralbidva 3223	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
89	66	raleqdv 3319	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
90	66, 89	raleqbidv 3335	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
91	88, 90	bitr3d 283	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
92	91	3ad2antr1 1201	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
93	64, 92	mpbid 234	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)))
94		wrd0 14545	. . . . . . . . . . . 12 ⊢ ∅ ∈ Word (𝐶 ∪ 𝑉)
95		ffvelcdm 7056	. . . . . . . . . . . 12 ⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∅ ∈ Word (𝐶 ∪ 𝑉)) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉))
96	63, 94, 95	sylancl 595	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉))
97		lencl 14539	. . . . . . . . . . 11 ⊢ ((𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉) → (♯‘(𝐹‘∅)) ∈ ℕ₀)
98	96, 97	syl 17	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℕ₀)
99	98	nn0cnd 12537	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℂ)
100		0cnd 11165	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 0 ∈ ℂ)
101	99	addridd 11376	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + 0) = (♯‘(𝐹‘∅)))
102	94, 13	eleqtrrid 2868	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∅ ∈ 𝑅)
103		fvoveq1 7413	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (𝐹‘(𝑥 ++ 𝑦)) = (𝐹‘(∅ ++ 𝑦)))
104		fveq2 6861	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → (𝐹‘𝑥) = (𝐹‘∅))
105	104	oveq1d 7405	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → ((𝐹‘𝑥) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)))
106	103, 105	eqeq12d 2777	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → ((𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ (𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦))))
107		oveq2 7398	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (∅ ++ 𝑦) = (∅ ++ ∅))
108		ccatidid 14597	. . . . . . . . . . . . . . . 16 ⊢ (∅ ++ ∅) = ∅
109	107, 108	eqtrdi 2812	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (∅ ++ 𝑦) = ∅)
110	109	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → (𝐹‘(∅ ++ 𝑦)) = (𝐹‘∅))
111		fveq2 6861	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (𝐹‘𝑦) = (𝐹‘∅))
112	111	oveq2d 7406	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ((𝐹‘∅) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘∅)))
113	110, 112	eqeq12d 2777	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → ((𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)) ↔ (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))))
114	106, 113	rspc2va 3592	. . . . . . . . . . . 12 ⊢ (((∅ ∈ 𝑅 ∧ ∅ ∈ 𝑅) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
115	102, 102, 64, 114	syl21anc 848	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
116	115	fveq2d 6865	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = (♯‘((𝐹‘∅) ++ (𝐹‘∅))))
117		ccatlen 14581	. . . . . . . . . . 11 ⊢ (((𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
118	96, 96, 117	syl2anc 593	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
119	101, 116, 118	3eqtrrd 2801	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))) = ((♯‘(𝐹‘∅)) + 0))
120	99, 99, 100, 119	addcanad 11381	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = 0)
121		fvex 6874	. . . . . . . . 9 ⊢ (𝐹‘∅) ∈ V
122		hasheq0 14369	. . . . . . . . 9 ⊢ ((𝐹‘∅) ∈ V → ((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) = ∅))
123	121, 122	ax-mp 5	. . . . . . . 8 ⊢ ((♯‘(𝐹‘∅)) = 0 ↔ (𝐹‘∅) = ∅)
124	120, 123	sylib 220	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ∅)
125	56, 56	pm3.2i 474	. . . . . . . 8 ⊢ ((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd)
126	49	frmd0 18884	. . . . . . . . 9 ⊢ ∅ = (0_g‘(freeMnd‘(𝐶 ∪ 𝑉)))
127	74, 74, 75, 75, 126, 126	ismhm 18809	. . . . . . . 8 ⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd) ∧ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) = ∅)))
128	125, 127	mpbiran 719	. . . . . . 7 ⊢ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ↔ (𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∀𝑥 ∈ Word (𝐶 ∪ 𝑉)∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ∧ (𝐹‘∅) = ∅))
129	63, 93, 124, 128	syl3anbrc 1356	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))))
130		eqid 2761	. . . . . . . . . 10 ⊢ (var_FMnd‘(𝐶 ∪ 𝑉)) = (var_FMnd‘(𝐶 ∪ 𝑉))
131	130	vrmdf 18882	. . . . . . . . 9 ⊢ ((𝐶 ∪ 𝑉) ∈ V → (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
132	54, 131	ax-mp 5	. . . . . . . 8 ⊢ (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)
133		fcompt 7109	. . . . . . . 8 ⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))))
134	63, 132, 133	sylancl 595	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))))
135	130	vrmdval 18881	. . . . . . . . . 10 ⊢ (((𝐶 ∪ 𝑉) ∈ V ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣) = ⟨“𝑣”⟩)
136	54, 135	mpan 700	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) → ((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣) = ⟨“𝑣”⟩)
137	136	fveq2d 6865	. . . . . . . 8 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) → (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣)) = (𝐹‘⟨“𝑣”⟩))
138	137	mpteq2ia 5192	. . . . . . 7 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩))
139	134, 138	eqtrdi 2812	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
140	49, 74, 130	frmdup3lem 18890	. . . . . 6 ⊢ ((((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (𝐶 ∪ 𝑉) ∈ V ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) ∧ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ∧ (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
141	57, 58, 60, 129, 139, 140	syl32anc 1396	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
142	37, 51, 141	3eqtr4rd 2807	. . . 4 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))))
143	4, 2, 1	mrsubff 35822	. . . . . . 7 ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑_pm 𝑉)⟶(𝑅 ↑_m 𝑅))
144	143	ffnd 6686	. . . . . 6 ⊢ (𝑇 ∈ 𝑊 → 𝑆 Fn (𝑅 ↑_pm 𝑉))
145	144	adantr 484	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑆 Fn (𝑅 ↑_pm 𝑉))
146	2	fvexi 6875	. . . . . . 7 ⊢ 𝑅 ∈ V
147		elpm2r 8819	. . . . . . 7 ⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉)) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
148	146, 53, 147	mpanl12 712	. . . . . 6 ⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
149	47, 48, 148	sylancl 595	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
150		fnfvelrn 7055	. . . . 5 ⊢ ((𝑆 Fn (𝑅 ↑_pm 𝑉) ∧ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉)) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
151	145, 149, 150	syl2anc 593	. . . 4 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
152	142, 151	eqeltrd 2861	. . 3 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 ∈ ran 𝑆)
153	152	ex 416	. 2 ⊢ (𝑇 ∈ 𝑊 → ((𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → 𝐹 ∈ ran 𝑆))
154	11, 153	impbid2 228	1 ⊢ (𝑇 ∈ 𝑊 → (𝐹 ∈ ran 𝑆 ↔ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ∀wral 3075 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ⊆ wss 3902 ∅c0 4283 ifcif 4477 ↦ cmpt 5178 ran crn 5644 ∘ ccom 5647 Fn wfn 6510 ⟶wf 6511 ‘cfv 6515 (class class class)co 7390 ↑_m cmap 8801 ↑_pm cpm 8802 0cc0 11066 + caddc 11069 ℕ₀cn0 12474 ♯chash 14336 Word cword 14519 ++ cconcat 14576 ⟨“cs1 14602 Basecbs 17235 +_gcplusg 17276 Σ_g cgsu 17459 Mndcmnd 18758 MndHom cmhm 18805 freeMndcfrmd 18871 var_FMndcvrmd 18872 mCNcmcn 35770 mVRcmvar 35771 mRExcmrex 35776 mRSubstcmrsub 35780

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-cnex 11122 ax-resscn 11123 ax-1cn 11124 ax-icn 11125 ax-addcl 11126 ax-addrcl 11127 ax-mulcl 11128 ax-mulrcl 11129 ax-mulcom 11130 ax-addass 11131 ax-mulass 11132 ax-distr 11133 ax-i2m1 11134 ax-1ne0 11135 ax-1rid 11136 ax-rnegex 11137 ax-rrecex 11138 ax-cnre 11139 ax-pre-lttri 11140 ax-pre-lttrn 11141 ax-pre-ltadd 11142 ax-pre-mulgt0 11143

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 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 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-1st 7964 df-2nd 7965 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-er 8671 df-map 8803 df-pm 8804 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-card 9890 df-pnf 11211 df-mnf 11212 df-xr 11213 df-ltxr 11214 df-le 11215 df-sub 11409 df-neg 11410 df-nn 12204 df-2 12273 df-n0 12475 df-xnn0 12548 df-z 12562 df-uz 12833 df-fz 13506 df-fzo 13653 df-seq 14008 df-hash 14337 df-word 14520 df-lsw 14569 df-concat 14577 df-s1 14603 df-substr 14648 df-pfx 14678 df-struct 17173 df-sets 17190 df-slot 17208 df-ndx 17220 df-base 17236 df-ress 17257 df-plusg 17289 df-0g 17460 df-gsum 17461 df-mgm 18664 df-sgrp 18743 df-mnd 18759 df-mhm 18807 df-submnd 18808 df-frmd 18873 df-vrmd 18874 df-mrex 35796 df-mrsub 35800

This theorem is referenced by: mrsubco 35831

W3C validator