# Metamath Proof Explorer

## Theorem evl1sca

Description: Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1sca.o 𝑂 = ( eval1𝑅 )
evl1sca.p 𝑃 = ( Poly1𝑅 )
evl1sca.b 𝐵 = ( Base ‘ 𝑅 )
evl1sca.a 𝐴 = ( algSc ‘ 𝑃 )
Assertion evl1sca ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑂 ‘ ( 𝐴𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )

### Proof

Step Hyp Ref Expression
1 evl1sca.o 𝑂 = ( eval1𝑅 )
2 evl1sca.p 𝑃 = ( Poly1𝑅 )
3 evl1sca.b 𝐵 = ( Base ‘ 𝑅 )
4 evl1sca.a 𝐴 = ( algSc ‘ 𝑃 )
5 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6 5 adantr ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → 𝑅 ∈ Ring )
7 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8 2 4 3 7 ply1sclf ( 𝑅 ∈ Ring → 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑃 ) )
9 6 8 syl ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑃 ) )
10 ffvelrn ( ( 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑃 ) ∧ 𝑋𝐵 ) → ( 𝐴𝑋 ) ∈ ( Base ‘ 𝑃 ) )
11 9 10 sylancom ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝐴𝑋 ) ∈ ( Base ‘ 𝑃 ) )
12 eqid ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
13 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
14 eqid ( PwSer1𝑅 ) = ( PwSer1𝑅 )
15 2 14 7 ply1bas ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
16 1 12 3 13 15 evl1val ( ( 𝑅 ∈ CRing ∧ ( 𝐴𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑂 ‘ ( 𝐴𝑋 ) ) = ( ( ( 1o eval 𝑅 ) ‘ ( 𝐴𝑋 ) ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
17 11 16 syldan ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑂 ‘ ( 𝐴𝑋 ) ) = ( ( ( 1o eval 𝑅 ) ‘ ( 𝐴𝑋 ) ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
18 2 4 ply1ascl 𝐴 = ( algSc ‘ ( 1o mPoly 𝑅 ) )
19 3 ressid ( 𝑅 ∈ CRing → ( 𝑅s 𝐵 ) = 𝑅 )
20 19 adantr ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑅s 𝐵 ) = 𝑅 )
21 20 oveq2d ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 1o mPoly ( 𝑅s 𝐵 ) ) = ( 1o mPoly 𝑅 ) )
22 21 fveq2d ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( algSc ‘ ( 1o mPoly ( 𝑅s 𝐵 ) ) ) = ( algSc ‘ ( 1o mPoly 𝑅 ) ) )
23 18 22 eqtr4id ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → 𝐴 = ( algSc ‘ ( 1o mPoly ( 𝑅s 𝐵 ) ) ) )
24 23 fveq1d ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝐴𝑋 ) = ( ( algSc ‘ ( 1o mPoly ( 𝑅s 𝐵 ) ) ) ‘ 𝑋 ) )
25 24 fveq2d ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( 𝐴𝑋 ) ) = ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly ( 𝑅s 𝐵 ) ) ) ‘ 𝑋 ) ) )
26 12 3 evlval ( 1o eval 𝑅 ) = ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
27 eqid ( 1o mPoly ( 𝑅s 𝐵 ) ) = ( 1o mPoly ( 𝑅s 𝐵 ) )
28 eqid ( 𝑅s 𝐵 ) = ( 𝑅s 𝐵 )
29 eqid ( algSc ‘ ( 1o mPoly ( 𝑅s 𝐵 ) ) ) = ( algSc ‘ ( 1o mPoly ( 𝑅s 𝐵 ) ) )
30 1on 1o ∈ On
31 30 a1i ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → 1o ∈ On )
32 simpl ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → 𝑅 ∈ CRing )
33 3 subrgid ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
34 6 33 syl ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
35 simpr ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → 𝑋𝐵 )
36 26 27 28 3 29 31 32 34 35 evlssca ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly ( 𝑅s 𝐵 ) ) ) ‘ 𝑋 ) ) = ( ( 𝐵m 1o ) × { 𝑋 } ) )
37 25 36 eqtrd ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( 𝐴𝑋 ) ) = ( ( 𝐵m 1o ) × { 𝑋 } ) )
38 37 coeq1d ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( ( ( 1o eval 𝑅 ) ‘ ( 𝐴𝑋 ) ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐵m 1o ) × { 𝑋 } ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
39 df1o2 1o = { ∅ }
40 3 fvexi 𝐵 ∈ V
41 0ex ∅ ∈ V
42 eqid ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) )
43 39 40 41 42 mapsnf1o3 ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵1-1-onto→ ( 𝐵m 1o )
44 f1of ( ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵1-1-onto→ ( 𝐵m 1o ) → ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵m 1o ) )
45 43 44 mp1i ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵m 1o ) )
46 42 fmpt ( ∀ 𝑦𝐵 ( 1o × { 𝑦 } ) ∈ ( 𝐵m 1o ) ↔ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵m 1o ) )
47 45 46 sylibr ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ∀ 𝑦𝐵 ( 1o × { 𝑦 } ) ∈ ( 𝐵m 1o ) )
48 eqidd ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) )
49 fconstmpt ( ( 𝐵m 1o ) × { 𝑋 } ) = ( 𝑥 ∈ ( 𝐵m 1o ) ↦ 𝑋 )
50 49 a1i ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( ( 𝐵m 1o ) × { 𝑋 } ) = ( 𝑥 ∈ ( 𝐵m 1o ) ↦ 𝑋 ) )
51 eqidd ( 𝑥 = ( 1o × { 𝑦 } ) → 𝑋 = 𝑋 )
52 47 48 50 51 fmptcof ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( ( ( 𝐵m 1o ) × { 𝑋 } ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝑦𝐵𝑋 ) )
53 fconstmpt ( 𝐵 × { 𝑋 } ) = ( 𝑦𝐵𝑋 )
54 52 53 eqtr4di ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( ( ( 𝐵m 1o ) × { 𝑋 } ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝐵 × { 𝑋 } ) )
55 17 38 54 3eqtrd ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑂 ‘ ( 𝐴𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )