Metamath Proof Explorer


Theorem plyremlem

Description: Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis plyrem.1 G = X p f × A
Assertion plyremlem A G Poly deg G = 1 G -1 0 = A

Proof

Step Hyp Ref Expression
1 plyrem.1 G = X p f × A
2 ssid
3 ax-1cn 1
4 plyid 1 X p Poly
5 2 3 4 mp2an X p Poly
6 plyconst A × A Poly
7 2 6 mpan A × A Poly
8 plysubcl X p Poly × A Poly X p f × A Poly
9 5 7 8 sylancr A X p f × A Poly
10 1 9 eqeltrid A G Poly
11 negcl A A
12 addcom A z - A + z = z + A
13 11 12 sylan A z - A + z = z + A
14 negsub z A z + A = z A
15 14 ancoms A z z + A = z A
16 13 15 eqtrd A z - A + z = z A
17 16 mpteq2dva A z - A + z = z z A
18 cnex V
19 18 a1i A V
20 negex A V
21 20 a1i A z A V
22 simpr A z z
23 fconstmpt × A = z A
24 23 a1i A × A = z A
25 df-idp X p = I
26 mptresid I = z z
27 25 26 eqtri X p = z z
28 27 a1i A X p = z z
29 19 21 22 24 28 offval2 A × A + f X p = z - A + z
30 simpl A z A
31 fconstmpt × A = z A
32 31 a1i A × A = z A
33 19 22 30 28 32 offval2 A X p f × A = z z A
34 17 29 33 3eqtr4d A × A + f X p = X p f × A
35 34 1 eqtr4di A × A + f X p = G
36 35 fveq2d A deg × A + f X p = deg G
37 plyconst A × A Poly
38 2 11 37 sylancr A × A Poly
39 5 a1i A X p Poly
40 0dgr A deg × A = 0
41 11 40 syl A deg × A = 0
42 0lt1 0 < 1
43 41 42 eqbrtrdi A deg × A < 1
44 eqid deg × A = deg × A
45 dgrid deg X p = 1
46 45 eqcomi 1 = deg X p
47 44 46 dgradd2 × A Poly X p Poly deg × A < 1 deg × A + f X p = 1
48 38 39 43 47 syl3anc A deg × A + f X p = 1
49 36 48 eqtr3d A deg G = 1
50 1 33 syl5eq A G = z z A
51 50 fveq1d A G z = z z A z
52 51 adantr A z G z = z z A z
53 ovex z A V
54 eqid z z A = z z A
55 54 fvmpt2 z z A V z z A z = z A
56 22 53 55 sylancl A z z z A z = z A
57 52 56 eqtrd A z G z = z A
58 57 eqeq1d A z G z = 0 z A = 0
59 subeq0 z A z A = 0 z = A
60 59 ancoms A z z A = 0 z = A
61 58 60 bitrd A z G z = 0 z = A
62 61 pm5.32da A z G z = 0 z z = A
63 plyf G Poly G :
64 ffn G : G Fn
65 fniniseg G Fn z G -1 0 z G z = 0
66 10 63 64 65 4syl A z G -1 0 z G z = 0
67 eleq1a A z = A z
68 67 pm4.71rd A z = A z z = A
69 62 66 68 3bitr4d A z G -1 0 z = A
70 velsn z A z = A
71 69 70 bitr4di A z G -1 0 z A
72 71 eqrdv A G -1 0 = A
73 10 49 72 3jca A G Poly deg G = 1 G -1 0 = A