Step | Hyp | Ref
| Expression |
1 | | domnnzr 20788 |
. . 3
β’ (π
β Domn β π
β NzRing) |
2 | | ply1domn.p |
. . . 4
β’ π = (Poly1βπ
) |
3 | 2 | ply1nz 25509 |
. . 3
β’ (π
β NzRing β π β NzRing) |
4 | 1, 3 | syl 17 |
. 2
β’ (π
β Domn β π β NzRing) |
5 | | neanior 3034 |
. . . . 5
β’ ((π₯ β (0gβπ) β§ π¦ β (0gβπ)) β Β¬ (π₯ = (0gβπ) β¨ π¦ = (0gβπ))) |
6 | | eqid 2733 |
. . . . . . . . 9
β’ (
deg1 βπ
) =
( deg1 βπ
) |
7 | | eqid 2733 |
. . . . . . . . 9
β’
(RLRegβπ
) =
(RLRegβπ
) |
8 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
9 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
10 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
11 | | domnring 20789 |
. . . . . . . . . 10
β’ (π
β Domn β π
β Ring) |
12 | 11 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π
β Ring) |
13 | | simplrl 776 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π₯ β (Baseβπ)) |
14 | | simprl 770 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π₯ β (0gβπ)) |
15 | | simpll 766 |
. . . . . . . . . 10
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π
β Domn) |
16 | | eqid 2733 |
. . . . . . . . . . 11
β’
(coe1βπ₯) = (coe1βπ₯) |
17 | 6, 2, 10, 8, 7, 16 | deg1ldgdomn 25482 |
. . . . . . . . . 10
β’ ((π
β Domn β§ π₯ β (Baseβπ) β§ π₯ β (0gβπ)) β ((coe1βπ₯)β(( deg1
βπ
)βπ₯)) β (RLRegβπ
)) |
18 | 15, 13, 14, 17 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β ((coe1βπ₯)β(( deg1
βπ
)βπ₯)) β (RLRegβπ
)) |
19 | | simplrr 777 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π¦ β (Baseβπ)) |
20 | | simprr 772 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π¦ β (0gβπ)) |
21 | 6, 2, 7, 8, 9, 10,
12, 13, 14, 18, 19, 20 | deg1mul2 25502 |
. . . . . . . 8
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) = ((( deg1 βπ
)βπ₯) + (( deg1 βπ
)βπ¦))) |
22 | 6, 2, 10, 8 | deg1nn0cl 25476 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π₯ β (Baseβπ) β§ π₯ β (0gβπ)) β (( deg1 βπ
)βπ₯) β
β0) |
23 | 12, 13, 14, 22 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (( deg1 βπ
)βπ₯) β
β0) |
24 | 6, 2, 10, 8 | deg1nn0cl 25476 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π¦ β (Baseβπ) β§ π¦ β (0gβπ)) β (( deg1 βπ
)βπ¦) β
β0) |
25 | 12, 19, 20, 24 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (( deg1 βπ
)βπ¦) β
β0) |
26 | 23, 25 | nn0addcld 12485 |
. . . . . . . 8
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β ((( deg1 βπ
)βπ₯) + (( deg1 βπ
)βπ¦)) β
β0) |
27 | 21, 26 | eqeltrd 2834 |
. . . . . . 7
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) β
β0) |
28 | 2 | ply1ring 21642 |
. . . . . . . . . . 11
β’ (π
β Ring β π β Ring) |
29 | 11, 28 | syl 17 |
. . . . . . . . . 10
β’ (π
β Domn β π β Ring) |
30 | 29 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π β Ring) |
31 | 8, 9 | ringcl 19989 |
. . . . . . . . 9
β’ ((π β Ring β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
32 | 30, 13, 19, 31 | syl3anc 1372 |
. . . . . . . 8
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (π₯(.rβπ)π¦) β (Baseβπ)) |
33 | 6, 2, 10, 8 | deg1nn0clb 25478 |
. . . . . . . 8
β’ ((π
β Ring β§ (π₯(.rβπ)π¦) β (Baseβπ)) β ((π₯(.rβπ)π¦) β (0gβπ) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) β
β0)) |
34 | 12, 32, 33 | syl2anc 585 |
. . . . . . 7
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β ((π₯(.rβπ)π¦) β (0gβπ) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) β
β0)) |
35 | 27, 34 | mpbird 257 |
. . . . . 6
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (π₯(.rβπ)π¦) β (0gβπ)) |
36 | 35 | ex 414 |
. . . . 5
β’ ((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((π₯ β (0gβπ) β§ π¦ β (0gβπ)) β (π₯(.rβπ)π¦) β (0gβπ))) |
37 | 5, 36 | biimtrrid 242 |
. . . 4
β’ ((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (Β¬ (π₯ = (0gβπ) β¨ π¦ = (0gβπ)) β (π₯(.rβπ)π¦) β (0gβπ))) |
38 | 37 | necon4bd 2960 |
. . 3
β’ ((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β ((π₯(.rβπ)π¦) = (0gβπ) β (π₯ = (0gβπ) β¨ π¦ = (0gβπ)))) |
39 | 38 | ralrimivva 3194 |
. 2
β’ (π
β Domn β
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((π₯(.rβπ)π¦) = (0gβπ) β (π₯ = (0gβπ) β¨ π¦ = (0gβπ)))) |
40 | 8, 9, 10 | isdomn 20787 |
. 2
β’ (π β Domn β (π β NzRing β§
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((π₯(.rβπ)π¦) = (0gβπ) β (π₯ = (0gβπ) β¨ π¦ = (0gβπ))))) |
41 | 4, 39, 40 | sylanbrc 584 |
1
β’ (π
β Domn β π β Domn) |