Metamath Proof Explorer


Theorem evl1sca

Description: Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1sca.o
|- O = ( eval1 ` R )
evl1sca.p
|- P = ( Poly1 ` R )
evl1sca.b
|- B = ( Base ` R )
evl1sca.a
|- A = ( algSc ` P )
Assertion evl1sca
|- ( ( R e. CRing /\ X e. B ) -> ( O ` ( A ` X ) ) = ( B X. { X } ) )

Proof

Step Hyp Ref Expression
1 evl1sca.o
 |-  O = ( eval1 ` R )
2 evl1sca.p
 |-  P = ( Poly1 ` R )
3 evl1sca.b
 |-  B = ( Base ` R )
4 evl1sca.a
 |-  A = ( algSc ` P )
5 crngring
 |-  ( R e. CRing -> R e. Ring )
6 5 adantr
 |-  ( ( R e. CRing /\ X e. B ) -> R e. Ring )
7 eqid
 |-  ( Base ` P ) = ( Base ` P )
8 2 4 3 7 ply1sclf
 |-  ( R e. Ring -> A : B --> ( Base ` P ) )
9 6 8 syl
 |-  ( ( R e. CRing /\ X e. B ) -> A : B --> ( Base ` P ) )
10 ffvelrn
 |-  ( ( A : B --> ( Base ` P ) /\ X e. B ) -> ( A ` X ) e. ( Base ` P ) )
11 9 10 sylancom
 |-  ( ( R e. CRing /\ X e. B ) -> ( A ` X ) e. ( Base ` P ) )
12 eqid
 |-  ( 1o eval R ) = ( 1o eval R )
13 eqid
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
14 eqid
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
15 2 14 7 ply1bas
 |-  ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
16 1 12 3 13 15 evl1val
 |-  ( ( R e. CRing /\ ( A ` X ) e. ( Base ` P ) ) -> ( O ` ( A ` X ) ) = ( ( ( 1o eval R ) ` ( A ` X ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
17 11 16 syldan
 |-  ( ( R e. CRing /\ X e. B ) -> ( O ` ( A ` X ) ) = ( ( ( 1o eval R ) ` ( A ` X ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
18 2 4 ply1ascl
 |-  A = ( algSc ` ( 1o mPoly R ) )
19 3 ressid
 |-  ( R e. CRing -> ( R |`s B ) = R )
20 19 adantr
 |-  ( ( R e. CRing /\ X e. B ) -> ( R |`s B ) = R )
21 20 oveq2d
 |-  ( ( R e. CRing /\ X e. B ) -> ( 1o mPoly ( R |`s B ) ) = ( 1o mPoly R ) )
22 21 fveq2d
 |-  ( ( R e. CRing /\ X e. B ) -> ( algSc ` ( 1o mPoly ( R |`s B ) ) ) = ( algSc ` ( 1o mPoly R ) ) )
23 18 22 eqtr4id
 |-  ( ( R e. CRing /\ X e. B ) -> A = ( algSc ` ( 1o mPoly ( R |`s B ) ) ) )
24 23 fveq1d
 |-  ( ( R e. CRing /\ X e. B ) -> ( A ` X ) = ( ( algSc ` ( 1o mPoly ( R |`s B ) ) ) ` X ) )
25 24 fveq2d
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( 1o eval R ) ` ( A ` X ) ) = ( ( 1o eval R ) ` ( ( algSc ` ( 1o mPoly ( R |`s B ) ) ) ` X ) ) )
26 12 3 evlval
 |-  ( 1o eval R ) = ( ( 1o evalSub R ) ` B )
27 eqid
 |-  ( 1o mPoly ( R |`s B ) ) = ( 1o mPoly ( R |`s B ) )
28 eqid
 |-  ( R |`s B ) = ( R |`s B )
29 eqid
 |-  ( algSc ` ( 1o mPoly ( R |`s B ) ) ) = ( algSc ` ( 1o mPoly ( R |`s B ) ) )
30 1on
 |-  1o e. On
31 30 a1i
 |-  ( ( R e. CRing /\ X e. B ) -> 1o e. On )
32 simpl
 |-  ( ( R e. CRing /\ X e. B ) -> R e. CRing )
33 3 subrgid
 |-  ( R e. Ring -> B e. ( SubRing ` R ) )
34 6 33 syl
 |-  ( ( R e. CRing /\ X e. B ) -> B e. ( SubRing ` R ) )
35 simpr
 |-  ( ( R e. CRing /\ X e. B ) -> X e. B )
36 26 27 28 3 29 31 32 34 35 evlssca
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( 1o eval R ) ` ( ( algSc ` ( 1o mPoly ( R |`s B ) ) ) ` X ) ) = ( ( B ^m 1o ) X. { X } ) )
37 25 36 eqtrd
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( 1o eval R ) ` ( A ` X ) ) = ( ( B ^m 1o ) X. { X } ) )
38 37 coeq1d
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( ( 1o eval R ) ` ( A ` X ) ) o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
39 df1o2
 |-  1o = { (/) }
40 3 fvexi
 |-  B e. _V
41 0ex
 |-  (/) e. _V
42 eqid
 |-  ( y e. B |-> ( 1o X. { y } ) ) = ( y e. B |-> ( 1o X. { y } ) )
43 39 40 41 42 mapsnf1o3
 |-  ( y e. B |-> ( 1o X. { y } ) ) : B -1-1-onto-> ( B ^m 1o )
44 f1of
 |-  ( ( y e. B |-> ( 1o X. { y } ) ) : B -1-1-onto-> ( B ^m 1o ) -> ( y e. B |-> ( 1o X. { y } ) ) : B --> ( B ^m 1o ) )
45 43 44 mp1i
 |-  ( ( R e. CRing /\ X e. B ) -> ( y e. B |-> ( 1o X. { y } ) ) : B --> ( B ^m 1o ) )
46 42 fmpt
 |-  ( A. y e. B ( 1o X. { y } ) e. ( B ^m 1o ) <-> ( y e. B |-> ( 1o X. { y } ) ) : B --> ( B ^m 1o ) )
47 45 46 sylibr
 |-  ( ( R e. CRing /\ X e. B ) -> A. y e. B ( 1o X. { y } ) e. ( B ^m 1o ) )
48 eqidd
 |-  ( ( R e. CRing /\ X e. B ) -> ( y e. B |-> ( 1o X. { y } ) ) = ( y e. B |-> ( 1o X. { y } ) ) )
49 fconstmpt
 |-  ( ( B ^m 1o ) X. { X } ) = ( x e. ( B ^m 1o ) |-> X )
50 49 a1i
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( B ^m 1o ) X. { X } ) = ( x e. ( B ^m 1o ) |-> X ) )
51 eqidd
 |-  ( x = ( 1o X. { y } ) -> X = X )
52 47 48 50 51 fmptcof
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( y e. B |-> X ) )
53 fconstmpt
 |-  ( B X. { X } ) = ( y e. B |-> X )
54 52 53 eqtr4di
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( ( B ^m 1o ) X. { X } ) o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( B X. { X } ) )
55 17 38 54 3eqtrd
 |-  ( ( R e. CRing /\ X e. B ) -> ( O ` ( A ` X ) ) = ( B X. { X } ) )