Step | Hyp | Ref
| Expression |
1 | | domnnzr 20910 |
. . 3
β’ (π
β Domn β π
β NzRing) |
2 | | ply1domn.p |
. . . 4
β’ π = (Poly1βπ
) |
3 | 2 | ply1nz 25638 |
. . 3
β’ (π
β NzRing β π β NzRing) |
4 | 1, 3 | syl 17 |
. 2
β’ (π
β Domn β π β NzRing) |
5 | | neanior 3035 |
. . . . 5
β’ ((π₯ β (0gβπ) β§ π¦ β (0gβπ)) β Β¬ (π₯ = (0gβπ) β¨ π¦ = (0gβπ))) |
6 | | eqid 2732 |
. . . . . . . . 9
β’ (
deg1 βπ
) =
( deg1 βπ
) |
7 | | eqid 2732 |
. . . . . . . . 9
β’
(RLRegβπ
) =
(RLRegβπ
) |
8 | | eqid 2732 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
9 | | eqid 2732 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
10 | | eqid 2732 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
11 | | domnring 20911 |
. . . . . . . . . 10
β’ (π
β Domn β π
β Ring) |
12 | 11 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π
β Ring) |
13 | | simplrl 775 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π₯ β (Baseβπ)) |
14 | | simprl 769 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π₯ β (0gβπ)) |
15 | | simpll 765 |
. . . . . . . . . 10
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π
β Domn) |
16 | | eqid 2732 |
. . . . . . . . . . 11
β’
(coe1βπ₯) = (coe1βπ₯) |
17 | 6, 2, 10, 8, 7, 16 | deg1ldgdomn 25611 |
. . . . . . . . . 10
β’ ((π
β Domn β§ π₯ β (Baseβπ) β§ π₯ β (0gβπ)) β ((coe1βπ₯)β(( deg1
βπ
)βπ₯)) β (RLRegβπ
)) |
18 | 15, 13, 14, 17 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β ((coe1βπ₯)β(( deg1
βπ
)βπ₯)) β (RLRegβπ
)) |
19 | | simplrr 776 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π¦ β (Baseβπ)) |
20 | | simprr 771 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π¦ β (0gβπ)) |
21 | 6, 2, 7, 8, 9, 10,
12, 13, 14, 18, 19, 20 | deg1mul2 25631 |
. . . . . . . 8
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) = ((( deg1 βπ
)βπ₯) + (( deg1 βπ
)βπ¦))) |
22 | 6, 2, 10, 8 | deg1nn0cl 25605 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π₯ β (Baseβπ) β§ π₯ β (0gβπ)) β (( deg1 βπ
)βπ₯) β
β0) |
23 | 12, 13, 14, 22 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (( deg1 βπ
)βπ₯) β
β0) |
24 | 6, 2, 10, 8 | deg1nn0cl 25605 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π¦ β (Baseβπ) β§ π¦ β (0gβπ)) β (( deg1 βπ
)βπ¦) β
β0) |
25 | 12, 19, 20, 24 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (( deg1 βπ
)βπ¦) β
β0) |
26 | 23, 25 | nn0addcld 12535 |
. . . . . . . 8
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β ((( deg1 βπ
)βπ₯) + (( deg1 βπ
)βπ¦)) β
β0) |
27 | 21, 26 | eqeltrd 2833 |
. . . . . . 7
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) β
β0) |
28 | 2 | ply1ring 21769 |
. . . . . . . . . . 11
β’ (π
β Ring β π β Ring) |
29 | 11, 28 | syl 17 |
. . . . . . . . . 10
β’ (π
β Domn β π β Ring) |
30 | 29 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β π β Ring) |
31 | 8, 9 | ringcl 20072 |
. . . . . . . . 9
β’ ((π β Ring β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
32 | 30, 13, 19, 31 | syl3anc 1371 |
. . . . . . . 8
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (π₯(.rβπ)π¦) β (Baseβπ)) |
33 | 6, 2, 10, 8 | deg1nn0clb 25607 |
. . . . . . . 8
β’ ((π
β Ring β§ (π₯(.rβπ)π¦) β (Baseβπ)) β ((π₯(.rβπ)π¦) β (0gβπ) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) β
β0)) |
34 | 12, 32, 33 | syl2anc 584 |
. . . . . . 7
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β ((π₯(.rβπ)π¦) β (0gβπ) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) β
β0)) |
35 | 27, 34 | mpbird 256 |
. . . . . 6
β’ (((π
β Domn β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π₯ β (0gβπ) β§ π¦ β (0gβπ))) β (π₯(.rβπ)π¦) β (0gβπ)) |
36 | 35 | ex 413 |
. . . . 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 3200 |
. 2
β’ (π
β Domn β
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((π₯(.rβπ)π¦) = (0gβπ) β (π₯ = (0gβπ) β¨ π¦ = (0gβπ)))) |
40 | 8, 9, 10 | isdomn 20909 |
. 2
β’ (π β Domn β (π β NzRing β§
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((π₯(.rβπ)π¦) = (0gβπ) β (π₯ = (0gβπ) β¨ π¦ = (0gβπ))))) |
41 | 4, 39, 40 | sylanbrc 583 |
1
β’ (π
β Domn β π β Domn) |