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

Metamath Proof Explorer

Theorem evls1sca

Description: Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019)

Ref Expression
Hypotheses evls1sca.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1sca.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
evls1sca.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evls1sca.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
evls1sca.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
evls1sca.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evls1sca.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1sca.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion evls1sca ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 evls1sca.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1sca.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
3 evls1sca.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4 evls1sca.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
5 evls1sca.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
6 evls1sca.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
7 evls1sca.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8 evls1sca.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
9 1on ⊢ 1o ∈ On
10 eqid ⊢ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 1o evalSub 𝑆 ) ‘ 𝑅 )
11 eqid ⊢ ( 1o mPoly 𝑈 ) = ( 1o mPoly 𝑈 )
12 eqid ⊢ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 1o ) )
13 10 11 3 12 4 evlsrhm ⊢ ( ( 1o ∈ On ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
14 9 6 7 13 mp3an2i ⊢ ( 𝜑 → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
15 eqid ⊢ ( Base ‘ ( 1o mPoly 𝑈 ) ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
16 eqid ⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) )
17 15 16 rhmf ⊢ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 1o mPoly 𝑈 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
18 14 17 syl ⊢ ( 𝜑 → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 1o mPoly 𝑈 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
19 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
20 3 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
21 7 20 syl ⊢ ( 𝜑 → 𝑈 ∈ Ring )
22 2 ply1ring ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
23 21 22 syl ⊢ ( 𝜑 → 𝑊 ∈ Ring )
24 2 ply1lmod ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ LMod )
25 21 24 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
26 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
27 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
28 5 19 23 25 26 27 asclf ⊢ ( 𝜑 → 𝐴 : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) )
29 4 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
30 7 29 syl ⊢ ( 𝜑 → 𝑅 ⊆ 𝐵 )
31 3 4 ressbas2 ⊢ ( 𝑅 ⊆ 𝐵 → 𝑅 = ( Base ‘ 𝑈 ) )
32 30 31 syl ⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
33 2 ply1sca ⊢ ( 𝑈 ∈ Ring → 𝑈 = ( Scalar ‘ 𝑊 ) )
34 21 33 syl ⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ 𝑊 ) )
35 34 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
36 32 35 eqtrd ⊢ ( 𝜑 → 𝑅 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
37 2 27 ply1bas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
38 37 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) ) )
39 38 eqcomd ⊢ ( 𝜑 → ( Base ‘ ( 1o mPoly 𝑈 ) ) = ( Base ‘ 𝑊 ) )
40 36 39 feq23d ⊢ ( 𝜑 → ( 𝐴 : 𝑅 ⟶ ( Base ‘ ( 1o mPoly 𝑈 ) ) ↔ 𝐴 : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) ) )
41 28 40 mpbird ⊢ ( 𝜑 → 𝐴 : 𝑅 ⟶ ( Base ‘ ( 1o mPoly 𝑈 ) ) )
42 41 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ ( 1o mPoly 𝑈 ) ) )
43 fvco3 ⊢ ( ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 1o mPoly 𝑈 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ∧ ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ ( 1o mPoly 𝑈 ) ) ) → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
44 18 42 43 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
45 5 a1i ⊢ ( 𝜑 → 𝐴 = ( algSc ‘ 𝑊 ) )
46 eqid ⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
47 2 46 ply1ascl ⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ ( 1o mPoly 𝑈 ) )
48 45 47 eqtrdi ⊢ ( 𝜑 → 𝐴 = ( algSc ‘ ( 1o mPoly 𝑈 ) ) )
49 48 fveq1d ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( ( algSc ‘ ( 1o mPoly 𝑈 ) ) ‘ 𝑋 ) )
50 49 fveq2d ⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly 𝑈 ) ) ‘ 𝑋 ) ) )
51 eqid ⊢ ( algSc ‘ ( 1o mPoly 𝑈 ) ) = ( algSc ‘ ( 1o mPoly 𝑈 ) )
52 9 a1i ⊢ ( 𝜑 → 1o ∈ On )
53 10 11 3 4 51 52 6 7 8 evlssca ⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly 𝑈 ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
54 50 53 eqtrd ⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
55 54 fveq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) )
56 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) )
57 coeq1 ⊢ ( 𝑥 = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) → ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) → ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
59 30 8 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
60 fconst6g ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
61 59 60 syl ⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
62 4 fvexi ⊢ 𝐵 ∈ V
63 62 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
64 ovex ⊢ ( 𝐵 ↑m 1o ) ∈ V
65 64 a1i ⊢ ( 𝜑 → ( 𝐵 ↑m 1o ) ∈ V )
66 63 65 elmapd ⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↔ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) : ( 𝐵 ↑m 1o ) ⟶ 𝐵 ) )
67 61 66 mpbird ⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) )
68 snex ⊢ { 𝑋 } ∈ V
69 64 68 xpex ⊢ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ V
70 69 a1i ⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ V )
71 63 mptexd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ∈ V )
72 coexg ⊢ ( ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ V ∧ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ∈ V ) → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ V )
73 70 71 72 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ V )
74 56 58 67 73 fvmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
75 fconst6g ⊢ ( 𝑦 ∈ 𝐵 → ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 )
76 75 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 )
77 62 9 pm3.2i ⊢ ( 𝐵 ∈ V ∧ 1o ∈ On )
78 77 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐵 ∈ V ∧ 1o ∈ On ) )
79 elmapg ⊢ ( ( 𝐵 ∈ V ∧ 1o ∈ On ) → ( ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) ↔ ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 ) )
80 78 79 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) ↔ ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 ) )
81 76 80 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) )
82 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) )
83 fconstmpt ⊢ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 )
84 83 a1i ⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 ) )
85 eqidd ⊢ ( 𝑧 = ( 1o × { 𝑦 } ) → 𝑋 = 𝑋 )
86 81 82 84 85 fmptco ⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
87 74 86 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
88 44 55 87 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
89 elpwg ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵 ) )
90 29 89 mpbird ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ∈ 𝒫 𝐵 )
91 7 90 syl ⊢ ( 𝜑 → 𝑅 ∈ 𝒫 𝐵 )
92 eqid ⊢ ( 1o evalSub 𝑆 ) = ( 1o evalSub 𝑆 )
93 1 92 4 evls1fval ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ 𝒫 𝐵 ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
94 6 91 93 syl2anc ⊢ ( 𝜑 → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
95 94 fveq1d ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) )
96 fconstmpt ⊢ ( 𝐵 × { 𝑋 } ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 )
97 96 a1i ⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
98 88 95 97 3eqtr4d ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )