Metamath Proof Explorer


Theorem evl1var

Description: Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1var.q 𝑂 = ( eval1𝑅 )
evl1var.v 𝑋 = ( var1𝑅 )
evl1var.b 𝐵 = ( Base ‘ 𝑅 )
Assertion evl1var ( 𝑅 ∈ CRing → ( 𝑂𝑋 ) = ( I ↾ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 evl1var.q 𝑂 = ( eval1𝑅 )
2 evl1var.v 𝑋 = ( var1𝑅 )
3 evl1var.b 𝐵 = ( Base ‘ 𝑅 )
4 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
5 eqid ( Poly1𝑅 ) = ( Poly1𝑅 )
6 eqid ( Base ‘ ( Poly1𝑅 ) ) = ( Base ‘ ( Poly1𝑅 ) )
7 2 5 6 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ ( Poly1𝑅 ) ) )
8 4 7 syl ( 𝑅 ∈ CRing → 𝑋 ∈ ( Base ‘ ( Poly1𝑅 ) ) )
9 eqid ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
10 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
11 eqid ( PwSer1𝑅 ) = ( PwSer1𝑅 )
12 5 11 6 ply1bas ( Base ‘ ( Poly1𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
13 1 9 3 10 12 evl1val ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( 𝑂𝑋 ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
14 8 13 mpdan ( 𝑅 ∈ CRing → ( 𝑂𝑋 ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
15 df1o2 1o = { ∅ }
16 3 fvexi 𝐵 ∈ V
17 0ex ∅ ∈ V
18 eqid ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) = ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) )
19 15 16 17 18 mapsncnv ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) = ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) )
20 19 coeq2i ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) )
21 3 ressid ( 𝑅 ∈ CRing → ( 𝑅s 𝐵 ) = 𝑅 )
22 21 oveq2d ( 𝑅 ∈ CRing → ( 1o mVar ( 𝑅s 𝐵 ) ) = ( 1o mVar 𝑅 ) )
23 22 fveq1d ( 𝑅 ∈ CRing → ( ( 1o mVar ( 𝑅s 𝐵 ) ) ‘ ∅ ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
24 2 vr1val 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
25 23 24 eqtr4di ( 𝑅 ∈ CRing → ( ( 1o mVar ( 𝑅s 𝐵 ) ) ‘ ∅ ) = 𝑋 )
26 25 fveq2d ( 𝑅 ∈ CRing → ( ( 1o eval 𝑅 ) ‘ ( ( 1o mVar ( 𝑅s 𝐵 ) ) ‘ ∅ ) ) = ( ( 1o eval 𝑅 ) ‘ 𝑋 ) )
27 9 3 evlval ( 1o eval 𝑅 ) = ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
28 eqid ( 1o mVar ( 𝑅s 𝐵 ) ) = ( 1o mVar ( 𝑅s 𝐵 ) )
29 eqid ( 𝑅s 𝐵 ) = ( 𝑅s 𝐵 )
30 1on 1o ∈ On
31 30 a1i ( 𝑅 ∈ CRing → 1o ∈ On )
32 id ( 𝑅 ∈ CRing → 𝑅 ∈ CRing )
33 3 subrgid ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
34 4 33 syl ( 𝑅 ∈ CRing → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
35 0lt1o ∅ ∈ 1o
36 35 a1i ( 𝑅 ∈ CRing → ∅ ∈ 1o )
37 27 28 29 3 31 32 34 36 evlsvar ( 𝑅 ∈ CRing → ( ( 1o eval 𝑅 ) ‘ ( ( 1o mVar ( 𝑅s 𝐵 ) ) ‘ ∅ ) ) = ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) )
38 26 37 eqtr3d ( 𝑅 ∈ CRing → ( ( 1o eval 𝑅 ) ‘ 𝑋 ) = ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) )
39 38 coeq1d ( 𝑅 ∈ CRing → ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) = ( ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ∘ ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) )
40 20 39 syl5eqr ( 𝑅 ∈ CRing → ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ∘ ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) )
41 15 16 17 18 mapsnf1o2 ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) : ( 𝐵m 1o ) –1-1-onto𝐵
42 f1ococnv2 ( ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) : ( 𝐵m 1o ) –1-1-onto𝐵 → ( ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ∘ ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) = ( I ↾ 𝐵 ) )
43 41 42 mp1i ( 𝑅 ∈ CRing → ( ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ∘ ( 𝑧 ∈ ( 𝐵m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) = ( I ↾ 𝐵 ) )
44 14 40 43 3eqtrd ( 𝑅 ∈ CRing → ( 𝑂𝑋 ) = ( I ↾ 𝐵 ) )