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 O = eval 1 R
evl1var.v X = var 1 R
evl1var.b B = Base R
Assertion evl1var R CRing O X = I B

Proof

Step Hyp Ref Expression
1 evl1var.q O = eval 1 R
2 evl1var.v X = var 1 R
3 evl1var.b B = Base R
4 crngring R CRing R Ring
5 eqid Poly 1 R = Poly 1 R
6 eqid Base Poly 1 R = Base Poly 1 R
7 2 5 6 vr1cl R Ring X Base Poly 1 R
8 4 7 syl R CRing X Base Poly 1 R
9 eqid 1 𝑜 eval R = 1 𝑜 eval R
10 eqid 1 𝑜 mPoly R = 1 𝑜 mPoly R
11 eqid PwSer 1 R = PwSer 1 R
12 5 11 6 ply1bas Base Poly 1 R = Base 1 𝑜 mPoly R
13 1 9 3 10 12 evl1val R CRing X Base Poly 1 R O X = 1 𝑜 eval R X y B 1 𝑜 × y
14 8 13 mpdan R CRing O X = 1 𝑜 eval R X y B 1 𝑜 × y
15 df1o2 1 𝑜 =
16 3 fvexi B V
17 0ex V
18 eqid z B 1 𝑜 z = z B 1 𝑜 z
19 15 16 17 18 mapsncnv z B 1 𝑜 z -1 = y B 1 𝑜 × y
20 19 coeq2i 1 𝑜 eval R X z B 1 𝑜 z -1 = 1 𝑜 eval R X y B 1 𝑜 × y
21 3 ressid R CRing R 𝑠 B = R
22 21 oveq2d R CRing 1 𝑜 mVar R 𝑠 B = 1 𝑜 mVar R
23 22 fveq1d R CRing 1 𝑜 mVar R 𝑠 B = 1 𝑜 mVar R
24 2 vr1val X = 1 𝑜 mVar R
25 23 24 eqtr4di R CRing 1 𝑜 mVar R 𝑠 B = X
26 25 fveq2d R CRing 1 𝑜 eval R 1 𝑜 mVar R 𝑠 B = 1 𝑜 eval R X
27 9 3 evlval 1 𝑜 eval R = 1 𝑜 evalSub R B
28 eqid 1 𝑜 mVar R 𝑠 B = 1 𝑜 mVar R 𝑠 B
29 eqid R 𝑠 B = R 𝑠 B
30 1on 1 𝑜 On
31 30 a1i R CRing 1 𝑜 On
32 id R CRing R CRing
33 3 subrgid R Ring B SubRing R
34 4 33 syl R CRing B SubRing R
35 0lt1o 1 𝑜
36 35 a1i R CRing 1 𝑜
37 27 28 29 3 31 32 34 36 evlsvar R CRing 1 𝑜 eval R 1 𝑜 mVar R 𝑠 B = z B 1 𝑜 z
38 26 37 eqtr3d R CRing 1 𝑜 eval R X = z B 1 𝑜 z
39 38 coeq1d R CRing 1 𝑜 eval R X z B 1 𝑜 z -1 = z B 1 𝑜 z z B 1 𝑜 z -1
40 20 39 eqtr3id R CRing 1 𝑜 eval R X y B 1 𝑜 × y = z B 1 𝑜 z z B 1 𝑜 z -1
41 15 16 17 18 mapsnf1o2 z B 1 𝑜 z : B 1 𝑜 1-1 onto B
42 f1ococnv2 z B 1 𝑜 z : B 1 𝑜 1-1 onto B z B 1 𝑜 z z B 1 𝑜 z -1 = I B
43 41 42 mp1i R CRing z B 1 𝑜 z z B 1 𝑜 z -1 = I B
44 14 40 43 3eqtrd R CRing O X = I B