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 36465

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 36494.) (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 36462	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅)
4		mrsubcn.v	. . . . 5 ⊢ 𝑉 = (mVR‘𝑇)
5		mrsubcn.c	. . . . 5 ⊢ 𝐶 = (mCN‘𝑇)
6	1, 2, 4, 5	mrsubcn 36464	. . . 4 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
7	6	ralrimiva 3158	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
8	1, 2	mrsubccat 36463	. . . . 5 ⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
9	8	3expb 1138	. . . 4 ⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
10	9	ralrimivva 3209	. . 3 ⊢ (𝐹 ∈ ran 𝑆 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
11	3, 7, 10	3jca 1146	. 2 ⊢ (𝐹 ∈ ran 𝑆 → (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
12	5, 4, 2	mrexval 36446	. . . . . . 7 ⊢ (𝑇 ∈ 𝑊 → 𝑅 = Word (𝐶 ∪ 𝑉))
13	12	adantr 486	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑅 = Word (𝐶 ∪ 𝑉))
14		s1eq 14777	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑣 → ⟨“𝑤”⟩ = ⟨“𝑣”⟩)
15	14	fveq2d 6915	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝐹‘⟨“𝑤”⟩) = (𝐹‘⟨“𝑣”⟩))
16		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))
17		fvex 6924	. . . . . . . . . . . 12 ⊢ (𝐹‘⟨“𝑣”⟩) ∈ V
18	15, 16, 17	fvmpt 7019	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑉 → ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
19	18	adantl 487	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝑉) → ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣) = (𝐹‘⟨“𝑣”⟩))
20		difun2 4440	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∪ 𝑉) ∖ 𝑉) = (𝐶 ∖ 𝑉)
21	20	eleq2i 2856	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ 𝑣 ∈ (𝐶 ∖ 𝑉))
22		eldif 4052	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ((𝐶 ∪ 𝑉) ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉))
23	21, 22	bitr3i 280	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝐶 ∖ 𝑉) ↔ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉))
24		simpr2 1214	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩)
25		s1eq 14777	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑣 → ⟨“𝑐”⟩ = ⟨“𝑣”⟩)
26	25	fveq2d 6915	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑣 → (𝐹‘⟨“𝑐”⟩) = (𝐹‘⟨“𝑣”⟩))
27	26, 25	eqeq12d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑣 → ((𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ↔ (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩))
28	27	rspccva 3579	. . . . . . . . . . . . . 14 ⊢ ((∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
29	24, 28	sylan 592	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∖ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
30	23, 29	sylan2br 607	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ∧ ¬ 𝑣 ∈ 𝑉)) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
31	30	anassrs 473	. . . . . . . . . . 11 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → (𝐹‘⟨“𝑣”⟩) = ⟨“𝑣”⟩)
32	31	eqcomd 2769	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝑉) → ⟨“𝑣”⟩ = (𝐹‘⟨“𝑣”⟩))
33	19, 32	ifeqda 4522	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩) = (𝐹‘⟨“𝑣”⟩))
34	33	mpteq2dva 5202	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
35	34	coeq1d 5846	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟) = ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))
36	35	oveq2d 7462	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟)) = ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟)))
37	13, 36	mpteq12dv 5196	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))) = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
38		elun2 4184	. . . . . . . 8 ⊢ (𝑣 ∈ 𝑉 → 𝑣 ∈ (𝐶 ∪ 𝑉))
39		simplr1 1234	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝐹:𝑅⟶𝑅)
40		simpr 490	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑣 ∈ (𝐶 ∪ 𝑉))
41	40	s1cld 14780	. . . . . . . . . 10 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ⟨“𝑣”⟩ ∈ Word (𝐶 ∪ 𝑉))
42	12	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝑅 = Word (𝐶 ∪ 𝑉))
43	41, 42	eleqtrrd 2867	. . . . . . . . 9 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ⟨“𝑣”⟩ ∈ 𝑅)
44	39, 43	ffvelcdmd 7112	. . . . . . . 8 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
45	38, 44	sylan2 605	. . . . . . 7 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘⟨“𝑣”⟩) ∈ 𝑅)
46	15	cbvmptv 5213	. . . . . . 7 ⊢ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) = (𝑣 ∈ 𝑉 ↦ (𝐹‘⟨“𝑣”⟩))
47	45, 46	fmptd 7141	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅)
48		ssid 3935	. . . . . 6 ⊢ 𝑉 ⊆ 𝑉
49		eqid 2763	. . . . . . 7 ⊢ (freeMnd‘(𝐶 ∪ 𝑉)) = (freeMnd‘(𝐶 ∪ 𝑉))
50	5, 4, 2, 1, 49	mrsubfval 36453	. . . . . 6 ⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
51	47, 48, 50	sylancl 598	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) = (𝑟 ∈ 𝑅 ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑟))))
52	5	fvexi 6925	. . . . . . . . 9 ⊢ 𝐶 ∈ V
53	4	fvexi 6925	. . . . . . . . 9 ⊢ 𝑉 ∈ V
54	52, 53	unex 7788	. . . . . . . 8 ⊢ (𝐶 ∪ 𝑉) ∈ V
55	49	frmdmnd 19087	. . . . . . . 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 2866	. . . . . . 7 ⊢ (((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → (𝐹‘⟨“𝑣”⟩) ∈ Word (𝐶 ∪ 𝑉))
60	59	fmpttd 7142	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
61		simpr1 1213	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹:𝑅⟶𝑅)
62	13, 13	feq23d 6729	. . . . . . . 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 2866	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ Word (𝐶 ∪ 𝑉))
69		simprr 785	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ 𝑅)
70	69, 67	eleqtrd 2866	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ Word (𝐶 ∪ 𝑉))
71		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉)))
72	49, 71	frmdbas 19080	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∪ 𝑉) ∈ V → (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉))
73	54, 72	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉)
74	73	eqcomi 2772	. . . . . . . . . . . . . . 15 ⊢ Word (𝐶 ∪ 𝑉) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉)))
75		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (+_g‘(freeMnd‘(𝐶 ∪ 𝑉))) = (+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))
76	49, 74, 75	frmdadd 19083	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Word (𝐶 ∪ 𝑉) ∧ 𝑦 ∈ Word (𝐶 ∪ 𝑉)) → (𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦))
77	68, 70, 76	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦) = (𝑥 ++ 𝑦))
78	77	fveq2d 6915	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = (𝐹‘(𝑥 ++ 𝑦)))
79		ffvelcdm 7108	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑥 ∈ 𝑅) → (𝐹‘𝑥) ∈ 𝑅)
80	79	ad2ant2lr 761	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ 𝑅)
81	80, 67	eleqtrd 2866	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉))
82		ffvelcdm 7108	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑅⟶𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹‘𝑦) ∈ 𝑅)
83	82	ad2ant2l 759	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ 𝑅)
84	83, 67	eleqtrd 2866	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉))
85	49, 74, 75	frmdadd 19083	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘𝑦) ∈ Word (𝐶 ∪ 𝑉)) → ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
86	81, 84, 85	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))
87	78, 86	eqeq12d 2779	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
88	87	2ralbidva 3228	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))))
89	66	raleqdv 3323	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ 𝐹:𝑅⟶𝑅) → (∀𝑦 ∈ 𝑅 (𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦)) ↔ ∀𝑦 ∈ Word (𝐶 ∪ 𝑉)(𝐹‘(𝑥(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))𝑦)) = ((𝐹‘𝑥)(+_g‘(freeMnd‘(𝐶 ∪ 𝑉)))(𝐹‘𝑦))))
90	66, 89	raleqbidv 3338	. . . . . . . . . 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 14714	. . . . . . . . . . . 12 ⊢ ∅ ∈ Word (𝐶 ∪ 𝑉)
95		ffvelcdm 7108	. . . . . . . . . . . 12 ⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ ∅ ∈ Word (𝐶 ∪ 𝑉)) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉))
96	63, 94, 95	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉))
97		lencl 14708	. . . . . . . . . . 11 ⊢ ((𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉) → (♯‘(𝐹‘∅)) ∈ ℕ₀)
98	96, 97	syl 18	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℕ₀)
99	98	nn0cnd 12699	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) ∈ ℂ)
100		0cnd 11329	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 0 ∈ ℂ)
101	99	addridd 11540	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + 0) = (♯‘(𝐹‘∅)))
102	94, 13	eleqtrrid 2871	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ∅ ∈ 𝑅)
103		fvoveq1 7469	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (𝐹‘(𝑥 ++ 𝑦)) = (𝐹‘(∅ ++ 𝑦)))
104		fveq2 6911	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → (𝐹‘𝑥) = (𝐹‘∅))
105	104	oveq1d 7461	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → ((𝐹‘𝑥) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)))
106	103, 105	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → ((𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)) ↔ (𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦))))
107		oveq2 7454	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (∅ ++ 𝑦) = (∅ ++ ∅))
108		ccatidid 14767	. . . . . . . . . . . . . . . 16 ⊢ (∅ ++ ∅) = ∅
109	107, 108	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (∅ ++ 𝑦) = ∅)
110	109	fveq2d 6915	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → (𝐹‘(∅ ++ 𝑦)) = (𝐹‘∅))
111		fveq2 6911	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (𝐹‘𝑦) = (𝐹‘∅))
112	111	oveq2d 7462	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ((𝐹‘∅) ++ (𝐹‘𝑦)) = ((𝐹‘∅) ++ (𝐹‘∅)))
113	110, 112	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → ((𝐹‘(∅ ++ 𝑦)) = ((𝐹‘∅) ++ (𝐹‘𝑦)) ↔ (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅))))
114	106, 113	rspc2va 3591	. . . . . . . . . . . 12 ⊢ (((∅ ∈ 𝑅 ∧ ∅ ∈ 𝑅) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
115	102, 102, 64, 114	syl21anc 851	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹‘∅) = ((𝐹‘∅) ++ (𝐹‘∅)))
116	115	fveq2d 6915	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = (♯‘((𝐹‘∅) ++ (𝐹‘∅))))
117		ccatlen 14750	. . . . . . . . . . 11 ⊢ (((𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉) ∧ (𝐹‘∅) ∈ Word (𝐶 ∪ 𝑉)) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
118	96, 96, 117	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘((𝐹‘∅) ++ (𝐹‘∅))) = ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))))
119	101, 116, 118	3eqtrrd 2803	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → ((♯‘(𝐹‘∅)) + (♯‘(𝐹‘∅))) = ((♯‘(𝐹‘∅)) + 0))
120	99, 99, 100, 119	addcanad 11545	. . . . . . . 8 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (♯‘(𝐹‘∅)) = 0)
121		fvex 6924	. . . . . . . . 9 ⊢ (𝐹‘∅) ∈ V
122		hasheq0 14537	. . . . . . . . 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 19088	. . . . . . . . 9 ⊢ ∅ = (0_g‘(freeMnd‘(𝐶 ∪ 𝑉)))
127	74, 74, 75, 75, 126, 126	ismhm 19012	. . . . . . . 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 2763	. . . . . . . . . 10 ⊢ (var_FMnd‘(𝐶 ∪ 𝑉)) = (var_FMnd‘(𝐶 ∪ 𝑉))
131	130	vrmdf 19086	. . . . . . . . 9 ⊢ ((𝐶 ∪ 𝑉) ∈ V → (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉))
132	54, 131	ax-mp 5	. . . . . . . 8 ⊢ (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)
133		fcompt 7161	. . . . . . . 8 ⊢ ((𝐹:Word (𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉) ∧ (var_FMnd‘(𝐶 ∪ 𝑉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))))
134	63, 132, 133	sylancl 598	. . . . . . 7 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))))
135	130	vrmdval 19085	. . . . . . . . . 10 ⊢ (((𝐶 ∪ 𝑉) ∈ V ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → ((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣) = ⟨“𝑣”⟩)
136	54, 135	mpan 703	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) → ((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣) = ⟨“𝑣”⟩)
137	136	fveq2d 6915	. . . . . . . 8 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) → (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣)) = (𝐹‘⟨“𝑣”⟩))
138	137	mpteq2ia 5204	. . . . . . 7 ⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘((var_FMnd‘(𝐶 ∪ 𝑉))‘𝑣))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩))
139	134, 138	eqtrdi 2814	. . . . . 6 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))
140	49, 74, 130	frmdup3lem 19094	. . . . . 6 ⊢ ((((freeMnd‘(𝐶 ∪ 𝑉)) ∈ Mnd ∧ (𝐶 ∪ 𝑉) ∈ V ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) ∧ (𝐹 ∈ ((freeMnd‘(𝐶 ∪ 𝑉)) MndHom (freeMnd‘(𝐶 ∪ 𝑉))) ∧ (𝐹 ∘ (var_FMnd‘(𝐶 ∪ 𝑉))) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
141	57, 58, 60, 129, 139, 140	syl32anc 1406	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑟 ∈ Word (𝐶 ∪ 𝑉) ↦ ((freeMnd‘(𝐶 ∪ 𝑉)) Σ_g ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ (𝐹‘⟨“𝑣”⟩)) ∘ 𝑟))))
142	37, 51, 141	3eqtr4rd 2809	. . . 4 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝐹 = (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))))
143	4, 2, 1	mrsubff 36457	. . . . . . 7 ⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑_pm 𝑉)⟶(𝑅 ↑_m 𝑅))
144	143	ffnd 6735	. . . . . 6 ⊢ (𝑇 ∈ 𝑊 → 𝑆 Fn (𝑅 ↑_pm 𝑉))
145	144	adantr 486	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → 𝑆 Fn (𝑅 ↑_pm 𝑉))
146	2	fvexi 6925	. . . . . . 7 ⊢ 𝑅 ∈ V
147		elpm2r 8896	. . . . . . 7 ⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ ((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉)) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
148	146, 53, 147	mpanl12 715	. . . . . 6 ⊢ (((𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
149	47, 48, 148	sylancl 598	. . . . 5 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉))
150		fnfvelrn 7107	. . . . 5 ⊢ ((𝑆 Fn (𝑅 ↑_pm 𝑉) ∧ (𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩)) ∈ (𝑅 ↑_pm 𝑉)) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
151	145, 149, 150	syl2anc 596	. . . 4 ⊢ ((𝑇 ∈ 𝑊 ∧ (𝐹:𝑅⟶𝑅 ∧ ∀𝑐 ∈ (𝐶 ∖ 𝑉)(𝐹‘⟨“𝑐”⟩) = ⟨“𝑐”⟩ ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝐹‘(𝑥 ++ 𝑦)) = ((𝐹‘𝑥) ++ (𝐹‘𝑦)))) → (𝑆‘(𝑤 ∈ 𝑉 ↦ (𝐹‘⟨“𝑤”⟩))) ∈ ran 𝑆)
152	142, 151	eqeltrd 2864	. . 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 2147 ∀wral 3080 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∪ cun 4152 ∅c0 4281 ifcif 4485 ↦ cmpt 5190 ran crn 5657 ∘ ccom 5660 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 (class class class)co 7446 ↑_m cmap 8878 ↑_pm cpm 8879 0cc0 11230 + caddc 11233 ℕ₀cn0 12636 ♯chash 14504 Word cword 14688 ++ cconcat 14745 ⟨“cs1 14772 Basecbs 17419 +_gcplusg 17460 Σ_g cgsu 17643 Mndcmnd 18955 MndHom cmhm 19008 freeMndcfrmd 19075 var_FMndcvrmd 19076 mCNcmcn 36405 mVRcmvar 36406 mRExcmrex 36411 mRSubstcmrsub 36415

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-er 8748 df-map 8880 df-pm 8881 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-card 10050 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-nn 12366 df-2 12435 df-n0 12637 df-xnn0 12710 df-z 12724 df-uz 12996 df-fz 13670 df-fzo 13819 df-seq 14175 df-hash 14505 df-word 14689 df-lsw 14738 df-concat 14746 df-s1 14773 df-substr 14820 df-pfx 14852 df-struct 17357 df-sets 17374 df-slot 17392 df-ndx 17404 df-base 17420 df-ress 17441 df-plusg 17473 df-0g 17644 df-gsum 17645 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-mhm 19010 df-submnd 19011 df-frmd 19077 df-vrmd 19078 df-mrex 36431 df-mrsub 36435

This theorem is used by: mrsubco 36466

W3C validator