Metamath Proof Explorer


Theorem mon1pval

Description: Value of the set of monic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses uc1pval.p P = Poly 1 R
uc1pval.b B = Base P
uc1pval.z 0 ˙ = 0 P
uc1pval.d D = deg 1 R
mon1pval.m M = Monic 1p R
mon1pval.o 1 ˙ = 1 R
Assertion mon1pval M = f B | f 0 ˙ coe 1 f D f = 1 ˙

Proof

Step Hyp Ref Expression
1 uc1pval.p P = Poly 1 R
2 uc1pval.b B = Base P
3 uc1pval.z 0 ˙ = 0 P
4 uc1pval.d D = deg 1 R
5 mon1pval.m M = Monic 1p R
6 mon1pval.o 1 ˙ = 1 R
7 fveq2 r = R Poly 1 r = Poly 1 R
8 7 1 eqtr4di r = R Poly 1 r = P
9 8 fveq2d r = R Base Poly 1 r = Base P
10 9 2 eqtr4di r = R Base Poly 1 r = B
11 8 fveq2d r = R 0 Poly 1 r = 0 P
12 11 3 eqtr4di r = R 0 Poly 1 r = 0 ˙
13 12 neeq2d r = R f 0 Poly 1 r f 0 ˙
14 fveq2 r = R deg 1 r = deg 1 R
15 14 4 eqtr4di r = R deg 1 r = D
16 15 fveq1d r = R deg 1 r f = D f
17 16 fveq2d r = R coe 1 f deg 1 r f = coe 1 f D f
18 fveq2 r = R 1 r = 1 R
19 18 6 eqtr4di r = R 1 r = 1 ˙
20 17 19 eqeq12d r = R coe 1 f deg 1 r f = 1 r coe 1 f D f = 1 ˙
21 13 20 anbi12d r = R f 0 Poly 1 r coe 1 f deg 1 r f = 1 r f 0 ˙ coe 1 f D f = 1 ˙
22 10 21 rabeqbidv r = R f Base Poly 1 r | f 0 Poly 1 r coe 1 f deg 1 r f = 1 r = f B | f 0 ˙ coe 1 f D f = 1 ˙
23 df-mon1 Monic 1p = r V f Base Poly 1 r | f 0 Poly 1 r coe 1 f deg 1 r f = 1 r
24 2 fvexi B V
25 24 rabex f B | f 0 ˙ coe 1 f D f = 1 ˙ V
26 22 23 25 fvmpt R V Monic 1p R = f B | f 0 ˙ coe 1 f D f = 1 ˙
27 fvprc ¬ R V Monic 1p R =
28 ssrab2 f B | f 0 ˙ coe 1 f D f = 1 ˙ B
29 fvprc ¬ R V Poly 1 R =
30 1 29 syl5eq ¬ R V P =
31 30 fveq2d ¬ R V Base P = Base
32 2 31 syl5eq ¬ R V B = Base
33 base0 = Base
34 32 33 eqtr4di ¬ R V B =
35 28 34 sseqtrid ¬ R V f B | f 0 ˙ coe 1 f D f = 1 ˙
36 ss0 f B | f 0 ˙ coe 1 f D f = 1 ˙ f B | f 0 ˙ coe 1 f D f = 1 ˙ =
37 35 36 syl ¬ R V f B | f 0 ˙ coe 1 f D f = 1 ˙ =
38 27 37 eqtr4d ¬ R V Monic 1p R = f B | f 0 ˙ coe 1 f D f = 1 ˙
39 26 38 pm2.61i Monic 1p R = f B | f 0 ˙ coe 1 f D f = 1 ˙
40 5 39 eqtri M = f B | f 0 ˙ coe 1 f D f = 1 ˙