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 = eval 1 R
evl1sca.p P = Poly 1 R
evl1sca.b B = Base R
evl1sca.a A = algSc P
Assertion evl1sca R CRing X B O A X = B × X

Proof

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