mpfproj

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

	Ref	Expression
Hypotheses	mpfconst.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	mpfconst.q	⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	mpfconst.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mpfconst.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	mpfconst.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	mpfproj.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
Assertion	mpfproj	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐵 ↑_m 𝐼 ) ↦ ( 𝑓 ‘ 𝐽 ) ) ∈ 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		mpfconst.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
2		mpfconst.q	⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
3		mpfconst.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		mpfconst.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
5		mpfconst.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
6		mpfproj.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
7		eqid	⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
8		eqid	⊢ ( 𝐼 mVar ( 𝑆 ↾_s 𝑅 ) ) = ( 𝐼 mVar ( 𝑆 ↾_s 𝑅 ) )
9		eqid	⊢ ( 𝑆 ↾_s 𝑅 ) = ( 𝑆 ↾_s 𝑅 )
10	7 8 9 1 3 4 5 6	evlsvar	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾_s 𝑅 ) ) ‘ 𝐽 ) ) = ( 𝑓 ∈ ( 𝐵 ↑_m 𝐼 ) ↦ ( 𝑓 ‘ 𝐽 ) ) )
11		eqid	⊢ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) = ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) )
12		eqid	⊢ ( 𝑆 ↑_s ( 𝐵 ↑_m 𝐼 ) ) = ( 𝑆 ↑_s ( 𝐵 ↑_m 𝐼 ) )
13	7 11 9 12 1	evlsrhm	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) RingHom ( 𝑆 ↑_s ( 𝐵 ↑_m 𝐼 ) ) ) )
14	3 4 5 13	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) RingHom ( 𝑆 ↑_s ( 𝐵 ↑_m 𝐼 ) ) ) )
15		eqid	⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) )
16		eqid	⊢ ( Base ‘ ( 𝑆 ↑_s ( 𝐵 ↑_m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑_s ( 𝐵 ↑_m 𝐼 ) ) )
17	15 16	rhmf	⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) RingHom ( 𝑆 ↑_s ( 𝐵 ↑_m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆 ↑_s ( 𝐵 ↑_m 𝐼 ) ) ) )
18		ffn	⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆 ↑_s ( 𝐵 ↑_m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) ) )
19	14 17 18	3syl	⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) ) )
20	9	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑆 ↾_s 𝑅 ) ∈ Ring )
21	5 20	syl	⊢ ( 𝜑 → ( 𝑆 ↾_s 𝑅 ) ∈ Ring )
22	11 8 15 3 21 6	mvrcl	⊢ ( 𝜑 → ( ( 𝐼 mVar ( 𝑆 ↾_s 𝑅 ) ) ‘ 𝐽 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) ) )
23		fnfvelrn	⊢ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) ) ∧ ( ( 𝐼 mVar ( 𝑆 ↾_s 𝑅 ) ) ‘ 𝐽 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾_s 𝑅 ) ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾_s 𝑅 ) ) ‘ 𝐽 ) ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
24	19 22 23	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾_s 𝑅 ) ) ‘ 𝐽 ) ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
25	24 2	eleqtrrdi	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾_s 𝑅 ) ) ‘ 𝐽 ) ) ∈ 𝑄 )
26	10 25	eqeltrrd	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐵 ↑_m 𝐼 ) ↦ ( 𝑓 ‘ 𝐽 ) ) ∈ 𝑄 )

Metamath Proof Explorer

Theorem mpfproj

Proof