Metamath Proof Explorer

Theorem pf1id

Description: The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Hypotheses pf1const.b 
|- B = ( Base ` R )
pf1const.q 
|- Q = ran ( eval1 ` R )
Assertion pf1id 
|- ( R e. CRing -> ( _I |` B ) e. Q )

Proof

Step Hyp Ref Expression
1 pf1const.b 
 |-  B = ( Base ` R )
2 pf1const.q 
 |-  Q = ran ( eval1 ` R )
3 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
4 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
5 3 4 1 evl1var 
 |-  ( R e. CRing -> ( ( eval1 ` R ) ` ( var1 ` R ) ) = ( _I |` B ) )
6 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
7 eqid 
 |-  ( R ^s B ) = ( R ^s B )
8 3 6 7 1 evl1rhm 
 |-  ( R e. CRing -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
9 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
10 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
11 9 10 rhmf 
 |-  ( ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
12 ffn 
 |-  ( ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) )
13 8 11 12 3syl 
 |-  ( R e. CRing -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) )
14 crngring 
 |-  ( R e. CRing -> R e. Ring )
15 4 6 9 vr1cl 
 |-  ( R e. Ring -> ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) )
16 14 15 syl 
 |-  ( R e. CRing -> ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) )
17 fnfvelrn 
 |-  ( ( ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) /\ ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` ( var1 ` R ) ) e. ran ( eval1 ` R ) )
18 13 16 17 syl2anc 
 |-  ( R e. CRing -> ( ( eval1 ` R ) ` ( var1 ` R ) ) e. ran ( eval1 ` R ) )
19 5 18 eqeltrrd 
 |-  ( R e. CRing -> ( _I |` B ) e. ran ( eval1 ` R ) )
20 19 2 eleqtrrdi 
 |-  ( R e. CRing -> ( _I |` B ) e. Q )