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