Metamath Proof Explorer


Theorem deg1leb

Description: Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1leb.d D = deg 1 R
deg1leb.p P = Poly 1 R
deg1leb.b B = Base P
deg1leb.y 0 ˙ = 0 R
deg1leb.a A = coe 1 F
Assertion deg1leb F B G * D F G x 0 G < x A x = 0 ˙

Proof

Step Hyp Ref Expression
1 deg1leb.d D = deg 1 R
2 deg1leb.p P = Poly 1 R
3 deg1leb.b B = Base P
4 deg1leb.y 0 ˙ = 0 R
5 deg1leb.a A = coe 1 F
6 1 deg1fval D = 1 𝑜 mDeg R
7 eqid 1 𝑜 mPoly R = 1 𝑜 mPoly R
8 eqid PwSer 1 R = PwSer 1 R
9 2 8 3 ply1bas B = Base 1 𝑜 mPoly R
10 psr1baslem 0 1 𝑜 = a 0 1 𝑜 | a -1 Fin
11 tdeglem2 b 0 1 𝑜 b = b 0 1 𝑜 fld b
12 6 7 9 4 10 11 mdegleb F B G * D F G y 0 1 𝑜 G < b 0 1 𝑜 b y F y = 0 ˙
13 df1o2 1 𝑜 =
14 nn0ex 0 V
15 0ex V
16 eqid b 0 1 𝑜 b = b 0 1 𝑜 b
17 13 14 15 16 mapsnf1o2 b 0 1 𝑜 b : 0 1 𝑜 1-1 onto 0
18 f1ofo b 0 1 𝑜 b : 0 1 𝑜 1-1 onto 0 b 0 1 𝑜 b : 0 1 𝑜 onto 0
19 breq2 b 0 1 𝑜 b y = x G < b 0 1 𝑜 b y G < x
20 fveqeq2 b 0 1 𝑜 b y = x A b 0 1 𝑜 b y = 0 ˙ A x = 0 ˙
21 19 20 imbi12d b 0 1 𝑜 b y = x G < b 0 1 𝑜 b y A b 0 1 𝑜 b y = 0 ˙ G < x A x = 0 ˙
22 21 cbvfo b 0 1 𝑜 b : 0 1 𝑜 onto 0 y 0 1 𝑜 G < b 0 1 𝑜 b y A b 0 1 𝑜 b y = 0 ˙ x 0 G < x A x = 0 ˙
23 17 18 22 mp2b y 0 1 𝑜 G < b 0 1 𝑜 b y A b 0 1 𝑜 b y = 0 ˙ x 0 G < x A x = 0 ˙
24 fveq1 b = y b = y
25 fvex y V
26 24 16 25 fvmpt y 0 1 𝑜 b 0 1 𝑜 b y = y
27 26 fveq2d y 0 1 𝑜 A b 0 1 𝑜 b y = A y
28 27 adantl F B G * y 0 1 𝑜 A b 0 1 𝑜 b y = A y
29 5 fvcoe1 F B y 0 1 𝑜 F y = A y
30 29 adantlr F B G * y 0 1 𝑜 F y = A y
31 28 30 eqtr4d F B G * y 0 1 𝑜 A b 0 1 𝑜 b y = F y
32 31 eqeq1d F B G * y 0 1 𝑜 A b 0 1 𝑜 b y = 0 ˙ F y = 0 ˙
33 32 imbi2d F B G * y 0 1 𝑜 G < b 0 1 𝑜 b y A b 0 1 𝑜 b y = 0 ˙ G < b 0 1 𝑜 b y F y = 0 ˙
34 33 ralbidva F B G * y 0 1 𝑜 G < b 0 1 𝑜 b y A b 0 1 𝑜 b y = 0 ˙ y 0 1 𝑜 G < b 0 1 𝑜 b y F y = 0 ˙
35 23 34 bitr3id F B G * x 0 G < x A x = 0 ˙ y 0 1 𝑜 G < b 0 1 𝑜 b y F y = 0 ˙
36 12 35 bitr4d F B G * D F G x 0 G < x A x = 0 ˙