mrsubrn

Description: Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrsubvr.v	$⊢ V = mVR (T)$
	mrsubvr.r	$⊢ R = mREx (T)$
	mrsubvr.s	$⊢ S = mRSubst (T)$
Assertion	mrsubrn	$⊢ ran S = S [R^{V}]$

Proof

Step	Hyp	Ref	Expression
1		mrsubvr.v	$⊢ V = mVR (T)$
2		mrsubvr.r	$⊢ R = mREx (T)$
3		mrsubvr.s	$⊢ S = mRSubst (T)$
4	1 2 3	mrsubff	$⊢ T \in V \to S : R ↑_{𝑝𝑚} V ⟶ R^{R}$
5	4	ffnd	$⊢ T \in V \to S Fn (R ↑_{𝑝𝑚} V)$
6		eleq1w	$⊢ x = v \to (x \in dom f \leftrightarrow v \in dom f)$
7		fveq2	$⊢ x = v \to f (x) = f (v)$
8		s1eq	$⊢ x = v \to ⟨“ x ”⟩ = ⟨“ v ”⟩$
9	6 7 8	ifbieq12d	$⊢ x = v \to if (x \in dom f, f (x), ⟨“ x ”⟩) = if (v \in dom f, f (v), ⟨“ v ”⟩)$
10		eqid	$⊢ (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) = (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩))$
11		fvex	$⊢ f (v) \in V$
12		s1cli	$⊢ ⟨“ v ”⟩ \in Word V$
13	12	elexi	$⊢ ⟨“ v ”⟩ \in V$
14	11 13	ifex	$⊢ if (v \in dom f, f (v), ⟨“ v ”⟩) \in V$
15	9 10 14	fvmpt	$⊢ v \in V \to (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v) = if (v \in dom f, f (v), ⟨“ v ”⟩)$
16	15	adantl	$⊢ ((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land v \in V) \to (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v) = if (v \in dom f, f (v), ⟨“ v ”⟩)$
17	16	ifeq1da	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to if (v \in V, (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v), ⟨“ v ”⟩) = if (v \in V, if (v \in dom f, f (v), ⟨“ v ”⟩), ⟨“ v ”⟩)$
18		ifan	$⊢ if ((v \in V \land v \in dom f), f (v), ⟨“ v ”⟩) = if (v \in V, if (v \in dom f, f (v), ⟨“ v ”⟩), ⟨“ v ”⟩)$
19	17 18	syl6eqr	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to if (v \in V, (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v), ⟨“ v ”⟩) = if ((v \in V \land v \in dom f), f (v), ⟨“ v ”⟩)$
20		elpmi	$⊢ f \in (R ↑_{𝑝𝑚} V) \to (f : dom f ⟶ R \land dom f \subseteq V)$
21	20	adantl	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (f : dom f ⟶ R \land dom f \subseteq V)$
22	21	simprd	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to dom f \subseteq V$
23	22	sseld	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (v \in dom f \to v \in V)$
24	23	pm4.71rd	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (v \in dom f \leftrightarrow (v \in V \land v \in dom f))$
25	24	bicomd	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to ((v \in V \land v \in dom f) \leftrightarrow v \in dom f)$
26	25	ifbid	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to if ((v \in V \land v \in dom f), f (v), ⟨“ v ”⟩) = if (v \in dom f, f (v), ⟨“ v ”⟩)$
27	19 26	eqtr2d	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to if (v \in dom f, f (v), ⟨“ v ”⟩) = if (v \in V, (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v), ⟨“ v ”⟩)$
28	27	mpteq2dv	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (v \in (mCN (T) \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) = (v \in (mCN (T) \cup V) ⟼ if (v \in V, (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v), ⟨“ v ”⟩))$
29	28	coeq1d	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (v \in (mCN (T) \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e = (v \in (mCN (T) \cup V) ⟼ if (v \in V, (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v), ⟨“ v ”⟩)) \circ e$
30	29	oveq2d	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to \sum_{freeMnd (mCN (T) \cup V)} ((v \in (mCN (T) \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e) = \sum_{freeMnd (mCN (T) \cup V)} ((v \in (mCN (T) \cup V) ⟼ if (v \in V, (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v), ⟨“ v ”⟩)) \circ e)$
31	30	mpteq2dv	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (e \in R ⟼ \sum_{freeMnd (mCN (T) \cup V)} ((v \in (mCN (T) \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e)) = (e \in R ⟼ \sum_{freeMnd (mCN (T) \cup V)} ((v \in (mCN (T) \cup V) ⟼ if (v \in V, (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v), ⟨“ v ”⟩)) \circ e))$
32		eqid	$⊢ mCN (T) = mCN (T)$
33		eqid	$⊢ freeMnd (mCN (T) \cup V) = freeMnd (mCN (T) \cup V)$
34	32 1 2 3 33	mrsubfval	$⊢ (f : dom f ⟶ R \land dom f \subseteq V) \to S (f) = (e \in R ⟼ \sum_{freeMnd (mCN (T) \cup V)} ((v \in (mCN (T) \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e))$
35	21 34	syl	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to S (f) = (e \in R ⟼ \sum_{freeMnd (mCN (T) \cup V)} ((v \in (mCN (T) \cup V) ⟼ if (v \in dom f, f (v), ⟨“ v ”⟩)) \circ e))$
36	21	simpld	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to f : dom f ⟶ R$
37	36	adantr	$⊢ ((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land x \in V) \to f : dom f ⟶ R$
38	37	ffvelrnda	$⊢ (((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land x \in V) \land x \in dom f) \to f (x) \in R$
39		elun2	$⊢ x \in V \to x \in (mCN (T) \cup V)$
40	39	ad2antlr	$⊢ (((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land x \in V) \land \neg x \in dom f) \to x \in (mCN (T) \cup V)$
41	40	s1cld	$⊢ (((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land x \in V) \land \neg x \in dom f) \to ⟨“ x ”⟩ \in Word (mCN (T) \cup V)$
42	32 1 2	mrexval	$⊢ T \in V \to R = Word (mCN (T) \cup V)$
43	42	ad3antrrr	$⊢ (((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land x \in V) \land \neg x \in dom f) \to R = Word (mCN (T) \cup V)$
44	41 43	eleqtrrd	$⊢ (((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land x \in V) \land \neg x \in dom f) \to ⟨“ x ”⟩ \in R$
45	38 44	ifclda	$⊢ ((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land x \in V) \to if (x \in dom f, f (x), ⟨“ x ”⟩) \in R$
46	45	fmpttd	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) : V ⟶ R$
47		ssid	$⊢ V \subseteq V$
48	32 1 2 3 33	mrsubfval	$⊢ ((x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) : V ⟶ R \land V \subseteq V) \to S ((x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩))) = (e \in R ⟼ \sum_{freeMnd (mCN (T) \cup V)} ((v \in (mCN (T) \cup V) ⟼ if (v \in V, (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v), ⟨“ v ”⟩)) \circ e))$
49	46 47 48	sylancl	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to S ((x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩))) = (e \in R ⟼ \sum_{freeMnd (mCN (T) \cup V)} ((v \in (mCN (T) \cup V) ⟼ if (v \in V, (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) (v), ⟨“ v ”⟩)) \circ e))$
50	31 35 49	3eqtr4d	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to S (f) = S ((x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)))$
51	5	adantr	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to S Fn (R ↑_{𝑝𝑚} V)$
52		mapsspm	$⊢ R^{V} \subseteq R ↑_{𝑝𝑚} V$
53	52	a1i	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to R^{V} \subseteq R ↑_{𝑝𝑚} V$
54	2	fvexi	$⊢ R \in V$
55	1	fvexi	$⊢ V \in V$
56	54 55	elmap	$⊢ (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) \in (R^{V}) \leftrightarrow (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) : V ⟶ R$
57	46 56	sylibr	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) \in (R^{V})$
58		fnfvima	$⊢ (S Fn (R ↑_{𝑝𝑚} V) \land R^{V} \subseteq R ↑_{𝑝𝑚} V \land (x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩)) \in (R^{V})) \to S ((x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩))) \in S [R^{V}]$
59	51 53 57 58	syl3anc	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to S ((x \in V ⟼ if (x \in dom f, f (x), ⟨“ x ”⟩))) \in S [R^{V}]$
60	50 59	eqeltrd	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to S (f) \in S [R^{V}]$
61	60	ralrimiva	$⊢ T \in V \to \forall f \in (R ↑_{𝑝𝑚} V) S (f) \in S [R^{V}]$
62		ffnfv	$⊢ S : R ↑_{𝑝𝑚} V ⟶ S [R^{V}] \leftrightarrow (S Fn (R ↑_{𝑝𝑚} V) \land \forall f \in (R ↑_{𝑝𝑚} V) S (f) \in S [R^{V}])$
63	5 61 62	sylanbrc	$⊢ T \in V \to S : R ↑_{𝑝𝑚} V ⟶ S [R^{V}]$
64	63	frnd	$⊢ T \in V \to ran S \subseteq S [R^{V}]$
65	3	rnfvprc	$⊢ \neg T \in V \to ran S = \emptyset$
66		0ss	$⊢ \emptyset \subseteq S [R^{V}]$
67	65 66	eqsstrdi	$⊢ \neg T \in V \to ran S \subseteq S [R^{V}]$
68	64 67	pm2.61i	$⊢ ran S \subseteq S [R^{V}]$
69		imassrn	$⊢ S [R^{V}] \subseteq ran S$
70	68 69	eqssi	$⊢ ran S = S [R^{V}]$

Metamath Proof Explorer

Theorem mrsubrn

Proof