Metamath Proof Explorer


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 𝐼 ) × { 𝑋 } ) )