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