mrsubcn

Description: A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrsubccat.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
	mrsubccat.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	mrsubcn.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mrsubcn.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
Assertion	mrsubcn	⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ) → ( 𝐹 ‘ ⟨“ 𝑋 ”⟩ ) = ⟨“ 𝑋 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		mrsubccat.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
2		mrsubccat.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
3		mrsubcn.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
4		mrsubcn.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
5		n0i	⊢ ( 𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅ )
6	1	rnfvprc	⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 = ∅ )
7	5 6	nsyl2	⊢ ( 𝐹 ∈ ran 𝑆 → 𝑇 ∈ V )
8	3 2 1	mrsubff	⊢ ( 𝑇 ∈ V → 𝑆 : ( 𝑅 ↑_pm 𝑉 ) ⟶ ( 𝑅 ↑_m 𝑅 ) )
9		ffun	⊢ ( 𝑆 : ( 𝑅 ↑_pm 𝑉 ) ⟶ ( 𝑅 ↑_m 𝑅 ) → Fun 𝑆 )
10	7 8 9	3syl	⊢ ( 𝐹 ∈ ran 𝑆 → Fun 𝑆 )
11	3 2 1	mrsubrn	⊢ ran 𝑆 = ( 𝑆 “ ( 𝑅 ↑_m 𝑉 ) )
12	11	eleq2i	⊢ ( 𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ( 𝑆 “ ( 𝑅 ↑_m 𝑉 ) ) )
13	12	biimpi	⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 ∈ ( 𝑆 “ ( 𝑅 ↑_m 𝑉 ) ) )
14		fvelima	⊢ ( ( Fun 𝑆 ∧ 𝐹 ∈ ( 𝑆 “ ( 𝑅 ↑_m 𝑉 ) ) ) → ∃ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ( 𝑆 ‘ 𝑓 ) = 𝐹 )
15	10 13 14	syl2anc	⊢ ( 𝐹 ∈ ran 𝑆 → ∃ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ( 𝑆 ‘ 𝑓 ) = 𝐹 )
16		elmapi	⊢ ( 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) → 𝑓 : 𝑉 ⟶ 𝑅 )
17	16	adantl	⊢ ( ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ∧ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ) → 𝑓 : 𝑉 ⟶ 𝑅 )
18		ssidd	⊢ ( ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ∧ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ) → 𝑉 ⊆ 𝑉 )
19		eldifi	⊢ ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) → 𝑋 ∈ 𝐶 )
20		elun1	⊢ ( 𝑋 ∈ 𝐶 → 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) )
21	19 20	syl	⊢ ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) → 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) )
22	21	adantr	⊢ ( ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ∧ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ) → 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) )
23	4 3 2 1	mrsubcv	⊢ ( ( 𝑓 : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨“ 𝑋 ”⟩ ) = if ( 𝑋 ∈ 𝑉 , ( 𝑓 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )
24	17 18 22 23	syl3anc	⊢ ( ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ∧ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨“ 𝑋 ”⟩ ) = if ( 𝑋 ∈ 𝑉 , ( 𝑓 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )
25		eldifn	⊢ ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) → ¬ 𝑋 ∈ 𝑉 )
26	25	adantr	⊢ ( ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ∧ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ) → ¬ 𝑋 ∈ 𝑉 )
27	26	iffalsed	⊢ ( ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ∧ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ) → if ( 𝑋 ∈ 𝑉 , ( 𝑓 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) = ⟨“ 𝑋 ”⟩ )
28	24 27	eqtrd	⊢ ( ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ∧ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨“ 𝑋 ”⟩ ) = ⟨“ 𝑋 ”⟩ )
29		fveq1	⊢ ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨“ 𝑋 ”⟩ ) = ( 𝐹 ‘ ⟨“ 𝑋 ”⟩ ) )
30	29	eqeq1d	⊢ ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨“ 𝑋 ”⟩ ) = ⟨“ 𝑋 ”⟩ ↔ ( 𝐹 ‘ ⟨“ 𝑋 ”⟩ ) = ⟨“ 𝑋 ”⟩ ) )
31	28 30	syl5ibcom	⊢ ( ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ∧ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ) → ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( 𝐹 ‘ ⟨“ 𝑋 ”⟩ ) = ⟨“ 𝑋 ”⟩ ) )
32	31	rexlimdva	⊢ ( 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) → ( ∃ 𝑓 ∈ ( 𝑅 ↑_m 𝑉 ) ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( 𝐹 ‘ ⟨“ 𝑋 ”⟩ ) = ⟨“ 𝑋 ”⟩ ) )
33	15 32	mpan9	⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ ( 𝐶 ∖ 𝑉 ) ) → ( 𝐹 ‘ ⟨“ 𝑋 ”⟩ ) = ⟨“ 𝑋 ”⟩ )

Metamath Proof Explorer

Theorem mrsubcn

Proof