Step | Hyp | Ref
| Expression |
1 | | qsscn 12940 |
. . . . . 6
โข โ
โ โ |
2 | | eldifi 4125 |
. . . . . . . . . 10
โข (๐ โ ((Polyโโ)
โ {0๐}) โ ๐ โ
(Polyโโ)) |
3 | 2 | ad2antlr 725 |
. . . . . . . . 9
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ๐ โ
(Polyโโ)) |
4 | | zssq 12936 |
. . . . . . . . . 10
โข โค
โ โ |
5 | | 0z 12565 |
. . . . . . . . . 10
โข 0 โ
โค |
6 | 4, 5 | sselii 3978 |
. . . . . . . . 9
โข 0 โ
โ |
7 | | eqid 2732 |
. . . . . . . . . 10
โข
(coeffโ๐) =
(coeffโ๐) |
8 | 7 | coef2 25736 |
. . . . . . . . 9
โข ((๐ โ (Polyโโ)
โง 0 โ โ) โ (coeffโ๐):โ0โถโ) |
9 | 3, 6, 8 | sylancl 586 |
. . . . . . . 8
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (coeffโ๐):โ0โถโ) |
10 | | dgrcl 25738 |
. . . . . . . . 9
โข (๐ โ (Polyโโ)
โ (degโ๐) โ
โ0) |
11 | 3, 10 | syl 17 |
. . . . . . . 8
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (degโ๐) โ
โ0) |
12 | 9, 11 | ffvelcdmd 7084 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ((coeffโ๐)โ(degโ๐)) โ
โ) |
13 | | eldifsni 4792 |
. . . . . . . . 9
โข (๐ โ ((Polyโโ)
โ {0๐}) โ ๐ โ 0๐) |
14 | 13 | ad2antlr 725 |
. . . . . . . 8
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ๐ โ 0๐) |
15 | | eqid 2732 |
. . . . . . . . . . 11
โข
(degโ๐) =
(degโ๐) |
16 | 15, 7 | dgreq0 25770 |
. . . . . . . . . 10
โข (๐ โ (Polyโโ)
โ (๐ =
0๐ โ ((coeffโ๐)โ(degโ๐)) = 0)) |
17 | 16 | necon3bid 2985 |
. . . . . . . . 9
โข (๐ โ (Polyโโ)
โ (๐ โ
0๐ โ ((coeffโ๐)โ(degโ๐)) โ 0)) |
18 | 3, 17 | syl 17 |
. . . . . . . 8
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (๐ โ 0๐ โ
((coeffโ๐)โ(degโ๐)) โ 0)) |
19 | 14, 18 | mpbid 231 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ((coeffโ๐)โ(degโ๐)) โ 0) |
20 | | qreccl 12949 |
. . . . . . 7
โข
((((coeffโ๐)โ(degโ๐)) โ โ โง ((coeffโ๐)โ(degโ๐)) โ 0) โ (1 /
((coeffโ๐)โ(degโ๐))) โ โ) |
21 | 12, 19, 20 | syl2anc 584 |
. . . . . 6
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (1 / ((coeffโ๐)โ(degโ๐))) โ
โ) |
22 | | plyconst 25711 |
. . . . . 6
โข ((โ
โ โ โง (1 / ((coeffโ๐)โ(degโ๐))) โ โ) โ (โ ร
{(1 / ((coeffโ๐)โ(degโ๐)))}) โ
(Polyโโ)) |
23 | 1, 21, 22 | sylancr 587 |
. . . . 5
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โ
(Polyโโ)) |
24 | | simpl 483 |
. . . . . 6
โข
(((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โ (Polyโโ) โง ๐ โ (Polyโโ))
โ (โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โ
(Polyโโ)) |
25 | | simpr 485 |
. . . . . 6
โข
(((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โ (Polyโโ) โง ๐ โ (Polyโโ))
โ ๐ โ
(Polyโโ)) |
26 | | qaddcl 12945 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + ๐) โ โ) |
27 | 26 | adantl 482 |
. . . . . 6
โข
((((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โ (Polyโโ) โง ๐ โ (Polyโโ))
โง (๐ โ โ
โง ๐ โ โ))
โ (๐ + ๐) โ
โ) |
28 | | qmulcl 12947 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
29 | 28 | adantl 482 |
. . . . . 6
โข
((((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โ (Polyโโ) โง ๐ โ (Polyโโ))
โง (๐ โ โ
โง ๐ โ โ))
โ (๐ ยท ๐) โ
โ) |
30 | 24, 25, 27, 29 | plymul 25723 |
. . . . 5
โข
(((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โ (Polyโโ) โง ๐ โ (Polyโโ))
โ ((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ
(Polyโโ)) |
31 | 23, 3, 30 | syl2anc 584 |
. . . 4
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ
(Polyโโ)) |
32 | 7 | coef3 25737 |
. . . . . . . . 9
โข (๐ โ (Polyโโ)
โ (coeffโ๐):โ0โถโ) |
33 | 3, 32 | syl 17 |
. . . . . . . 8
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (coeffโ๐):โ0โถโ) |
34 | 33, 11 | ffvelcdmd 7084 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ((coeffโ๐)โ(degโ๐)) โ
โ) |
35 | 34, 19 | reccld 11979 |
. . . . . 6
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (1 / ((coeffโ๐)โ(degโ๐))) โ
โ) |
36 | 34, 19 | recne0d 11980 |
. . . . . 6
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (1 / ((coeffโ๐)โ(degโ๐))) โ 0) |
37 | | dgrmulc 25776 |
. . . . . 6
โข (((1 /
((coeffโ๐)โ(degโ๐))) โ โ โง (1 /
((coeffโ๐)โ(degโ๐))) โ 0 โง ๐ โ (Polyโโ)) โ
(degโ((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)) = (degโ๐)) |
38 | 35, 36, 3, 37 | syl3anc 1371 |
. . . . 5
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (degโ((โ ร
{(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)) = (degโ๐)) |
39 | | simprl 769 |
. . . . 5
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (degโ๐) = (degAAโ๐ด)) |
40 | 38, 39 | eqtrd 2772 |
. . . 4
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (degโ((โ ร
{(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)) =
(degAAโ๐ด)) |
41 | | aacn 25821 |
. . . . . . 7
โข (๐ด โ ๐ธ โ ๐ด โ
โ) |
42 | 41 | ad2antrr 724 |
. . . . . 6
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ๐ด โ โ) |
43 | | ovex 7438 |
. . . . . . . 8
โข (1 /
((coeffโ๐)โ(degโ๐))) โ V |
44 | | fnconstg 6776 |
. . . . . . . 8
โข ((1 /
((coeffโ๐)โ(degโ๐))) โ V โ (โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) Fn โ) |
45 | 43, 44 | mp1i 13 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) Fn โ) |
46 | | plyf 25703 |
. . . . . . . 8
โข (๐ โ (Polyโโ)
โ ๐:โโถโ) |
47 | | ffn 6714 |
. . . . . . . 8
โข (๐:โโถโ โ
๐ Fn
โ) |
48 | 3, 46, 47 | 3syl 18 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ๐ Fn โ) |
49 | | cnex 11187 |
. . . . . . . 8
โข โ
โ V |
50 | 49 | a1i 11 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ โ โ
V) |
51 | | inidm 4217 |
. . . . . . 7
โข (โ
โฉ โ) = โ |
52 | 43 | fvconst2 7201 |
. . . . . . . 8
โข (๐ด โ โ โ ((โ
ร {(1 / ((coeffโ๐)โ(degโ๐)))})โ๐ด) = (1 / ((coeffโ๐)โ(degโ๐)))) |
53 | 52 | adantl 482 |
. . . . . . 7
โข ((((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โง ๐ด โ โ) โ ((โ ร
{(1 / ((coeffโ๐)โ(degโ๐)))})โ๐ด) = (1 / ((coeffโ๐)โ(degโ๐)))) |
54 | | simplrr 776 |
. . . . . . 7
โข ((((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โง ๐ด โ โ) โ (๐โ๐ด) = 0) |
55 | 45, 48, 50, 50, 51, 53, 54 | ofval 7677 |
. . . . . 6
โข ((((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โง ๐ด โ โ) โ (((โ ร
{(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)โ๐ด) = ((1 / ((coeffโ๐)โ(degโ๐))) ยท 0)) |
56 | 42, 55 | mpdan 685 |
. . . . 5
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)โ๐ด) = ((1 / ((coeffโ๐)โ(degโ๐))) ยท 0)) |
57 | 35 | mul01d 11409 |
. . . . 5
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ((1 / ((coeffโ๐)โ(degโ๐))) ยท 0) =
0) |
58 | 56, 57 | eqtrd 2772 |
. . . 4
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)โ๐ด) = 0) |
59 | | coemulc 25760 |
. . . . . . 7
โข (((1 /
((coeffโ๐)โ(degโ๐))) โ โ โง ๐ โ (Polyโโ)) โ
(coeffโ((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)) = ((โ0
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท
(coeffโ๐))) |
60 | 35, 3, 59 | syl2anc 584 |
. . . . . 6
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (coeffโ((โ
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)) = ((โ0
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท
(coeffโ๐))) |
61 | 60 | fveq1d 6890 |
. . . . 5
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ((coeffโ((โ
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐))โ(degAAโ๐ด)) = (((โ0
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท
(coeffโ๐))โ(degAAโ๐ด))) |
62 | | dgraacl 41873 |
. . . . . . . 8
โข (๐ด โ ๐ธ โ
(degAAโ๐ด)
โ โ) |
63 | 62 | ad2antrr 724 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (degAAโ๐ด) โ
โ) |
64 | 63 | nnnn0d 12528 |
. . . . . 6
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (degAAโ๐ด) โ
โ0) |
65 | | fnconstg 6776 |
. . . . . . . 8
โข ((1 /
((coeffโ๐)โ(degโ๐))) โ V โ (โ0
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) Fn
โ0) |
66 | 43, 65 | mp1i 13 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (โ0 ร
{(1 / ((coeffโ๐)โ(degโ๐)))}) Fn
โ0) |
67 | 33 | ffnd 6715 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (coeffโ๐) Fn
โ0) |
68 | | nn0ex 12474 |
. . . . . . . 8
โข
โ0 โ V |
69 | 68 | a1i 11 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ โ0 โ
V) |
70 | | inidm 4217 |
. . . . . . 7
โข
(โ0 โฉ โ0) =
โ0 |
71 | 43 | fvconst2 7201 |
. . . . . . . 8
โข
((degAAโ๐ด) โ โ0 โ
((โ0 ร {(1 / ((coeffโ๐)โ(degโ๐)))})โ(degAAโ๐ด)) = (1 / ((coeffโ๐)โ(degโ๐)))) |
72 | 71 | adantl 482 |
. . . . . . 7
โข ((((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โง (degAAโ๐ด) โ โ0)
โ ((โ0 ร {(1 / ((coeffโ๐)โ(degโ๐)))})โ(degAAโ๐ด)) = (1 / ((coeffโ๐)โ(degโ๐)))) |
73 | | simplrl 775 |
. . . . . . . . 9
โข ((((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โง (degAAโ๐ด) โ โ0)
โ (degโ๐) =
(degAAโ๐ด)) |
74 | 73 | eqcomd 2738 |
. . . . . . . 8
โข ((((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โง (degAAโ๐ด) โ โ0)
โ (degAAโ๐ด) = (degโ๐)) |
75 | 74 | fveq2d 6892 |
. . . . . . 7
โข ((((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โง (degAAโ๐ด) โ โ0)
โ ((coeffโ๐)โ(degAAโ๐ด)) = ((coeffโ๐)โ(degโ๐))) |
76 | 66, 67, 69, 69, 70, 72, 75 | ofval 7677 |
. . . . . 6
โข ((((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โง (degAAโ๐ด) โ โ0)
โ (((โ0 ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท
(coeffโ๐))โ(degAAโ๐ด)) = ((1 / ((coeffโ๐)โ(degโ๐))) ยท ((coeffโ๐)โ(degโ๐)))) |
77 | 64, 76 | mpdan 685 |
. . . . 5
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ (((โ0
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท
(coeffโ๐))โ(degAAโ๐ด)) = ((1 / ((coeffโ๐)โ(degโ๐))) ยท ((coeffโ๐)โ(degโ๐)))) |
78 | 34, 19 | recid2d 11982 |
. . . . 5
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ((1 / ((coeffโ๐)โ(degโ๐))) ยท ((coeffโ๐)โ(degโ๐))) = 1) |
79 | 61, 77, 78 | 3eqtrd 2776 |
. . . 4
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ ((coeffโ((โ
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐))โ(degAAโ๐ด)) = 1) |
80 | | fveqeq2 6897 |
. . . . . 6
โข (๐ = ((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ ((degโ๐) =
(degAAโ๐ด)
โ (degโ((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)) =
(degAAโ๐ด))) |
81 | | fveq1 6887 |
. . . . . . 7
โข (๐ = ((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ (๐โ๐ด) = (((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)โ๐ด)) |
82 | 81 | eqeq1d 2734 |
. . . . . 6
โข (๐ = ((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ ((๐โ๐ด) = 0 โ (((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)โ๐ด) = 0)) |
83 | | fveq2 6888 |
. . . . . . . 8
โข (๐ = ((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ (coeffโ๐) = (coeffโ((โ
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐))) |
84 | 83 | fveq1d 6890 |
. . . . . . 7
โข (๐ = ((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ ((coeffโ๐)โ(degAAโ๐ด)) = ((coeffโ((โ
ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐))โ(degAAโ๐ด))) |
85 | 84 | eqeq1d 2734 |
. . . . . 6
โข (๐ = ((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ (((coeffโ๐)โ(degAAโ๐ด)) = 1 โ
((coeffโ((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐))โ(degAAโ๐ด)) = 1)) |
86 | 80, 82, 85 | 3anbi123d 1436 |
. . . . 5
โข (๐ = ((โ ร {(1 /
((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ (((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โ
((degโ((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)) =
(degAAโ๐ด)
โง (((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)โ๐ด) = 0 โง ((coeffโ((โ ร
{(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐))โ(degAAโ๐ด)) = 1))) |
87 | 86 | rspcev 3612 |
. . . 4
โข
((((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐) โ (Polyโโ)
โง ((degโ((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)) =
(degAAโ๐ด)
โง (((โ ร {(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐)โ๐ด) = 0 โง ((coeffโ((โ ร
{(1 / ((coeffโ๐)โ(degโ๐)))}) โf ยท ๐))โ(degAAโ๐ด)) = 1)) โ โ๐ โ
(Polyโโ)((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1)) |
88 | 31, 40, 58, 79, 87 | syl13anc 1372 |
. . 3
โข (((๐ด โ ๐ธ โง ๐ โ ((Polyโโ)
โ {0๐})) โง ((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0)) โ โ๐ โ (Polyโโ)((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1)) |
89 | | dgraalem 41872 |
. . . 4
โข (๐ด โ ๐ธ โ
((degAAโ๐ด)
โ โ โง โ๐ โ ((Polyโโ) โ
{0๐})((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0))) |
90 | 89 | simprd 496 |
. . 3
โข (๐ด โ ๐ธ โ
โ๐ โ
((Polyโโ) โ {0๐})((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0)) |
91 | 88, 90 | r19.29a 3162 |
. 2
โข (๐ด โ ๐ธ โ
โ๐ โ
(Polyโโ)((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1)) |
92 | | simp2 1137 |
. . . . . . . . . . 11
โข
(((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โ (๐โ๐ด) = 0) |
93 | | simp2 1137 |
. . . . . . . . . . 11
โข
(((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โ (๐โ๐ด) = 0) |
94 | 92, 93 | anim12i 613 |
. . . . . . . . . 10
โข
((((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1)) โ ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) |
95 | | plyf 25703 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (Polyโโ)
โ ๐:โโถโ) |
96 | 95 | ffnd 6715 |
. . . . . . . . . . . . . . 15
โข (๐ โ (Polyโโ)
โ ๐ Fn
โ) |
97 | 96 | ad2antrr 724 |
. . . . . . . . . . . . . 14
โข (((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) โ ๐ Fn โ) |
98 | 46 | ffnd 6715 |
. . . . . . . . . . . . . . 15
โข (๐ โ (Polyโโ)
โ ๐ Fn
โ) |
99 | 98 | ad2antlr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) โ ๐ Fn โ) |
100 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
โข (((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) โ โ โ
V) |
101 | | simplrl 775 |
. . . . . . . . . . . . . 14
โข ((((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) โง ๐ด โ โ) โ (๐โ๐ด) = 0) |
102 | | simplrr 776 |
. . . . . . . . . . . . . 14
โข ((((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) โง ๐ด โ โ) โ (๐โ๐ด) = 0) |
103 | 97, 99, 100, 100, 51, 101, 102 | ofval 7677 |
. . . . . . . . . . . . 13
โข ((((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) โง ๐ด โ โ) โ ((๐ โf โ ๐)โ๐ด) = (0 โ 0)) |
104 | 41, 103 | sylan2 593 |
. . . . . . . . . . . 12
โข ((((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) โง ๐ด โ ๐ธ) โ ((๐ โf โ
๐)โ๐ด) = (0 โ 0)) |
105 | | 0m0e0 12328 |
. . . . . . . . . . . 12
โข (0
โ 0) = 0 |
106 | 104, 105 | eqtrdi 2788 |
. . . . . . . . . . 11
โข ((((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) โง ๐ด โ ๐ธ) โ ((๐ โf โ
๐)โ๐ด) = 0) |
107 | 106 | ex 413 |
. . . . . . . . . 10
โข (((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((๐โ๐ด) = 0 โง (๐โ๐ด) = 0)) โ (๐ด โ ๐ธ โ ((๐ โf โ
๐)โ๐ด) = 0)) |
108 | 94, 107 | sylan2 593 |
. . . . . . . . 9
โข (((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ (๐ด โ ๐ธ โ ((๐ โf โ
๐)โ๐ด) = 0)) |
109 | 108 | com12 32 |
. . . . . . . 8
โข (๐ด โ ๐ธ โ
(((๐ โ
(Polyโโ) โง ๐ โ (Polyโโ)) โง
(((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ ((๐ โf โ
๐)โ๐ด) = 0)) |
110 | 109 | impl 456 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ ((๐ โf โ
๐)โ๐ด) = 0) |
111 | | simpll 765 |
. . . . . . . 8
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ ๐ด โ
๐ธ) |
112 | | simpl 483 |
. . . . . . . . . 10
โข ((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โ ๐ โ
(Polyโโ)) |
113 | | simpr 485 |
. . . . . . . . . 10
โข ((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โ ๐ โ
(Polyโโ)) |
114 | 26 | adantl 482 |
. . . . . . . . . 10
โข (((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง (๐ โ โ โง ๐ โ โ)) โ (๐ + ๐) โ โ) |
115 | 28 | adantl 482 |
. . . . . . . . . 10
โข (((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง (๐ โ โ โง ๐ โ โ)) โ (๐ ยท ๐) โ โ) |
116 | | 1z 12588 |
. . . . . . . . . . . 12
โข 1 โ
โค |
117 | | zq 12934 |
. . . . . . . . . . . 12
โข (1 โ
โค โ 1 โ โ) |
118 | | qnegcl 12946 |
. . . . . . . . . . . 12
โข (1 โ
โ โ -1 โ โ) |
119 | 116, 117,
118 | mp2b 10 |
. . . . . . . . . . 11
โข -1 โ
โ |
120 | 119 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โ -1 โ โ) |
121 | 112, 113,
114, 115, 120 | plysub 25724 |
. . . . . . . . 9
โข ((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โ (๐ โf โ ๐) โ
(Polyโโ)) |
122 | 121 | ad2antlr 725 |
. . . . . . . 8
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ (๐ โf โ
๐) โ
(Polyโโ)) |
123 | | simplrl 775 |
. . . . . . . . . 10
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ ๐ โ
(Polyโโ)) |
124 | | simplrr 776 |
. . . . . . . . . 10
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ ๐ โ
(Polyโโ)) |
125 | | simprr1 1221 |
. . . . . . . . . . 11
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
(degโ๐) =
(degAAโ๐ด)) |
126 | | simprl1 1218 |
. . . . . . . . . . 11
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
(degโ๐) =
(degAAโ๐ด)) |
127 | 125, 126 | eqtr4d 2775 |
. . . . . . . . . 10
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
(degโ๐) =
(degโ๐)) |
128 | 62 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
(degAAโ๐ด)
โ โ) |
129 | 126, 128 | eqeltrd 2833 |
. . . . . . . . . 10
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
(degโ๐) โ
โ) |
130 | | simprl3 1220 |
. . . . . . . . . . 11
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
((coeffโ๐)โ(degAAโ๐ด)) = 1) |
131 | 126 | fveq2d 6892 |
. . . . . . . . . . 11
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
((coeffโ๐)โ(degโ๐)) = ((coeffโ๐)โ(degAAโ๐ด))) |
132 | 126 | fveq2d 6892 |
. . . . . . . . . . . 12
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
((coeffโ๐)โ(degโ๐)) = ((coeffโ๐)โ(degAAโ๐ด))) |
133 | | simprr3 1223 |
. . . . . . . . . . . 12
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
((coeffโ๐)โ(degAAโ๐ด)) = 1) |
134 | 132, 133 | eqtrd 2772 |
. . . . . . . . . . 11
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
((coeffโ๐)โ(degโ๐)) = 1) |
135 | 130, 131,
134 | 3eqtr4d 2782 |
. . . . . . . . . 10
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
((coeffโ๐)โ(degโ๐)) = ((coeffโ๐)โ(degโ๐))) |
136 | | eqid 2732 |
. . . . . . . . . . 11
โข
(degโ๐) =
(degโ๐) |
137 | 136 | dgrsub2 41862 |
. . . . . . . . . 10
โข (((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โง ((degโ๐) = (degโ๐) โง (degโ๐) โ โ โง ((coeffโ๐)โ(degโ๐)) = ((coeffโ๐)โ(degโ๐)))) โ (degโ(๐ โf โ
๐)) < (degโ๐)) |
138 | 123, 124,
127, 129, 135, 137 | syl23anc 1377 |
. . . . . . . . 9
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
(degโ(๐
โf โ ๐)) < (degโ๐)) |
139 | 138, 126 | breqtrd 5173 |
. . . . . . . 8
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ
(degโ(๐
โf โ ๐)) < (degAAโ๐ด)) |
140 | | dgraa0p 41876 |
. . . . . . . 8
โข ((๐ด โ ๐ธ โง (๐ โf โ
๐) โ
(Polyโโ) โง (degโ(๐ โf โ ๐)) <
(degAAโ๐ด))
โ (((๐
โf โ ๐)โ๐ด) = 0 โ (๐ โf โ ๐) =
0๐)) |
141 | 111, 122,
139, 140 | syl3anc 1371 |
. . . . . . 7
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ (((๐ โf โ
๐)โ๐ด) = 0 โ (๐ โf โ ๐) =
0๐)) |
142 | 110, 141 | mpbid 231 |
. . . . . 6
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ (๐ โf โ
๐) =
0๐) |
143 | | df-0p 25178 |
. . . . . 6
โข
0๐ = (โ ร {0}) |
144 | 142, 143 | eqtrdi 2788 |
. . . . 5
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ (๐ โf โ
๐) = (โ ร
{0})) |
145 | | ofsubeq0 12205 |
. . . . . . . 8
โข ((โ
โ V โง ๐:โโถโ โง ๐:โโถโ) โ
((๐ โf
โ ๐) = (โ
ร {0}) โ ๐ =
๐)) |
146 | 49, 145 | mp3an1 1448 |
. . . . . . 7
โข ((๐:โโถโ โง
๐:โโถโ)
โ ((๐
โf โ ๐) = (โ ร {0}) โ ๐ = ๐)) |
147 | 95, 46, 146 | syl2an 596 |
. . . . . 6
โข ((๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ)) โ ((๐ โf โ ๐) = (โ ร {0}) โ
๐ = ๐)) |
148 | 147 | ad2antlr 725 |
. . . . 5
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ ((๐ โf โ
๐) = (โ ร {0})
โ ๐ = ๐)) |
149 | 144, 148 | mpbid 231 |
. . . 4
โข (((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โง (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) โ ๐ = ๐) |
150 | 149 | ex 413 |
. . 3
โข ((๐ด โ ๐ธ โง (๐ โ (Polyโโ)
โง ๐ โ
(Polyโโ))) โ ((((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1)) โ ๐ = ๐)) |
151 | 150 | ralrimivva 3200 |
. 2
โข (๐ด โ ๐ธ โ
โ๐ โ
(Polyโโ)โ๐ โ
(Polyโโ)((((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1)) โ ๐ = ๐)) |
152 | | fveqeq2 6897 |
. . . 4
โข (๐ = ๐ โ ((degโ๐) = (degAAโ๐ด) โ (degโ๐) = (degAAโ๐ด))) |
153 | | fveq1 6887 |
. . . . 5
โข (๐ = ๐ โ (๐โ๐ด) = (๐โ๐ด)) |
154 | 153 | eqeq1d 2734 |
. . . 4
โข (๐ = ๐ โ ((๐โ๐ด) = 0 โ (๐โ๐ด) = 0)) |
155 | | fveq2 6888 |
. . . . . 6
โข (๐ = ๐ โ (coeffโ๐) = (coeffโ๐)) |
156 | 155 | fveq1d 6890 |
. . . . 5
โข (๐ = ๐ โ ((coeffโ๐)โ(degAAโ๐ด)) = ((coeffโ๐)โ(degAAโ๐ด))) |
157 | 156 | eqeq1d 2734 |
. . . 4
โข (๐ = ๐ โ (((coeffโ๐)โ(degAAโ๐ด)) = 1 โ
((coeffโ๐)โ(degAAโ๐ด)) = 1)) |
158 | 152, 154,
157 | 3anbi123d 1436 |
. . 3
โข (๐ = ๐ โ (((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โ ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1))) |
159 | 158 | reu4 3726 |
. 2
โข
(โ!๐ โ
(Polyโโ)((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โ (โ๐ โ
(Polyโโ)((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง โ๐ โ
(Polyโโ)โ๐ โ
(Polyโโ)((((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1) โง ((degโ๐) =
(degAAโ๐ด)
โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1)) โ ๐ = ๐))) |
160 | 91, 151, 159 | sylanbrc 583 |
1
โข (๐ด โ ๐ธ โ
โ!๐ โ
(Polyโโ)((degโ๐) = (degAAโ๐ด) โง (๐โ๐ด) = 0 โง ((coeffโ๐)โ(degAAโ๐ด)) = 1)) |