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 )

Metamath Proof Explorer

Theorem mpfproj

Proof