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 
|- Q = ( S evalSub1 R )
evls1sca.w 
|- W = ( Poly1 ` U )
evls1sca.u 
|- U = ( S |`s R )
evls1sca.b 
|- B = ( Base ` S )
evls1sca.a 
|- A = ( algSc ` W )
evls1sca.s 
|- ( ph -> S e. CRing )
evls1sca.r 
|- ( ph -> R e. ( SubRing ` S ) )
evls1sca.x 
|- ( ph -> X e. R )
Assertion evls1sca 
|- ( ph -> ( Q ` ( A ` X ) ) = ( B X. { X } ) )

Proof

Step Hyp Ref Expression
1 evls1sca.q 
 |-  Q = ( S evalSub1 R )
2 evls1sca.w 
 |-  W = ( Poly1 ` U )
3 evls1sca.u 
 |-  U = ( S |`s R )
4 evls1sca.b 
 |-  B = ( Base ` S )
5 evls1sca.a 
 |-  A = ( algSc ` W )
6 evls1sca.s 
 |-  ( ph -> S e. CRing )
7 evls1sca.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
8 evls1sca.x 
 |-  ( ph -> X e. R )
9 1on 
 |-  1o e. On
10 eqid 
 |-  ( ( 1o evalSub S ) ` R ) = ( ( 1o evalSub S ) ` R )
11 eqid 
 |-  ( 1o mPoly U ) = ( 1o mPoly U )
12 eqid 
 |-  ( S ^s ( B ^m 1o ) ) = ( S ^s ( B ^m 1o ) )
13 10 11 3 12 4 evlsrhm 
 |-  ( ( 1o e. On /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( 1o evalSub S ) ` R ) e. ( ( 1o mPoly U ) RingHom ( S ^s ( B ^m 1o ) ) ) )
14 9 6 7 13 mp3an2i 
 |-  ( ph -> ( ( 1o evalSub S ) ` R ) e. ( ( 1o mPoly U ) RingHom ( S ^s ( B ^m 1o ) ) ) )
15 eqid 
 |-  ( Base ` ( 1o mPoly U ) ) = ( Base ` ( 1o mPoly U ) )
16 eqid 
 |-  ( Base ` ( S ^s ( B ^m 1o ) ) ) = ( Base ` ( S ^s ( B ^m 1o ) ) )
17 15 16 rhmf 
 |-  ( ( ( 1o evalSub S ) ` R ) e. ( ( 1o mPoly U ) RingHom ( S ^s ( B ^m 1o ) ) ) -> ( ( 1o evalSub S ) ` R ) : ( Base ` ( 1o mPoly U ) ) --> ( Base ` ( S ^s ( B ^m 1o ) ) ) )
18 14 17 syl 
 |-  ( ph -> ( ( 1o evalSub S ) ` R ) : ( Base ` ( 1o mPoly U ) ) --> ( Base ` ( S ^s ( B ^m 1o ) ) ) )
19 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
20 3 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
21 7 20 syl 
 |-  ( ph -> U e. Ring )
22 2 ply1ring 
 |-  ( U e. Ring -> W e. Ring )
23 21 22 syl 
 |-  ( ph -> W e. Ring )
24 2 ply1lmod 
 |-  ( U e. Ring -> W e. LMod )
25 21 24 syl 
 |-  ( ph -> W e. LMod )
26 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
27 eqid 
 |-  ( Base ` W ) = ( Base ` W )
28 5 19 23 25 26 27 asclf 
 |-  ( ph -> A : ( Base ` ( Scalar ` W ) ) --> ( Base ` W ) )
29 4 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
30 7 29 syl 
 |-  ( ph -> R C_ B )
31 3 4 ressbas2 
 |-  ( R C_ B -> R = ( Base ` U ) )
32 30 31 syl 
 |-  ( ph -> R = ( Base ` U ) )
33 2 ply1sca 
 |-  ( U e. Ring -> U = ( Scalar ` W ) )
34 21 33 syl 
 |-  ( ph -> U = ( Scalar ` W ) )
35 34 fveq2d 
 |-  ( ph -> ( Base ` U ) = ( Base ` ( Scalar ` W ) ) )
36 32 35 eqtrd 
 |-  ( ph -> R = ( Base ` ( Scalar ` W ) ) )
37 eqid 
 |-  ( PwSer1 ` U ) = ( PwSer1 ` U )
38 2 37 27 ply1bas 
 |-  ( Base ` W ) = ( Base ` ( 1o mPoly U ) )
39 38 a1i 
 |-  ( ph -> ( Base ` W ) = ( Base ` ( 1o mPoly U ) ) )
40 39 eqcomd 
 |-  ( ph -> ( Base ` ( 1o mPoly U ) ) = ( Base ` W ) )
41 36 40 feq23d 
 |-  ( ph -> ( A : R --> ( Base ` ( 1o mPoly U ) ) <-> A : ( Base ` ( Scalar ` W ) ) --> ( Base ` W ) ) )
42 28 41 mpbird 
 |-  ( ph -> A : R --> ( Base ` ( 1o mPoly U ) ) )
43 42 8 ffvelrnd 
 |-  ( ph -> ( A ` X ) e. ( Base ` ( 1o mPoly U ) ) )
44 fvco3 
 |-  ( ( ( ( 1o evalSub S ) ` R ) : ( Base ` ( 1o mPoly U ) ) --> ( Base ` ( S ^s ( B ^m 1o ) ) ) /\ ( A ` X ) e. ( Base ` ( 1o mPoly U ) ) ) -> ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) ` ( A ` X ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( ( 1o evalSub S ) ` R ) ` ( A ` X ) ) ) )
45 18 43 44 syl2anc 
 |-  ( ph -> ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) ` ( A ` X ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( ( 1o evalSub S ) ` R ) ` ( A ` X ) ) ) )
46 5 a1i 
 |-  ( ph -> A = ( algSc ` W ) )
47 eqid 
 |-  ( algSc ` W ) = ( algSc ` W )
48 2 47 ply1ascl 
 |-  ( algSc ` W ) = ( algSc ` ( 1o mPoly U ) )
49 46 48 eqtrdi 
 |-  ( ph -> A = ( algSc ` ( 1o mPoly U ) ) )
50 49 fveq1d 
 |-  ( ph -> ( A ` X ) = ( ( algSc ` ( 1o mPoly U ) ) ` X ) )
51 50 fveq2d 
 |-  ( ph -> ( ( ( 1o evalSub S ) ` R ) ` ( A ` X ) ) = ( ( ( 1o evalSub S ) ` R ) ` ( ( algSc ` ( 1o mPoly U ) ) ` X ) ) )
52 eqid 
 |-  ( algSc ` ( 1o mPoly U ) ) = ( algSc ` ( 1o mPoly U ) )
53 9 a1i 
 |-  ( ph -> 1o e. On )
54 10 11 3 4 52 53 6 7 8 evlssca 
 |-  ( ph -> ( ( ( 1o evalSub S ) ` R ) ` ( ( algSc ` ( 1o mPoly U ) ) ` X ) ) = ( ( B ^m 1o ) X. { X } ) )
55 51 54 eqtrd 
 |-  ( ph -> ( ( ( 1o evalSub S ) ` R ) ` ( A ` X ) ) = ( ( B ^m 1o ) X. { X } ) )
56 55 fveq2d 
 |-  ( ph -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( ( 1o evalSub S ) ` R ) ` ( A ` X ) ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( B ^m 1o ) X. { X } ) ) )
57 eqidd 
 |-  ( ph -> ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) = ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) )
58 coeq1 
 |-  ( x = ( ( B ^m 1o ) X. { X } ) -> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
59 58 adantl 
 |-  ( ( ph /\ x = ( ( B ^m 1o ) X. { X } ) ) -> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
60 30 8 sseldd 
 |-  ( ph -> X e. B )
61 fconst6g 
 |-  ( X e. B -> ( ( B ^m 1o ) X. { X } ) : ( B ^m 1o ) --> B )
62 60 61 syl 
 |-  ( ph -> ( ( B ^m 1o ) X. { X } ) : ( B ^m 1o ) --> B )
63 4 fvexi 
 |-  B e. _V
64 63 a1i 
 |-  ( ph -> B e. _V )
65 ovex 
 |-  ( B ^m 1o ) e. _V
66 65 a1i 
 |-  ( ph -> ( B ^m 1o ) e. _V )
67 64 66 elmapd 
 |-  ( ph -> ( ( ( B ^m 1o ) X. { X } ) e. ( B ^m ( B ^m 1o ) ) <-> ( ( B ^m 1o ) X. { X } ) : ( B ^m 1o ) --> B ) )
68 62 67 mpbird 
 |-  ( ph -> ( ( B ^m 1o ) X. { X } ) e. ( B ^m ( B ^m 1o ) ) )
69 snex 
 |-  { X } e. _V
70 65 69 xpex 
 |-  ( ( B ^m 1o ) X. { X } ) e. _V
71 70 a1i 
 |-  ( ph -> ( ( B ^m 1o ) X. { X } ) e. _V )
72 64 mptexd 
 |-  ( ph -> ( y e. B |-> ( 1o X. { y } ) ) e. _V )
73 coexg 
 |-  ( ( ( ( B ^m 1o ) X. { X } ) e. _V /\ ( y e. B |-> ( 1o X. { y } ) ) e. _V ) -> ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) e. _V )
74 71 72 73 syl2anc 
 |-  ( ph -> ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) e. _V )
75 57 59 68 74 fvmptd 
 |-  ( ph -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( B ^m 1o ) X. { X } ) ) = ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
76 fconst6g 
 |-  ( y e. B -> ( 1o X. { y } ) : 1o --> B )
77 76 adantl 
 |-  ( ( ph /\ y e. B ) -> ( 1o X. { y } ) : 1o --> B )
78 63 9 pm3.2i 
 |-  ( B e. _V /\ 1o e. On )
79 78 a1i 
 |-  ( ( ph /\ y e. B ) -> ( B e. _V /\ 1o e. On ) )
80 elmapg 
 |-  ( ( B e. _V /\ 1o e. On ) -> ( ( 1o X. { y } ) e. ( B ^m 1o ) <-> ( 1o X. { y } ) : 1o --> B ) )
81 79 80 syl 
 |-  ( ( ph /\ y e. B ) -> ( ( 1o X. { y } ) e. ( B ^m 1o ) <-> ( 1o X. { y } ) : 1o --> B ) )
82 77 81 mpbird 
 |-  ( ( ph /\ y e. B ) -> ( 1o X. { y } ) e. ( B ^m 1o ) )
83 eqidd 
 |-  ( ph -> ( y e. B |-> ( 1o X. { y } ) ) = ( y e. B |-> ( 1o X. { y } ) ) )
84 fconstmpt 
 |-  ( ( B ^m 1o ) X. { X } ) = ( z e. ( B ^m 1o ) |-> X )
85 84 a1i 
 |-  ( ph -> ( ( B ^m 1o ) X. { X } ) = ( z e. ( B ^m 1o ) |-> X ) )
86 eqidd 
 |-  ( z = ( 1o X. { y } ) -> X = X )
87 82 83 85 86 fmptco 
 |-  ( ph -> ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( y e. B |-> X ) )
88 75 87 eqtrd 
 |-  ( ph -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( B ^m 1o ) X. { X } ) ) = ( y e. B |-> X ) )
89 45 56 88 3eqtrd 
 |-  ( ph -> ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) ` ( A ` X ) ) = ( y e. B |-> X ) )
90 elpwg 
 |-  ( R e. ( SubRing ` S ) -> ( R e. ~P B <-> R C_ B ) )
91 29 90 mpbird 
 |-  ( R e. ( SubRing ` S ) -> R e. ~P B )
92 7 91 syl 
 |-  ( ph -> R e. ~P B )
93 eqid 
 |-  ( 1o evalSub S ) = ( 1o evalSub S )
94 1 93 4 evls1fval 
 |-  ( ( S e. CRing /\ R e. ~P B ) -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) )
95 6 92 94 syl2anc 
 |-  ( ph -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) )
96 95 fveq1d 
 |-  ( ph -> ( Q ` ( A ` X ) ) = ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) ` ( A ` X ) ) )
97 fconstmpt 
 |-  ( B X. { X } ) = ( y e. B |-> X )
98 97 a1i 
 |-  ( ph -> ( B X. { X } ) = ( y e. B |-> X ) )
99 89 96 98 3eqtr4d 
 |-  ( ph -> ( Q ` ( A ` X ) ) = ( B X. { X } ) )