Metamath Proof Explorer

Theorem pf1subrg

Description: Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses pf1const.b 
|- B = ( Base ` R )
pf1const.q 
|- Q = ran ( eval1 ` R )
Assertion pf1subrg 
|- ( R e. CRing -> Q e. ( SubRing ` ( R ^s B ) ) )

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 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
5 eqid 
 |-  ( R ^s B ) = ( R ^s B )
6 3 4 5 1 evl1rhm 
 |-  ( R e. CRing -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
7 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
8 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
9 7 8 rhmf 
 |-  ( ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
10 ffn 
 |-  ( ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) )
11 fnima 
 |-  ( ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) -> ( ( eval1 ` R ) " ( Base ` ( Poly1 ` R ) ) ) = ran ( eval1 ` R ) )
12 6 9 10 11 4syl 
 |-  ( R e. CRing -> ( ( eval1 ` R ) " ( Base ` ( Poly1 ` R ) ) ) = ran ( eval1 ` R ) )
13 12 2 eqtr4di 
 |-  ( R e. CRing -> ( ( eval1 ` R ) " ( Base ` ( Poly1 ` R ) ) ) = Q )
14 4 ply1assa 
 |-  ( R e. CRing -> ( Poly1 ` R ) e. AssAlg )
15 assaring 
 |-  ( ( Poly1 ` R ) e. AssAlg -> ( Poly1 ` R ) e. Ring )
16 7 subrgid 
 |-  ( ( Poly1 ` R ) e. Ring -> ( Base ` ( Poly1 ` R ) ) e. ( SubRing ` ( Poly1 ` R ) ) )
17 14 15 16 3syl 
 |-  ( R e. CRing -> ( Base ` ( Poly1 ` R ) ) e. ( SubRing ` ( Poly1 ` R ) ) )
18 rhmima 
 |-  ( ( ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) /\ ( Base ` ( Poly1 ` R ) ) e. ( SubRing ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) " ( Base ` ( Poly1 ` R ) ) ) e. ( SubRing ` ( R ^s B ) ) )
19 6 17 18 syl2anc 
 |-  ( R e. CRing -> ( ( eval1 ` R ) " ( Base ` ( Poly1 ` R ) ) ) e. ( SubRing ` ( R ^s B ) ) )
20 13 19 eqeltrrd 
 |-  ( R e. CRing -> Q e. ( SubRing ` ( R ^s B ) ) )