Metamath Proof Explorer

Theorem mpfsubrg

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

Ref Expression
Hypothesis mpfsubrg.q 
|- Q = ran ( ( I evalSub S ) ` R )
Assertion mpfsubrg 
|- ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )

Proof

Step Hyp Ref Expression
1 mpfsubrg.q 
 |-  Q = ran ( ( I evalSub S ) ` R )
2 eqid 
 |-  ( ( I evalSub S ) ` R ) = ( ( I evalSub S ) ` R )
3 eqid 
 |-  ( I mPoly ( S |`s R ) ) = ( I mPoly ( S |`s R ) )
4 eqid 
 |-  ( S |`s R ) = ( S |`s R )
5 eqid 
 |-  ( S ^s ( ( Base ` S ) ^m I ) ) = ( S ^s ( ( Base ` S ) ^m I ) )
6 eqid 
 |-  ( Base ` S ) = ( Base ` S )
7 2 3 4 5 6 evlsrhm 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) )
8 eqid 
 |-  ( Base ` ( I mPoly ( S |`s R ) ) ) = ( Base ` ( I mPoly ( S |`s R ) ) )
9 eqid 
 |-  ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) = ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) )
10 8 9 rhmf 
 |-  ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) -> ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
11 ffn 
 |-  ( ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) -> ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) )
12 fnima 
 |-  ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) -> ( ( ( I evalSub S ) ` R ) " ( Base ` ( I mPoly ( S |`s R ) ) ) ) = ran ( ( I evalSub S ) ` R ) )
13 7 10 11 12 4syl 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( ( I evalSub S ) ` R ) " ( Base ` ( I mPoly ( S |`s R ) ) ) ) = ran ( ( I evalSub S ) ` R ) )
14 1 13 eqtr4id 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q = ( ( ( I evalSub S ) ` R ) " ( Base ` ( I mPoly ( S |`s R ) ) ) ) )
15 4 subrgring 
 |-  ( R e. ( SubRing ` S ) -> ( S |`s R ) e. Ring )
16 3 mplring 
 |-  ( ( I e. V /\ ( S |`s R ) e. Ring ) -> ( I mPoly ( S |`s R ) ) e. Ring )
17 15 16 sylan2 
 |-  ( ( I e. V /\ R e. ( SubRing ` S ) ) -> ( I mPoly ( S |`s R ) ) e. Ring )
18 17 3adant2 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( I mPoly ( S |`s R ) ) e. Ring )
19 8 subrgid 
 |-  ( ( I mPoly ( S |`s R ) ) e. Ring -> ( Base ` ( I mPoly ( S |`s R ) ) ) e. ( SubRing ` ( I mPoly ( S |`s R ) ) ) )
20 18 19 syl 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Base ` ( I mPoly ( S |`s R ) ) ) e. ( SubRing ` ( I mPoly ( S |`s R ) ) ) )
21 rhmima 
 |-  ( ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( ( Base ` S ) ^m I ) ) ) /\ ( Base ` ( I mPoly ( S |`s R ) ) ) e. ( SubRing ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) " ( Base ` ( I mPoly ( S |`s R ) ) ) ) e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
22 7 20 21 syl2anc 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( ( I evalSub S ) ` R ) " ( Base ` ( I mPoly ( S |`s R ) ) ) ) e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )
23 14 22 eqeltrd 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )