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

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