Metamath Proof Explorer

Theorem mpfproj

Description: Projections are multivariate polynomial functions. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Hypotheses mpfconst.b 
|- B = ( Base ` S )
mpfconst.q 
|- Q = ran ( ( I evalSub S ) ` R )
mpfconst.i 
|- ( ph -> I e. V )
mpfconst.s 
|- ( ph -> S e. CRing )
mpfconst.r 
|- ( ph -> R e. ( SubRing ` S ) )
mpfproj.j 
|- ( ph -> J e. I )
Assertion mpfproj 
|- ( ph -> ( f e. ( B ^m I ) |-> ( f ` J ) ) e. Q )

Proof

Step Hyp Ref Expression
1 mpfconst.b 
 |-  B = ( Base ` S )
2 mpfconst.q 
 |-  Q = ran ( ( I evalSub S ) ` R )
3 mpfconst.i 
 |-  ( ph -> I e. V )
4 mpfconst.s 
 |-  ( ph -> S e. CRing )
5 mpfconst.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
6 mpfproj.j 
 |-  ( ph -> J e. I )
7 eqid 
 |-  ( ( I evalSub S ) ` R ) = ( ( I evalSub S ) ` R )
8 eqid 
 |-  ( I mVar ( S |`s R ) ) = ( I mVar ( S |`s R ) )
9 eqid 
 |-  ( S |`s R ) = ( S |`s R )
10 7 8 9 1 3 4 5 6 evlsvar 
 |-  ( ph -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` J ) ) = ( f e. ( B ^m I ) |-> ( f ` J ) ) )
11 eqid 
 |-  ( I mPoly ( S |`s R ) ) = ( I mPoly ( S |`s R ) )
12 eqid 
 |-  ( S ^s ( B ^m I ) ) = ( S ^s ( B ^m I ) )
13 7 11 9 12 1 evlsrhm 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) )
14 3 4 5 13 syl3anc 
 |-  ( ph -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) )
15 eqid 
 |-  ( Base ` ( I mPoly ( S |`s R ) ) ) = ( Base ` ( I mPoly ( S |`s R ) ) )
16 eqid 
 |-  ( Base ` ( S ^s ( B ^m I ) ) ) = ( Base ` ( S ^s ( B ^m I ) ) )
17 15 16 rhmf 
 |-  ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) )
18 ffn 
 |-  ( ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) )
19 14 17 18 3syl 
 |-  ( ph -> ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) )
20 9 subrgring 
 |-  ( R e. ( SubRing ` S ) -> ( S |`s R ) e. Ring )
21 5 20 syl 
 |-  ( ph -> ( S |`s R ) e. Ring )
22 11 8 15 3 21 6 mvrcl 
 |-  ( ph -> ( ( I mVar ( S |`s R ) ) ` J ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
23 fnfvelrn 
 |-  ( ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( I mVar ( S |`s R ) ) ` J ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` J ) ) e. ran ( ( I evalSub S ) ` R ) )
24 19 22 23 syl2anc 
 |-  ( ph -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` J ) ) e. ran ( ( I evalSub S ) ` R ) )
25 24 2 eleqtrrdi 
 |-  ( ph -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S |`s R ) ) ` J ) ) e. Q )
26 10 25 eqeltrrd 
 |-  ( ph -> ( f e. ( B ^m I ) |-> ( f ` J ) ) e. Q )