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 } ) )