Theorem evlscaval

Description: Polynomial evaluation for scalars. See evlsscaval . (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	evlscafv.1	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
	evlscafv.2	⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
	evlscafv.3	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evlscafv.4	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	evlscafv.5	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlscafv.6	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evlscafv.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	evlscafv.8	⊢ ( 𝜑 → 𝐿 : 𝐼 ⟶ 𝐵 )
Assertion	evlscaval	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐿 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		evlscafv.1	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
2		evlscafv.2	⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
3		evlscafv.3	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		evlscafv.4	⊢ 𝐴 = ( algSc ‘ 𝑊 )
5		evlscafv.5	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		evlscafv.6	⊢ ( 𝜑 → 𝑅 ∈ CRing )
7		evlscafv.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		evlscafv.8	⊢ ( 𝜑 → 𝐿 : 𝐼 ⟶ 𝐵 )
9	1 2 3 4 5 6 7	evlsca	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
10	9	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐿 ) = ( ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ‘ 𝐿 ) )
11	3	fvexi	⊢ 𝐵 ∈ V
12	11	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
13	12 5 8	elmapdd	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐵 ↑m 𝐼 ) )
14		fvconst2g	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐿 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ‘ 𝐿 ) = 𝑋 )
15	7 13 14	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ‘ 𝐿 ) = 𝑋 )
16	10 15	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐿 ) = 𝑋 )