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 2 27 ply1bas 
 |-  ( Base ` W ) = ( Base ` ( 1o mPoly U ) )
38 37 a1i 
 |-  ( ph -> ( Base ` W ) = ( Base ` ( 1o mPoly U ) ) )
39 38 eqcomd 
 |-  ( ph -> ( Base ` ( 1o mPoly U ) ) = ( Base ` W ) )
40 36 39 feq23d 
 |-  ( ph -> ( A : R --> ( Base ` ( 1o mPoly U ) ) <-> A : ( Base ` ( Scalar ` W ) ) --> ( Base ` W ) ) )
41 28 40 mpbird 
 |-  ( ph -> A : R --> ( Base ` ( 1o mPoly U ) ) )
42 41 8 ffvelcdmd 
 |-  ( ph -> ( A ` X ) e. ( Base ` ( 1o mPoly U ) ) )
43 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 ) ) ) )
44 18 42 43 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 ) ) ) )
45 5 a1i 
 |-  ( ph -> A = ( algSc ` W ) )
46 eqid 
 |-  ( algSc ` W ) = ( algSc ` W )
47 2 46 ply1ascl 
 |-  ( algSc ` W ) = ( algSc ` ( 1o mPoly U ) )
48 45 47 eqtrdi 
 |-  ( ph -> A = ( algSc ` ( 1o mPoly U ) ) )
49 48 fveq1d 
 |-  ( ph -> ( A ` X ) = ( ( algSc ` ( 1o mPoly U ) ) ` X ) )
50 49 fveq2d 
 |-  ( ph -> ( ( ( 1o evalSub S ) ` R ) ` ( A ` X ) ) = ( ( ( 1o evalSub S ) ` R ) ` ( ( algSc ` ( 1o mPoly U ) ) ` X ) ) )
51 eqid 
 |-  ( algSc ` ( 1o mPoly U ) ) = ( algSc ` ( 1o mPoly U ) )
52 9 a1i 
 |-  ( ph -> 1o e. On )
53 10 11 3 4 51 52 6 7 8 evlssca 
 |-  ( ph -> ( ( ( 1o evalSub S ) ` R ) ` ( ( algSc ` ( 1o mPoly U ) ) ` X ) ) = ( ( B ^m 1o ) X. { X } ) )
54 50 53 eqtrd 
 |-  ( ph -> ( ( ( 1o evalSub S ) ` R ) ` ( A ` X ) ) = ( ( B ^m 1o ) X. { X } ) )
55 54 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 } ) ) )
56 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 } ) ) ) ) )
57 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 } ) ) ) )
58 57 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 } ) ) ) )
59 30 8 sseldd 
 |-  ( ph -> X e. B )
60 fconst6g 
 |-  ( X e. B -> ( ( B ^m 1o ) X. { X } ) : ( B ^m 1o ) --> B )
61 59 60 syl 
 |-  ( ph -> ( ( B ^m 1o ) X. { X } ) : ( B ^m 1o ) --> B )
62 4 fvexi 
 |-  B e. _V
63 62 a1i 
 |-  ( ph -> B e. _V )
64 ovex 
 |-  ( B ^m 1o ) e. _V
65 64 a1i 
 |-  ( ph -> ( B ^m 1o ) e. _V )
66 63 65 elmapd 
 |-  ( ph -> ( ( ( B ^m 1o ) X. { X } ) e. ( B ^m ( B ^m 1o ) ) <-> ( ( B ^m 1o ) X. { X } ) : ( B ^m 1o ) --> B ) )
67 61 66 mpbird 
 |-  ( ph -> ( ( B ^m 1o ) X. { X } ) e. ( B ^m ( B ^m 1o ) ) )
68 snex 
 |-  { X } e. _V
69 64 68 xpex 
 |-  ( ( B ^m 1o ) X. { X } ) e. _V
70 69 a1i 
 |-  ( ph -> ( ( B ^m 1o ) X. { X } ) e. _V )
71 63 mptexd 
 |-  ( ph -> ( y e. B |-> ( 1o X. { y } ) ) e. _V )
72 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 )
73 70 71 72 syl2anc 
 |-  ( ph -> ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) e. _V )
74 56 58 67 73 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 } ) ) ) )
75 fconst6g 
 |-  ( y e. B -> ( 1o X. { y } ) : 1o --> B )
76 75 adantl 
 |-  ( ( ph /\ y e. B ) -> ( 1o X. { y } ) : 1o --> B )
77 62 9 pm3.2i 
 |-  ( B e. _V /\ 1o e. On )
78 77 a1i 
 |-  ( ( ph /\ y e. B ) -> ( B e. _V /\ 1o e. On ) )
79 elmapg 
 |-  ( ( B e. _V /\ 1o e. On ) -> ( ( 1o X. { y } ) e. ( B ^m 1o ) <-> ( 1o X. { y } ) : 1o --> B ) )
80 78 79 syl 
 |-  ( ( ph /\ y e. B ) -> ( ( 1o X. { y } ) e. ( B ^m 1o ) <-> ( 1o X. { y } ) : 1o --> B ) )
81 76 80 mpbird 
 |-  ( ( ph /\ y e. B ) -> ( 1o X. { y } ) e. ( B ^m 1o ) )
82 eqidd 
 |-  ( ph -> ( y e. B |-> ( 1o X. { y } ) ) = ( y e. B |-> ( 1o X. { y } ) ) )
83 fconstmpt 
 |-  ( ( B ^m 1o ) X. { X } ) = ( z e. ( B ^m 1o ) |-> X )
84 83 a1i 
 |-  ( ph -> ( ( B ^m 1o ) X. { X } ) = ( z e. ( B ^m 1o ) |-> X ) )
85 eqidd 
 |-  ( z = ( 1o X. { y } ) -> X = X )
86 81 82 84 85 fmptco 
 |-  ( ph -> ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( y e. B |-> X ) )
87 74 86 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 ) )
88 44 55 87 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 ) )
89 elpwg 
 |-  ( R e. ( SubRing ` S ) -> ( R e. ~P B <-> R C_ B ) )
90 29 89 mpbird 
 |-  ( R e. ( SubRing ` S ) -> R e. ~P B )
91 7 90 syl 
 |-  ( ph -> R e. ~P B )
92 eqid 
 |-  ( 1o evalSub S ) = ( 1o evalSub S )
93 1 92 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 ) ) )
94 6 91 93 syl2anc 
 |-  ( ph -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) )
95 94 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 ) ) )
96 fconstmpt 
 |-  ( B X. { X } ) = ( y e. B |-> X )
97 96 a1i 
 |-  ( ph -> ( B X. { X } ) = ( y e. B |-> X ) )
98 88 95 97 3eqtr4d 
 |-  ( ph -> ( Q ` ( A ` X ) ) = ( B X. { X } ) )