Metamath Proof Explorer


Theorem uc1pval

Description: Value of the set of unitic 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
uc1pval.c C = Unic 1p R
uc1pval.u U = Unit R
Assertion uc1pval C = f B | f 0 ˙ coe 1 f D f U

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 uc1pval.c C = Unic 1p R
6 uc1pval.u U = Unit 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 Unit r = Unit R
19 18 6 eqtr4di r = R Unit r = U
20 17 19 eleq12d r = R coe 1 f deg 1 r f Unit r coe 1 f D f U
21 13 20 anbi12d r = R f 0 Poly 1 r coe 1 f deg 1 r f Unit r f 0 ˙ coe 1 f D f U
22 10 21 rabeqbidv r = R f Base Poly 1 r | f 0 Poly 1 r coe 1 f deg 1 r f Unit r = f B | f 0 ˙ coe 1 f D f U
23 df-uc1p Unic 1p = r V f Base Poly 1 r | f 0 Poly 1 r coe 1 f deg 1 r f Unit r
24 2 fvexi B V
25 24 rabex f B | f 0 ˙ coe 1 f D f U V
26 22 23 25 fvmpt R V Unic 1p R = f B | f 0 ˙ coe 1 f D f U
27 fvprc ¬ R V Unic 1p R =
28 ssrab2 f B | f 0 ˙ coe 1 f D f U B
29 fvprc ¬ R V Poly 1 R =
30 1 29 syl5eq ¬ R V P =
31 30 fveq2d ¬ R V Base P = Base
32 base0 = Base
33 31 32 eqtr4di ¬ R V Base P =
34 2 33 syl5eq ¬ R V B =
35 28 34 sseqtrid ¬ R V f B | f 0 ˙ coe 1 f D f U
36 ss0 f B | f 0 ˙ coe 1 f D f U f B | f 0 ˙ coe 1 f D f U =
37 35 36 syl ¬ R V f B | f 0 ˙ coe 1 f D f U =
38 27 37 eqtr4d ¬ R V Unic 1p R = f B | f 0 ˙ coe 1 f D f U
39 26 38 pm2.61i Unic 1p R = f B | f 0 ˙ coe 1 f D f U
40 5 39 eqtri C = f B | f 0 ˙ coe 1 f D f U