Theorem evlsca

Description: Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019)

	Ref	Expression
Hypotheses	evlsca.q	⊢ 𝑄 = ( 𝐼 eval 𝑆 )
	evlsca.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
	evlsca.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evlsca.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	evlsca.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlsca.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsca.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	evlsca	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		evlsca.q	⊢ 𝑄 = ( 𝐼 eval 𝑆 )
2		evlsca.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
3		evlsca.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		evlsca.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
5		evlsca.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		evlsca.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
7		evlsca.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		eqid	⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
9		eqid	⊢ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) )
10		eqid	⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
11		eqid	⊢ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) )
12		crngring	⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
13	3	subrgid	⊢ ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
14	6 12 13	3syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
15	8 1 9 10 2 3 11 4 5 6 14 7	evlsscasrng	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) = ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) )
16	8 9 10 3 11 5 6 14 7	evlssca	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
17	15 16	eqtr3d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )