mrsubcn

Description: A substitution does not change the value of constant substrings. (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	mrsubcn	$⊢ (F \in ran S \land X \in (C ∖ V)) \to F (⟨“ X ”⟩) = ⟨“ X ”⟩$

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		n0i	$⊢ F \in ran S \to \neg ran S = \emptyset$
6	1	rnfvprc	$⊢ \neg T \in V \to ran S = \emptyset$
7	5 6	nsyl2	$⊢ F \in ran S \to T \in V$
8	3 2 1	mrsubff	$⊢ T \in V \to S : R ↑_{𝑝𝑚} V ⟶ R^{R}$
9		ffun	$⊢ S : R ↑_{𝑝𝑚} V ⟶ R^{R} \to Fun S$
10	7 8 9	3syl	$⊢ F \in ran S \to Fun S$
11	3 2 1	mrsubrn	$⊢ ran S = S [R^{V}]$
12	11	eleq2i	$⊢ F \in ran S \leftrightarrow F \in S [R^{V}]$
13	12	biimpi	$⊢ F \in ran S \to F \in S [R^{V}]$
14		fvelima	$⊢ (Fun S \land F \in S [R^{V}]) \to \exists f \in (R^{V}) S (f) = F$
15	10 13 14	syl2anc	$⊢ F \in ran S \to \exists f \in (R^{V}) S (f) = F$
16		elmapi	$⊢ f \in (R^{V}) \to f : V ⟶ R$
17	16	adantl	$⊢ (X \in (C ∖ V) \land f \in (R^{V})) \to f : V ⟶ R$
18		ssidd	$⊢ (X \in (C ∖ V) \land f \in (R^{V})) \to V \subseteq V$
19		eldifi	$⊢ X \in (C ∖ V) \to X \in C$
20		elun1	$⊢ X \in C \to X \in (C \cup V)$
21	19 20	syl	$⊢ X \in (C ∖ V) \to X \in (C \cup V)$
22	21	adantr	$⊢ (X \in (C ∖ V) \land f \in (R^{V})) \to X \in (C \cup V)$
23	4 3 2 1	mrsubcv	$⊢ (f : V ⟶ R \land V \subseteq V \land X \in (C \cup V)) \to S (f) (⟨“ X ”⟩) = if (X \in V, f (X), ⟨“ X ”⟩)$
24	17 18 22 23	syl3anc	$⊢ (X \in (C ∖ V) \land f \in (R^{V})) \to S (f) (⟨“ X ”⟩) = if (X \in V, f (X), ⟨“ X ”⟩)$
25		eldifn	$⊢ X \in (C ∖ V) \to \neg X \in V$
26	25	adantr	$⊢ (X \in (C ∖ V) \land f \in (R^{V})) \to \neg X \in V$
27	26	iffalsed	$⊢ (X \in (C ∖ V) \land f \in (R^{V})) \to if (X \in V, f (X), ⟨“ X ”⟩) = ⟨“ X ”⟩$
28	24 27	eqtrd	$⊢ (X \in (C ∖ V) \land f \in (R^{V})) \to S (f) (⟨“ X ”⟩) = ⟨“ X ”⟩$
29		fveq1	$⊢ S (f) = F \to S (f) (⟨“ X ”⟩) = F (⟨“ X ”⟩)$
30	29	eqeq1d	$⊢ S (f) = F \to (S (f) (⟨“ X ”⟩) = ⟨“ X ”⟩ \leftrightarrow F (⟨“ X ”⟩) = ⟨“ X ”⟩)$
31	28 30	syl5ibcom	$⊢ (X \in (C ∖ V) \land f \in (R^{V})) \to (S (f) = F \to F (⟨“ X ”⟩) = ⟨“ X ”⟩)$
32	31	rexlimdva	$⊢ X \in (C ∖ V) \to (\exists f \in (R^{V}) S (f) = F \to F (⟨“ X ”⟩) = ⟨“ X ”⟩)$
33	15 32	mpan9	$⊢ (F \in ran S \land X \in (C ∖ V)) \to F (⟨“ X ”⟩) = ⟨“ X ”⟩$

Metamath Proof Explorer

Theorem mrsubcn

Proof