Theorem evls1scafv

Description: Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025)

	Ref	Expression
Hypotheses	evls1scafv.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	evls1scafv.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
	evls1scafv.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evls1scafv.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evls1scafv.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	evls1scafv.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evls1scafv.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evls1scafv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
	evls1scafv.1	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion	evls1scafv	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐶 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		evls1scafv.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		evls1scafv.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
3		evls1scafv.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		evls1scafv.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		evls1scafv.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
6		evls1scafv.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
7		evls1scafv.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8		evls1scafv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
9		evls1scafv.1	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
10	1 2 3 4 5 6 7 8	evls1sca	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )
11	10	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐶 ) = ( ( 𝐵 × { 𝑋 } ) ‘ 𝐶 ) )
12		fvconst2g	⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐵 × { 𝑋 } ) ‘ 𝐶 ) = 𝑋 )
13	8 9 12	syl2anc	⊢ ( 𝜑 → ( ( 𝐵 × { 𝑋 } ) ‘ 𝐶 ) = 𝑋 )
14	11 13	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐶 ) = 𝑋 )