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 11 12 syl 
 |-  ( ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) -> ( ( ( I evalSub S ) ` R ) " ( Base ` ( I mPoly ( S |`s R ) ) ) ) = ran ( ( I evalSub S ) ` R ) )
14 7 10 13 3syl 
 |-  ( ( 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 ) )
15 1 14 eqtr4id 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q = ( ( ( I evalSub S ) ` R ) " ( Base ` ( I mPoly ( S |`s R ) ) ) ) )
16 4 subrgring 
 |-  ( R e. ( SubRing ` S ) -> ( S |`s R ) e. Ring )
17 3 mplring 
 |-  ( ( I e. V /\ ( S |`s R ) e. Ring ) -> ( I mPoly ( S |`s R ) ) e. Ring )
18 16 17 sylan2 
 |-  ( ( I e. V /\ R e. ( SubRing ` S ) ) -> ( I mPoly ( S |`s R ) ) e. Ring )
19 18 3adant2 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( I mPoly ( S |`s R ) ) e. Ring )
20 8 subrgid 
 |-  ( ( I mPoly ( S |`s R ) ) e. Ring -> ( Base ` ( I mPoly ( S |`s R ) ) ) e. ( SubRing ` ( I mPoly ( S |`s R ) ) ) )
21 19 20 syl 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Base ` ( I mPoly ( S |`s R ) ) ) e. ( SubRing ` ( I mPoly ( S |`s R ) ) ) )
22 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 ) ) ) )
23 7 21 22 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 ) ) ) )
24 15 23 eqeltrd 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) )