mrsubfval

Description: The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrsubffval.c	$⊢ C = mCN (T)$
	mrsubffval.v	$⊢ V = mVR (T)$
	mrsubffval.r	$⊢ R = mREx (T)$
	mrsubffval.s	$⊢ S = mRSubst (T)$
	mrsubffval.g	$⊢ G = freeMnd (C \cup V)$
Assertion	mrsubfval	$⊢ (F : A ⟶ R \land A \subseteq V) \to S (F) = (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e))$

Proof

Step	Hyp	Ref	Expression
1		mrsubffval.c	$⊢ C = mCN (T)$
2		mrsubffval.v	$⊢ V = mVR (T)$
3		mrsubffval.r	$⊢ R = mREx (T)$
4		mrsubffval.s	$⊢ S = mRSubst (T)$
5		mrsubffval.g	$⊢ G = freeMnd (C \cup V)$
6	1 2 3 4 5	mrsubffval	$⊢ T \in V \to S = (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e)))$
7	6	adantr	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to S = (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e)))$
8		dmeq	$⊢ f = F \to dom f = dom F$
9		fdm	$⊢ F : A ⟶ R \to dom F = A$
10	9	ad2antrl	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to dom F = A$
11	8 10	sylan9eqr	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to dom f = A$
12	11	eleq2d	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to (v \in dom f \leftrightarrow v \in A)$
13		simpr	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to f = F$
14	13	fveq1d	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to f (v) = F (v)$
15	12 14	ifbieq1d	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to if (v \in dom f, f (v), ⟨“ v ”⟩) = if (v \in A, F (v), ⟨“ v ”⟩)$
16	15	mpteq2dv	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to (v \in (C \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) = (v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩))$
17	16	coeq1d	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to (v \in (C \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e = (v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e$
18	17	oveq2d	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to \sum_{G} ((v \in (C \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e) = \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e)$
19	18	mpteq2dv	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e)) = (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e))$
20	3	fvexi	$⊢ R \in V$
21	20	a1i	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to R \in V$
22	2	fvexi	$⊢ V \in V$
23	22	a1i	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to V \in V$
24		simprl	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to F : A ⟶ R$
25		simprr	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to A \subseteq V$
26		elpm2r	$⊢ ((R \in V \land V \in V) \land (F : A ⟶ R \land A \subseteq V)) \to F \in (R ↑_{𝑝𝑚} V)$
27	21 23 24 25 26	syl22anc	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to F \in (R ↑_{𝑝𝑚} V)$
28	20	mptex	$⊢ (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e)) \in V$
29	28	a1i	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e)) \in V$
30	7 19 27 29	fvmptd	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to S (F) = (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e))$
31	30	ex	$⊢ T \in V \to ((F : A ⟶ R \land A \subseteq V) \to S (F) = (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e)))$
32		0fv	$⊢ \emptyset (F) = \emptyset$
33		fvprc	$⊢ \neg T \in V \to mRSubst (T) = \emptyset$
34	4 33	eqtrid	$⊢ \neg T \in V \to S = \emptyset$
35	34	fveq1d	$⊢ \neg T \in V \to S (F) = \emptyset (F)$
36		fvprc	$⊢ \neg T \in V \to mREx (T) = \emptyset$
37	3 36	eqtrid	$⊢ \neg T \in V \to R = \emptyset$
38	37	mpteq1d	$⊢ \neg T \in V \to (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e)) = (e \in \emptyset ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e))$
39		mpt0	$⊢ (e \in \emptyset ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e)) = \emptyset$
40	38 39	eqtrdi	$⊢ \neg T \in V \to (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e)) = \emptyset$
41	32 35 40	3eqtr4a	$⊢ \neg T \in V \to S (F) = (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e))$
42	41	a1d	$⊢ \neg T \in V \to ((F : A ⟶ R \land A \subseteq V) \to S (F) = (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e)))$
43	31 42	pm2.61i	$⊢ (F : A ⟶ R \land A \subseteq V) \to S (F) = (e \in R ⟼ \sum_{G} ((v \in (C \cup V) ⟼ if (v \in A, F (v), ⟨“ v ”⟩)) \circ e))$

Metamath Proof Explorer

Theorem mrsubfval

Proof