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