Theorem evlsvar

Description: Polynomial evaluation maps variables to projections. (Contributed by Stefan O'Rear, 12-Mar-2015) (Proof shortened by AV, 18-Sep-2021)

	Ref	Expression
Hypotheses	evlsvar.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsvar.v	⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
	evlsvar.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlsvar.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evlsvar.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	evlsvar.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsvar.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsvar.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion	evlsvar	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsvar.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsvar.v	⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
3		evlsvar.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		evlsvar.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		evlsvar.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		evlsvar.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
7		evlsvar.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8		evlsvar.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
9		eqid	⊢ ( 𝐼 mPoly 𝑈 ) = ( 𝐼 mPoly 𝑈 )
10		eqid	⊢ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
11		eqid	⊢ ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) = ( algSc ‘ ( 𝐼 mPoly 𝑈 ) )
12		eqid	⊢ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) )
13		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
14	1 9 2 3 10 4 11 12 13	evlsval2	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑄 ∈ ( ( 𝐼 mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) ∧ ( ( 𝑄 ∘ ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑄 ∘ 𝑉 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
15	5 6 7 14	syl3anc	⊢ ( 𝜑 → ( 𝑄 ∈ ( ( 𝐼 mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) ∧ ( ( 𝑄 ∘ ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑄 ∘ 𝑉 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
16	15	simprrd	⊢ ( 𝜑 → ( 𝑄 ∘ 𝑉 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) )
17	16	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ∘ 𝑉 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑋 ) )
18		eqid	⊢ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑈 ) )
19	3	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
20	7 19	syl	⊢ ( 𝜑 → 𝑈 ∈ Ring )
21	9 2 18 5 20	mvrf2	⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
22	21	ffnd	⊢ ( 𝜑 → 𝑉 Fn 𝐼 )
23		fvco2	⊢ ( ( 𝑉 Fn 𝐼 ∧ 𝑋 ∈ 𝐼 ) → ( ( 𝑄 ∘ 𝑉 ) ‘ 𝑋 ) = ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) )
24	22 8 23	syl2anc	⊢ ( 𝜑 → ( ( 𝑄 ∘ 𝑉 ) ‘ 𝑋 ) = ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) )
25		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑋 ) )
26	25	mpteq2dv	⊢ ( 𝑥 = 𝑋 → ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
27		ovex	⊢ ( 𝐵 ↑m 𝐼 ) ∈ V
28	27	mptex	⊢ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) ∈ V
29	26 13 28	fvmpt	⊢ ( 𝑋 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑋 ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
30	8 29	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑋 ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
31	17 24 30	3eqtr3d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )