Theorem evlsscaval

Description: Polynomial evaluation builder for a scalar. Compare evl1scad . Note that scalar multiplication by X is the same as vector multiplication by ( AX ) by asclmul1 . (Contributed by SN, 27-Jul-2024)

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

Proof

Step	Hyp	Ref	Expression
1		evlsscaval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsscaval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3		evlsscaval.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		evlsscaval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
5		evlsscaval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
6		evlsscaval.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
7		evlsscaval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
8		evlsscaval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
9		evlsscaval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10		evlsscaval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
11		evlsscaval.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐾 ↑m 𝐼 ) )
12		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
13	3	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
14	9 13	syl	⊢ ( 𝜑 → 𝑈 ∈ Ring )
15	2 5 12 6 7 14	mplasclf	⊢ ( 𝜑 → 𝐴 : ( Base ‘ 𝑈 ) ⟶ 𝐵 )
16	3	subrgbas	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
17	9 16	syl	⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
18	10 17	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑈 ) )
19	15 18	ffvelrnd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 )
20	1 2 3 4 6 7 8 9 10	evlssca	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐾 ↑m 𝐼 ) × { 𝑋 } ) )
21	20	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐿 ) = ( ( ( 𝐾 ↑m 𝐼 ) × { 𝑋 } ) ‘ 𝐿 ) )
22		fvconst2g	⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝐿 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( ( 𝐾 ↑m 𝐼 ) × { 𝑋 } ) ‘ 𝐿 ) = 𝑋 )
23	10 11 22	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐾 ↑m 𝐼 ) × { 𝑋 } ) ‘ 𝐿 ) = 𝑋 )
24	21 23	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐿 ) = 𝑋 )
25	19 24	jca	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐿 ) = 𝑋 ) )