Theorem evlsvarval

Description: Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024)

	Ref	Expression
Hypotheses	evlsvarval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsvarval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
	evlsvarval.v	⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
	evlsvarval.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlsvarval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evlsvarval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlsvarval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	evlsvarval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsvarval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsvarval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	evlsvarval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion	evlsvarval	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsvarval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsvarval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3		evlsvarval.v	⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
4		evlsvarval.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5		evlsvarval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6		evlsvarval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
7		evlsvarval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
8		evlsvarval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
9		evlsvarval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10		evlsvarval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
11		evlsvarval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
12	4	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
13	9 12	syl	⊢ ( 𝜑 → 𝑈 ∈ Ring )
14	2 3 6 7 13 10	mvrcl	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )
15		fveq1	⊢ ( 𝑔 = 𝐴 → ( 𝑔 ‘ 𝑋 ) = ( 𝐴 ‘ 𝑋 ) )
16	1 3 4 5 7 8 9 10	evlsvar	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
17		fvexd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ V )
18	15 16 11 17	fvmptd4	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) )
19	14 18	jca	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) ) )