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	$⊢ φ \to I \in V$
	mpfconst.s	$⊢ φ \to S \in CRing$
	mpfconst.r	$⊢ φ \to R \in SubRing (S)$
	mpfproj.j	$⊢ φ \to J \in I$
Assertion	mpfproj	$⊢ φ \to (f \in (B^{I}) ⟼ f (J)) \in Q$

Proof

Step	Hyp	Ref	Expression
1		mpfconst.b	$⊢ B = {Base}_{S}$
2		mpfconst.q	$⊢ Q = ran (I evalSub S) (R)$
3		mpfconst.i	$⊢ φ \to I \in V$
4		mpfconst.s	$⊢ φ \to S \in CRing$
5		mpfconst.r	$⊢ φ \to R \in SubRing (S)$
6		mpfproj.j	$⊢ φ \to J \in I$
7		eqid	$⊢ (I evalSub S) (R) = (I evalSub S) (R)$
8		eqid	$⊢ I mVar (S ↾_{𝑠} R) = I mVar (S ↾_{𝑠} R)$
9		eqid	$⊢ S ↾_{𝑠} R = S ↾_{𝑠} R$
10	7 8 9 1 3 4 5 6	evlsvar	$⊢ φ \to (I evalSub S) (R) ((I mVar (S ↾_{𝑠} R)) (J)) = (f \in (B^{I}) ⟼ f (J))$
11		eqid	$⊢ I mPoly (S ↾_{𝑠} R) = I mPoly (S ↾_{𝑠} R)$
12		eqid	$⊢ S ↑_{𝑠} (B^{I}) = S ↑_{𝑠} (B^{I})$
13	7 11 9 12 1	evlsrhm	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to (I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) RingHom (S ↑_{𝑠} (B^{I})))$
14	3 4 5 13	syl3anc	$⊢ φ \to (I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) RingHom (S ↑_{𝑠} (B^{I})))$
15		eqid	$⊢ {Base}_{(I mPoly (S ↾_{𝑠} R))} = {Base}_{(I mPoly (S ↾_{𝑠} R))}$
16		eqid	$⊢ {Base}_{(S ↑_{𝑠} (B^{I}))} = {Base}_{(S ↑_{𝑠} (B^{I}))}$
17	15 16	rhmf	$⊢ (I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) RingHom (S ↑_{𝑠} (B^{I}))) \to (I evalSub S) (R) : {Base}_{(I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(S ↑_{𝑠} (B^{I}))}$
18		ffn	$⊢ (I evalSub S) (R) : {Base}_{(I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(S ↑_{𝑠} (B^{I}))} \to (I evalSub S) (R) Fn {Base}_{(I mPoly (S ↾_{𝑠} R))}$
19	14 17 18	3syl	$⊢ φ \to (I evalSub S) (R) Fn {Base}_{(I mPoly (S ↾_{𝑠} R))}$
20	9	subrgring	$⊢ R \in SubRing (S) \to S ↾_{𝑠} R \in Ring$
21	5 20	syl	$⊢ φ \to S ↾_{𝑠} R \in Ring$
22	11 8 15 3 21 6	mvrcl	$⊢ φ \to (I mVar (S ↾_{𝑠} R)) (J) \in {Base}_{(I mPoly (S ↾_{𝑠} R))}$
23		fnfvelrn	$⊢ ((I evalSub S) (R) Fn {Base}_{(I mPoly (S ↾_{𝑠} R))} \land (I mVar (S ↾_{𝑠} R)) (J) \in {Base}_{(I mPoly (S ↾_{𝑠} R))}) \to (I evalSub S) (R) ((I mVar (S ↾_{𝑠} R)) (J)) \in ran (I evalSub S) (R)$
24	19 22 23	syl2anc	$⊢ φ \to (I evalSub S) (R) ((I mVar (S ↾_{𝑠} R)) (J)) \in ran (I evalSub S) (R)$
25	24 2	eleqtrrdi	$⊢ φ \to (I evalSub S) (R) ((I mVar (S ↾_{𝑠} R)) (J)) \in Q$
26	10 25	eqeltrrd	$⊢ φ \to (f \in (B^{I}) ⟼ f (J)) \in Q$

Metamath Proof Explorer

Theorem mpfproj

Proof