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 = ( eval1 ` R )
evl1var.v 
|- X = ( var1 ` R )
evl1var.b 
|- B = ( Base ` R )
Assertion evl1var 
|- ( R e. CRing -> ( O ` X ) = ( _I |` B ) )

Proof

Step Hyp Ref Expression
1 evl1var.q 
 |-  O = ( eval1 ` R )
2 evl1var.v 
 |-  X = ( var1 ` R )
3 evl1var.b 
 |-  B = ( Base ` R )
4 crngring 
 |-  ( R e. CRing -> R e. Ring )
5 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
6 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
7 2 5 6 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` ( Poly1 ` R ) ) )
8 4 7 syl 
 |-  ( R e. CRing -> X e. ( Base ` ( Poly1 ` R ) ) )
9 eqid 
 |-  ( 1o eval R ) = ( 1o eval R )
10 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
11 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
12 5 11 6 ply1bas 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( 1o mPoly R ) )
13 1 9 3 10 12 evl1val 
 |-  ( ( R e. CRing /\ X e. ( Base ` ( Poly1 ` R ) ) ) -> ( O ` X ) = ( ( ( 1o eval R ) ` X ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
14 8 13 mpdan 
 |-  ( R e. CRing -> ( O ` X ) = ( ( ( 1o eval R ) ` X ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
15 df1o2 
 |-  1o = { (/) }
16 3 fvexi 
 |-  B e. _V
17 0ex 
 |-  (/) e. _V
18 eqid 
 |-  ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) = ( z e. ( B ^m 1o ) |-> ( z ` (/) ) )
19 15 16 17 18 mapsncnv 
 |-  `' ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) = ( y e. B |-> ( 1o X. { y } ) )
20 19 coeq2i 
 |-  ( ( ( 1o eval R ) ` X ) o. `' ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) ) = ( ( ( 1o eval R ) ` X ) o. ( y e. B |-> ( 1o X. { y } ) ) )
21 3 ressid 
 |-  ( R e. CRing -> ( R |`s B ) = R )
22 21 oveq2d 
 |-  ( R e. CRing -> ( 1o mVar ( R |`s B ) ) = ( 1o mVar R ) )
23 22 fveq1d 
 |-  ( R e. CRing -> ( ( 1o mVar ( R |`s B ) ) ` (/) ) = ( ( 1o mVar R ) ` (/) ) )
24 2 vr1val 
 |-  X = ( ( 1o mVar R ) ` (/) )
25 23 24 eqtr4di 
 |-  ( R e. CRing -> ( ( 1o mVar ( R |`s B ) ) ` (/) ) = X )
26 25 fveq2d 
 |-  ( R e. CRing -> ( ( 1o eval R ) ` ( ( 1o mVar ( R |`s B ) ) ` (/) ) ) = ( ( 1o eval R ) ` X ) )
27 9 3 evlval 
 |-  ( 1o eval R ) = ( ( 1o evalSub R ) ` B )
28 eqid 
 |-  ( 1o mVar ( R |`s B ) ) = ( 1o mVar ( R |`s B ) )
29 eqid 
 |-  ( R |`s B ) = ( R |`s B )
30 1on 
 |-  1o e. On
31 30 a1i 
 |-  ( R e. CRing -> 1o e. On )
32 id 
 |-  ( R e. CRing -> R e. CRing )
33 3 subrgid 
 |-  ( R e. Ring -> B e. ( SubRing ` R ) )
34 4 33 syl 
 |-  ( R e. CRing -> B e. ( SubRing ` R ) )
35 0lt1o 
 |-  (/) e. 1o
36 35 a1i 
 |-  ( R e. CRing -> (/) e. 1o )
37 27 28 29 3 31 32 34 36 evlsvar 
 |-  ( R e. CRing -> ( ( 1o eval R ) ` ( ( 1o mVar ( R |`s B ) ) ` (/) ) ) = ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) )
38 26 37 eqtr3d 
 |-  ( R e. CRing -> ( ( 1o eval R ) ` X ) = ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) )
39 38 coeq1d 
 |-  ( R e. CRing -> ( ( ( 1o eval R ) ` X ) o. `' ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) ) = ( ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) o. `' ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) ) )
40 20 39 eqtr3id 
 |-  ( R e. CRing -> ( ( ( 1o eval R ) ` X ) o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) o. `' ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) ) )
41 15 16 17 18 mapsnf1o2 
 |-  ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) : ( B ^m 1o ) -1-1-onto-> B
42 f1ococnv2 
 |-  ( ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) : ( B ^m 1o ) -1-1-onto-> B -> ( ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) o. `' ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) ) = ( _I |` B ) )
43 41 42 mp1i 
 |-  ( R e. CRing -> ( ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) o. `' ( z e. ( B ^m 1o ) |-> ( z ` (/) ) ) ) = ( _I |` B ) )
44 14 40 43 3eqtrd 
 |-  ( R e. CRing -> ( O ` X ) = ( _I |` B ) )