elmrsubrn

Description: Characterization of the substitutions as functions from expressions to expressions that distribute under concatenation and map constants to themselves. (The constant part uses ( C \ V ) because we don't know that C and V are disjoint until we get to ismfs .) (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrsubccat.s	$⊢ S = mRSubst (T)$
	mrsubccat.r	$⊢ R = mREx (T)$
	mrsubcn.v	$⊢ V = mVR (T)$
	mrsubcn.c	$⊢ C = mCN (T)$
Assertion	elmrsubrn	$⊢ T \in W \to (F \in ran S \leftrightarrow (F : R ⟶ R \land \forall c \in (C ∖ V) F (⟨“ c ”⟩) = ⟨“ c ”⟩ \land \forall x \in R \forall y \in R F (x ++ y) = F (x) ++ F (y)))$

Proof

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

Metamath Proof Explorer

Theorem elmrsubrn

Proof