Step | Hyp | Ref
| Expression |
1 | | isidom 20797 |
. . . 4
โข (๐
โ IDomn โ (๐
โ CRing โง ๐
โ Domn)) |
2 | 1 | simplbi 499 |
. . 3
โข (๐
โ IDomn โ ๐
โ CRing) |
3 | 1 | simprbi 498 |
. . . 4
โข (๐
โ IDomn โ ๐
โ Domn) |
4 | | domnnzr 20788 |
. . . 4
โข (๐
โ Domn โ ๐
โ NzRing) |
5 | 3, 4 | syl 17 |
. . 3
โข (๐
โ IDomn โ ๐
โ NzRing) |
6 | | fta1b.p |
. . . . 5
โข ๐ = (Poly1โ๐
) |
7 | | fta1b.b |
. . . . 5
โข ๐ต = (Baseโ๐) |
8 | | fta1b.d |
. . . . 5
โข ๐ท = ( deg1
โ๐
) |
9 | | fta1b.o |
. . . . 5
โข ๐ = (eval1โ๐
) |
10 | | fta1b.w |
. . . . 5
โข ๐ = (0gโ๐
) |
11 | | fta1b.z |
. . . . 5
โข 0 =
(0gโ๐) |
12 | | simpl 484 |
. . . . 5
โข ((๐
โ IDomn โง ๐ โ (๐ต โ { 0 })) โ ๐
โ IDomn) |
13 | | eldifsn 4751 |
. . . . . . 7
โข (๐ โ (๐ต โ { 0 }) โ (๐ โ ๐ต โง ๐ โ 0 )) |
14 | 13 | simplbi 499 |
. . . . . 6
โข (๐ โ (๐ต โ { 0 }) โ ๐ โ ๐ต) |
15 | 14 | adantl 483 |
. . . . 5
โข ((๐
โ IDomn โง ๐ โ (๐ต โ { 0 })) โ ๐ โ ๐ต) |
16 | 13 | simprbi 498 |
. . . . . 6
โข (๐ โ (๐ต โ { 0 }) โ ๐ โ 0 ) |
17 | 16 | adantl 483 |
. . . . 5
โข ((๐
โ IDomn โง ๐ โ (๐ต โ { 0 })) โ ๐ โ 0 ) |
18 | 6, 7, 8, 9, 10, 11, 12, 15, 17 | fta1g 25555 |
. . . 4
โข ((๐
โ IDomn โง ๐ โ (๐ต โ { 0 })) โ
(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) |
19 | 18 | ralrimiva 3140 |
. . 3
โข (๐
โ IDomn โ
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) |
20 | 2, 5, 19 | 3jca 1129 |
. 2
โข (๐
โ IDomn โ (๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐))) |
21 | | simp1 1137 |
. . 3
โข ((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โ ๐
โ CRing) |
22 | | simp2 1138 |
. . . 4
โข ((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โ ๐
โ NzRing) |
23 | | df-ne 2941 |
. . . . . . . 8
โข (๐ฅ โ ๐ โ ยฌ ๐ฅ = ๐) |
24 | | eqid 2733 |
. . . . . . . . . 10
โข
(Baseโ๐
) =
(Baseโ๐
) |
25 | | eqid 2733 |
. . . . . . . . . 10
โข
(.rโ๐
) = (.rโ๐
) |
26 | | eqid 2733 |
. . . . . . . . . 10
โข
(var1โ๐
) = (var1โ๐
) |
27 | | eqid 2733 |
. . . . . . . . . 10
โข (
ยท๐ โ๐) = ( ยท๐
โ๐) |
28 | | simpll1 1213 |
. . . . . . . . . 10
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง ((๐ฅ(.rโ๐
)๐ฆ) = ๐ โง ๐ฅ โ ๐)) โ ๐
โ CRing) |
29 | | simplrl 776 |
. . . . . . . . . 10
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง ((๐ฅ(.rโ๐
)๐ฆ) = ๐ โง ๐ฅ โ ๐)) โ ๐ฅ โ (Baseโ๐
)) |
30 | | simplrr 777 |
. . . . . . . . . 10
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง ((๐ฅ(.rโ๐
)๐ฆ) = ๐ โง ๐ฅ โ ๐)) โ ๐ฆ โ (Baseโ๐
)) |
31 | | simprl 770 |
. . . . . . . . . 10
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง ((๐ฅ(.rโ๐
)๐ฆ) = ๐ โง ๐ฅ โ ๐)) โ (๐ฅ(.rโ๐
)๐ฆ) = ๐) |
32 | | simprr 772 |
. . . . . . . . . 10
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง ((๐ฅ(.rโ๐
)๐ฆ) = ๐ โง ๐ฅ โ ๐)) โ ๐ฅ โ ๐) |
33 | | simpll3 1215 |
. . . . . . . . . . 11
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง ((๐ฅ(.rโ๐
)๐ฆ) = ๐ โง ๐ฅ โ ๐)) โ โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) |
34 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ฅ( ยท๐
โ๐)(var1โ๐
)) โ (๐โ๐) = (๐โ(๐ฅ( ยท๐
โ๐)(var1โ๐
)))) |
35 | 34 | cnveqd 5835 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ฅ( ยท๐
โ๐)(var1โ๐
)) โ โก(๐โ๐) = โก(๐โ(๐ฅ( ยท๐
โ๐)(var1โ๐
)))) |
36 | 35 | imaeq1d 6016 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ฅ( ยท๐
โ๐)(var1โ๐
)) โ (โก(๐โ๐) โ {๐}) = (โก(๐โ(๐ฅ( ยท๐
โ๐)(var1โ๐
))) โ {๐})) |
37 | 36 | fveq2d 6850 |
. . . . . . . . . . . . 13
โข (๐ = (๐ฅ( ยท๐
โ๐)(var1โ๐
)) โ (โฏโ(โก(๐โ๐) โ {๐})) = (โฏโ(โก(๐โ(๐ฅ( ยท๐
โ๐)(var1โ๐
))) โ {๐}))) |
38 | | fveq2 6846 |
. . . . . . . . . . . . 13
โข (๐ = (๐ฅ( ยท๐
โ๐)(var1โ๐
)) โ (๐ทโ๐) = (๐ทโ(๐ฅ( ยท๐
โ๐)(var1โ๐
)))) |
39 | 37, 38 | breq12d 5122 |
. . . . . . . . . . . 12
โข (๐ = (๐ฅ( ยท๐
โ๐)(var1โ๐
)) โ ((โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐) โ (โฏโ(โก(๐โ(๐ฅ( ยท๐
โ๐)(var1โ๐
))) โ {๐})) โค (๐ทโ(๐ฅ( ยท๐
โ๐)(var1โ๐
))))) |
40 | 39 | rspccv 3580 |
. . . . . . . . . . 11
โข
(โ๐ โ
(๐ต โ { 0
})(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐) โ ((๐ฅ( ยท๐
โ๐)(var1โ๐
)) โ (๐ต โ { 0 }) โ
(โฏโ(โก(๐โ(๐ฅ( ยท๐
โ๐)(var1โ๐
))) โ {๐})) โค (๐ทโ(๐ฅ( ยท๐
โ๐)(var1โ๐
))))) |
41 | 33, 40 | syl 17 |
. . . . . . . . . 10
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง ((๐ฅ(.rโ๐
)๐ฆ) = ๐ โง ๐ฅ โ ๐)) โ ((๐ฅ( ยท๐
โ๐)(var1โ๐
)) โ (๐ต โ { 0 }) โ
(โฏโ(โก(๐โ(๐ฅ( ยท๐
โ๐)(var1โ๐
))) โ {๐})) โค (๐ทโ(๐ฅ( ยท๐
โ๐)(var1โ๐
))))) |
42 | 6, 7, 8, 9, 10, 11, 24, 25, 26, 27, 28, 29, 30, 31, 32, 41 | fta1blem 25556 |
. . . . . . . . 9
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง ((๐ฅ(.rโ๐
)๐ฆ) = ๐ โง ๐ฅ โ ๐)) โ ๐ฆ = ๐) |
43 | 42 | expr 458 |
. . . . . . . 8
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง (๐ฅ(.rโ๐
)๐ฆ) = ๐) โ (๐ฅ โ ๐ โ ๐ฆ = ๐)) |
44 | 23, 43 | biimtrrid 242 |
. . . . . . 7
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง (๐ฅ(.rโ๐
)๐ฆ) = ๐) โ (ยฌ ๐ฅ = ๐ โ ๐ฆ = ๐)) |
45 | 44 | orrd 862 |
. . . . . 6
โข ((((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โง (๐ฅ(.rโ๐
)๐ฆ) = ๐) โ (๐ฅ = ๐ โจ ๐ฆ = ๐)) |
46 | 45 | ex 414 |
. . . . 5
โข (((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ ((๐ฅ(.rโ๐
)๐ฆ) = ๐ โ (๐ฅ = ๐ โจ ๐ฆ = ๐))) |
47 | 46 | ralrimivva 3194 |
. . . 4
โข ((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โ โ๐ฅ โ (Baseโ๐
)โ๐ฆ โ (Baseโ๐
)((๐ฅ(.rโ๐
)๐ฆ) = ๐ โ (๐ฅ = ๐ โจ ๐ฆ = ๐))) |
48 | 24, 25, 10 | isdomn 20787 |
. . . 4
โข (๐
โ Domn โ (๐
โ NzRing โง
โ๐ฅ โ
(Baseโ๐
)โ๐ฆ โ (Baseโ๐
)((๐ฅ(.rโ๐
)๐ฆ) = ๐ โ (๐ฅ = ๐ โจ ๐ฆ = ๐)))) |
49 | 22, 47, 48 | sylanbrc 584 |
. . 3
โข ((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โ ๐
โ Domn) |
50 | 21, 49, 1 | sylanbrc 584 |
. 2
โข ((๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐)) โ ๐
โ IDomn) |
51 | 20, 50 | impbii 208 |
1
โข (๐
โ IDomn โ (๐
โ CRing โง ๐
โ NzRing โง
โ๐ โ (๐ต โ { 0 })(โฏโ(โก(๐โ๐) โ {๐})) โค (๐ทโ๐))) |