Metamath Proof Explorer

Theorem mpfconst

Description: Constants are multivariate polynomial functions. (Contributed by Mario Carneiro, 19-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 ) )
mpfconst.x 
|- ( ph -> X e. R )
Assertion mpfconst 
|- ( ph -> ( ( B ^m I ) X. { X } ) 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 mpfconst.x 
 |-  ( ph -> X e. R )
7 eqid 
 |-  ( ( I evalSub S ) ` R ) = ( ( I evalSub S ) ` R )
8 eqid 
 |-  ( I mPoly ( S |`s R ) ) = ( I mPoly ( S |`s R ) )
9 eqid 
 |-  ( S |`s R ) = ( S |`s R )
10 eqid 
 |-  ( algSc ` ( I mPoly ( S |`s R ) ) ) = ( algSc ` ( I mPoly ( S |`s R ) ) )
11 7 8 9 1 10 3 4 5 6 evlssca 
 |-  ( ph -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) ) = ( ( B ^m I ) X. { X } ) )
12 eqid 
 |-  ( S ^s ( B ^m I ) ) = ( S ^s ( B ^m I ) )
13 7 8 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 eqid 
 |-  ( Scalar ` ( I mPoly ( S |`s R ) ) ) = ( Scalar ` ( I mPoly ( S |`s R ) ) )
23 8 mplring 
 |-  ( ( I e. V /\ ( S |`s R ) e. Ring ) -> ( I mPoly ( S |`s R ) ) e. Ring )
24 8 mpllmod 
 |-  ( ( I e. V /\ ( S |`s R ) e. Ring ) -> ( I mPoly ( S |`s R ) ) e. LMod )
25 eqid 
 |-  ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) )
26 10 22 23 24 25 15 asclf 
 |-  ( ( I e. V /\ ( S |`s R ) e. Ring ) -> ( algSc ` ( I mPoly ( S |`s R ) ) ) : ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) --> ( Base ` ( I mPoly ( S |`s R ) ) ) )
27 3 21 26 syl2anc 
 |-  ( ph -> ( algSc ` ( I mPoly ( S |`s R ) ) ) : ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) --> ( Base ` ( I mPoly ( S |`s R ) ) ) )
28 1 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
29 9 1 ressbas2 
 |-  ( R C_ B -> R = ( Base ` ( S |`s R ) ) )
30 5 28 29 3syl 
 |-  ( ph -> R = ( Base ` ( S |`s R ) ) )
31 ovexd 
 |-  ( ph -> ( S |`s R ) e. _V )
32 8 3 31 mplsca 
 |-  ( ph -> ( S |`s R ) = ( Scalar ` ( I mPoly ( S |`s R ) ) ) )
33 32 fveq2d 
 |-  ( ph -> ( Base ` ( S |`s R ) ) = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) )
34 30 33 eqtrd 
 |-  ( ph -> R = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) )
35 6 34 eleqtrd 
 |-  ( ph -> X e. ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) )
36 27 35 ffvelrnd 
 |-  ( ph -> ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) )
37 fnfvelrn 
 |-  ( ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) ) e. ran ( ( I evalSub S ) ` R ) )
38 19 36 37 syl2anc 
 |-  ( ph -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) ) e. ran ( ( I evalSub S ) ` R ) )
39 11 38 eqeltrrd 
 |-  ( ph -> ( ( B ^m I ) X. { X } ) e. ran ( ( I evalSub S ) ` R ) )
40 39 2 eleqtrrdi 
 |-  ( ph -> ( ( B ^m I ) X. { X } ) e. Q )