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 )