This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 𝐼 ) ↦ ( 𝑓 ‘ 𝐽 ) ) ∈ 𝑄 )