Metamath Proof Explorer

Theorem mpfconst

Description: Constants are multivariate polynomial functions. (Contributed by Mario Carneiro, 19-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
mpfconst.x ⊢ φ → X ∈ R
Assertion mpfconst ⊢ φ → B I × X ∈ 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 mpfconst.x ⊢ φ → X ∈ R
7 eqid ⊢ I evalSub S ⁡ R = I evalSub S ⁡ R
8 eqid ⊢ I mPoly S ↾ 𝑠 R = I mPoly S ↾ 𝑠 R
9 eqid ⊢ S ↾ 𝑠 R = S ↾ 𝑠 R
10 eqid ⊢ algSc ⁡ I mPoly S ↾ 𝑠 R = algSc ⁡ I mPoly S ↾ 𝑠 R
11 7 8 9 1 10 3 4 5 6 evlssca ⊢ φ → I evalSub S ⁡ R ⁡ algSc ⁡ I mPoly S ↾ 𝑠 R ⁡ X = B I × X
12 eqid ⊢ S ↑ 𝑠 B I = S ↑ 𝑠 B I
13 7 8 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 eqid ⊢ Scalar ⁡ I mPoly S ↾ 𝑠 R = Scalar ⁡ I mPoly S ↾ 𝑠 R
23 8 mplring ⊢ I ∈ V ∧ S ↾ 𝑠 R ∈ Ring → I mPoly S ↾ 𝑠 R ∈ Ring
24 8 mpllmod ⊢ I ∈ V ∧ S ↾ 𝑠 R ∈ Ring → I mPoly S ↾ 𝑠 R ∈ LMod
25 eqid ⊢ Base Scalar ⁡ I mPoly S ↾ 𝑠 R = Base Scalar ⁡ I mPoly S ↾ 𝑠 R
26 10 22 23 24 25 15 asclf ⊢ I ∈ V ∧ S ↾ 𝑠 R ∈ Ring → algSc ⁡ I mPoly S ↾ 𝑠 R : Base Scalar ⁡ I mPoly S ↾ 𝑠 R ⟶ Base I mPoly S ↾ 𝑠 R
27 3 21 26 syl2anc ⊢ φ → algSc ⁡ I mPoly S ↾ 𝑠 R : Base Scalar ⁡ I mPoly S ↾ 𝑠 R ⟶ Base I mPoly S ↾ 𝑠 R
28 1 subrgss ⊢ R ∈ SubRing ⁡ S → R ⊆ B
29 9 1 ressbas2 ⊢ R ⊆ B → R = Base S ↾ 𝑠 R
30 5 28 29 3syl ⊢ φ → R = Base S ↾ 𝑠 R
31 ovexd ⊢ φ → S ↾ 𝑠 R ∈ V
32 8 3 31 mplsca ⊢ φ → S ↾ 𝑠 R = Scalar ⁡ I mPoly S ↾ 𝑠 R
33 32 fveq2d ⊢ φ → Base S ↾ 𝑠 R = Base Scalar ⁡ I mPoly S ↾ 𝑠 R
34 30 33 eqtrd ⊢ φ → R = Base Scalar ⁡ I mPoly S ↾ 𝑠 R
35 6 34 eleqtrd ⊢ φ → X ∈ Base Scalar ⁡ I mPoly S ↾ 𝑠 R
36 27 35 ffvelcdmd ⊢ φ → algSc ⁡ I mPoly S ↾ 𝑠 R ⁡ X ∈ Base I mPoly S ↾ 𝑠 R
37 fnfvelrn ⊢ I evalSub S ⁡ R Fn Base I mPoly S ↾ 𝑠 R ∧ algSc ⁡ I mPoly S ↾ 𝑠 R ⁡ X ∈ Base I mPoly S ↾ 𝑠 R → I evalSub S ⁡ R ⁡ algSc ⁡ I mPoly S ↾ 𝑠 R ⁡ X ∈ ran ⁡ I evalSub S ⁡ R
38 19 36 37 syl2anc ⊢ φ → I evalSub S ⁡ R ⁡ algSc ⁡ I mPoly S ↾ 𝑠 R ⁡ X ∈ ran ⁡ I evalSub S ⁡ R
39 11 38 eqeltrrd ⊢ φ → B I × X ∈ ran ⁡ I evalSub S ⁡ R
40 39 2 eleqtrrdi ⊢ φ → B I × X ∈ Q