Metamath Proof Explorer

Theorem 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 ⊢ φ → I ∈ V
mpfconst.s ⊢ φ → S ∈ CRing
mpfconst.r ⊢ φ → R ∈ SubRing ⁡ S
mpfproj.j ⊢ φ → J ∈ I
Assertion mpfproj ⊢ φ → f ∈ B I ⟼ f ⁡ J ∈ Q

Proof

Step Hyp Ref Expression
1 mpfconst.b ⊢ B = Base S
2 mpfconst.q ⊢ Q = ran ⁡ I evalSub S ⁡ R
3 mpfconst.i ⊢ φ → I ∈ V
4 mpfconst.s ⊢ φ → S ∈ CRing
5 mpfconst.r ⊢ φ → R ∈ SubRing ⁡ S
6 mpfproj.j ⊢ φ → J ∈ 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 ⊢ φ → I evalSub S ⁡ R ⁡ I mVar S ↾ 𝑠 R ⁡ J = f ∈ 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 ∈ V ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → I evalSub S ⁡ R ∈ I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 B I
14 3 4 5 13 syl3anc ⊢ φ → I evalSub S ⁡ R ∈ 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 ∈ I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 B I → 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 → I evalSub S ⁡ R Fn Base I mPoly S ↾ 𝑠 R
19 14 17 18 3syl ⊢ φ → I evalSub S ⁡ R Fn Base I mPoly S ↾ 𝑠 R
20 9 subrgring ⊢ R ∈ SubRing ⁡ S → S ↾ 𝑠 R ∈ Ring
21 5 20 syl ⊢ φ → S ↾ 𝑠 R ∈ Ring
22 11 8 15 3 21 6 mvrcl ⊢ φ → I mVar S ↾ 𝑠 R ⁡ J ∈ Base I mPoly S ↾ 𝑠 R
23 fnfvelrn ⊢ I evalSub S ⁡ R Fn Base I mPoly S ↾ 𝑠 R ∧ I mVar S ↾ 𝑠 R ⁡ J ∈ Base I mPoly S ↾ 𝑠 R → I evalSub S ⁡ R ⁡ I mVar S ↾ 𝑠 R ⁡ J ∈ ran ⁡ I evalSub S ⁡ R
24 19 22 23 syl2anc ⊢ φ → I evalSub S ⁡ R ⁡ I mVar S ↾ 𝑠 R ⁡ J ∈ ran ⁡ I evalSub S ⁡ R
25 24 2 eleqtrrdi ⊢ φ → I evalSub S ⁡ R ⁡ I mVar S ↾ 𝑠 R ⁡ J ∈ Q
26 10 25 eqeltrrd ⊢ φ → f ∈ B I ⟼ f ⁡ J ∈ Q