This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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