Metamath Proof Explorer

Theorem mpfconst

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

Ref Expression
Hypotheses mpfconst.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
mpfconst.q ⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
mpfconst.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mpfconst.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
mpfconst.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
mpfconst.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion mpfconst ( 𝜑 → ( ( 𝐵 ↑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 mpfconst.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
7 eqid ⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
8 eqid ⊢ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) )
9 eqid ⊢ ( 𝑆 ↾s 𝑅 ) = ( 𝑆 ↾s 𝑅 )
10 eqid ⊢ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) )
11 7 8 9 1 10 3 4 5 6 evlssca ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
12 eqid ⊢ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
13 7 8 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 eqid ⊢ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) = ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) )
23 8 mplring ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑆 ↾s 𝑅 ) ∈ Ring ) → ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ∈ Ring )
24 8 mpllmod ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑆 ↾s 𝑅 ) ∈ Ring ) → ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ∈ LMod )
25 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
26 10 22 23 24 25 15 asclf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑆 ↾s 𝑅 ) ∈ Ring ) → ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) : ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) ⟶ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
27 3 21 26 syl2anc ⊢ ( 𝜑 → ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) : ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) ⟶ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
28 1 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
29 9 1 ressbas2 ⊢ ( 𝑅 ⊆ 𝐵 → 𝑅 = ( Base ‘ ( 𝑆 ↾s 𝑅 ) ) )
30 5 28 29 3syl ⊢ ( 𝜑 → 𝑅 = ( Base ‘ ( 𝑆 ↾s 𝑅 ) ) )
31 ovexd ⊢ ( 𝜑 → ( 𝑆 ↾s 𝑅 ) ∈ V )
32 8 3 31 mplsca ⊢ ( 𝜑 → ( 𝑆 ↾s 𝑅 ) = ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
33 32 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( 𝑆 ↾s 𝑅 ) ) = ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) )
34 30 33 eqtrd ⊢ ( 𝜑 → 𝑅 = ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) )
35 6 34 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) )
36 27 35 ffvelcdmd ⊢ ( 𝜑 → ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ‘ 𝑋 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
37 fnfvelrn ⊢ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ∧ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ‘ 𝑋 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ‘ 𝑋 ) ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
38 19 36 37 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ‘ 𝑋 ) ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
39 11 38 eqeltrrd ⊢ ( 𝜑 → ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
40 39 2 eleqtrrdi ⊢ ( 𝜑 → ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ∈ 𝑄 )