Step | Hyp | Ref
| Expression |
1 | | mon1psubm.p |
. . . . 5
β’ π = (Poly1βπ
) |
2 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
3 | | mon1psubm.m |
. . . . 5
β’ π =
(Monic1pβπ
) |
4 | 1, 2, 3 | mon1pcl 25525 |
. . . 4
β’ (π₯ β π β π₯ β (Baseβπ)) |
5 | 4 | ssriv 3953 |
. . 3
β’ π β (Baseβπ) |
6 | 5 | a1i 11 |
. 2
β’ (π
β NzRing β π β (Baseβπ)) |
7 | | eqid 2737 |
. . . 4
β’
(1rβπ) = (1rβπ) |
8 | | eqid 2737 |
. . . 4
β’ (
deg1 βπ
) =
( deg1 βπ
) |
9 | 1, 7, 3, 8 | mon1pid 41561 |
. . 3
β’ (π
β NzRing β
((1rβπ)
β π β§ ((
deg1 βπ
)β(1rβπ)) = 0)) |
10 | 9 | simpld 496 |
. 2
β’ (π
β NzRing β
(1rβπ)
β π) |
11 | 1 | ply1nz 25502 |
. . . . . . 7
β’ (π
β NzRing β π β NzRing) |
12 | | nzrring 20747 |
. . . . . . 7
β’ (π β NzRing β π β Ring) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ (π
β NzRing β π β Ring) |
14 | 13 | adantr 482 |
. . . . 5
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β π β Ring) |
15 | 4 | ad2antrl 727 |
. . . . 5
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β π₯ β (Baseβπ)) |
16 | | simprr 772 |
. . . . . 6
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
17 | 5, 16 | sselid 3947 |
. . . . 5
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β π¦ β (Baseβπ)) |
18 | | eqid 2737 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
19 | 2, 18 | ringcl 19988 |
. . . . 5
β’ ((π β Ring β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
20 | 14, 15, 17, 19 | syl3anc 1372 |
. . . 4
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
21 | | eqid 2737 |
. . . . . . 7
β’
(RLRegβπ
) =
(RLRegβπ
) |
22 | | eqid 2737 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
23 | | nzrring 20747 |
. . . . . . . 8
β’ (π
β NzRing β π
β Ring) |
24 | 23 | adantr 482 |
. . . . . . 7
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β π
β Ring) |
25 | 1, 22, 3 | mon1pn0 25527 |
. . . . . . . 8
β’ (π₯ β π β π₯ β (0gβπ)) |
26 | 25 | ad2antrl 727 |
. . . . . . 7
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β π₯ β (0gβπ)) |
27 | | eqid 2737 |
. . . . . . . . . 10
β’
(1rβπ
) = (1rβπ
) |
28 | 8, 27, 3 | mon1pldg 25530 |
. . . . . . . . 9
β’ (π₯ β π β ((coe1βπ₯)β(( deg1
βπ
)βπ₯)) = (1rβπ
)) |
29 | 28 | ad2antrl 727 |
. . . . . . . 8
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((coe1βπ₯)β(( deg1
βπ
)βπ₯)) = (1rβπ
)) |
30 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Unitβπ
) =
(Unitβπ
) |
31 | 21, 30 | unitrrg 20779 |
. . . . . . . . . . 11
β’ (π
β Ring β
(Unitβπ
) β
(RLRegβπ
)) |
32 | 23, 31 | syl 17 |
. . . . . . . . . 10
β’ (π
β NzRing β
(Unitβπ
) β
(RLRegβπ
)) |
33 | 30, 27 | 1unit 20094 |
. . . . . . . . . . 11
β’ (π
β Ring β
(1rβπ
)
β (Unitβπ
)) |
34 | 23, 33 | syl 17 |
. . . . . . . . . 10
β’ (π
β NzRing β
(1rβπ
)
β (Unitβπ
)) |
35 | 32, 34 | sseldd 3950 |
. . . . . . . . 9
β’ (π
β NzRing β
(1rβπ
)
β (RLRegβπ
)) |
36 | 35 | adantr 482 |
. . . . . . . 8
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (1rβπ
) β (RLRegβπ
)) |
37 | 29, 36 | eqeltrd 2838 |
. . . . . . 7
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((coe1βπ₯)β(( deg1
βπ
)βπ₯)) β (RLRegβπ
)) |
38 | 1, 22, 3 | mon1pn0 25527 |
. . . . . . . 8
β’ (π¦ β π β π¦ β (0gβπ)) |
39 | 38 | ad2antll 728 |
. . . . . . 7
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β π¦ β (0gβπ)) |
40 | 8, 1, 21, 2, 18, 22, 24, 15, 26, 37, 17, 39 | deg1mul2 25495 |
. . . . . 6
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) = ((( deg1 βπ
)βπ₯) + (( deg1 βπ
)βπ¦))) |
41 | 8, 1, 22, 2 | deg1nn0cl 25469 |
. . . . . . . 8
β’ ((π
β Ring β§ π₯ β (Baseβπ) β§ π₯ β (0gβπ)) β (( deg1 βπ
)βπ₯) β
β0) |
42 | 24, 15, 26, 41 | syl3anc 1372 |
. . . . . . 7
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (( deg1 βπ
)βπ₯) β
β0) |
43 | 8, 1, 22, 2 | deg1nn0cl 25469 |
. . . . . . . 8
β’ ((π
β Ring β§ π¦ β (Baseβπ) β§ π¦ β (0gβπ)) β (( deg1 βπ
)βπ¦) β
β0) |
44 | 24, 17, 39, 43 | syl3anc 1372 |
. . . . . . 7
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (( deg1 βπ
)βπ¦) β
β0) |
45 | 42, 44 | nn0addcld 12484 |
. . . . . 6
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((( deg1 βπ
)βπ₯) + (( deg1 βπ
)βπ¦)) β
β0) |
46 | 40, 45 | eqeltrd 2838 |
. . . . 5
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) β
β0) |
47 | 8, 1, 22, 2 | deg1nn0clb 25471 |
. . . . . 6
β’ ((π
β Ring β§ (π₯(.rβπ)π¦) β (Baseβπ)) β ((π₯(.rβπ)π¦) β (0gβπ) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) β
β0)) |
48 | 24, 20, 47 | syl2anc 585 |
. . . . 5
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((π₯(.rβπ)π¦) β (0gβπ) β (( deg1 βπ
)β(π₯(.rβπ)π¦)) β
β0)) |
49 | 46, 48 | mpbird 257 |
. . . 4
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (π₯(.rβπ)π¦) β (0gβπ)) |
50 | 40 | fveq2d 6851 |
. . . . 5
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((coe1β(π₯(.rβπ)π¦))β(( deg1 βπ
)β(π₯(.rβπ)π¦))) = ((coe1β(π₯(.rβπ)π¦))β((( deg1 βπ
)βπ₯) + (( deg1 βπ
)βπ¦)))) |
51 | | eqid 2737 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
52 | 1, 18, 51, 2, 8, 22, 24, 15, 26, 17, 39 | coe1mul4 25481 |
. . . . . 6
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((coe1β(π₯(.rβπ)π¦))β((( deg1 βπ
)βπ₯) + (( deg1 βπ
)βπ¦))) = (((coe1βπ₯)β(( deg1
βπ
)βπ₯))(.rβπ
)((coe1βπ¦)β(( deg1
βπ
)βπ¦)))) |
53 | 8, 27, 3 | mon1pldg 25530 |
. . . . . . . . 9
β’ (π¦ β π β ((coe1βπ¦)β(( deg1
βπ
)βπ¦)) = (1rβπ
)) |
54 | 53 | ad2antll 728 |
. . . . . . . 8
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((coe1βπ¦)β(( deg1
βπ
)βπ¦)) = (1rβπ
)) |
55 | 29, 54 | oveq12d 7380 |
. . . . . . 7
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (((coe1βπ₯)β(( deg1
βπ
)βπ₯))(.rβπ
)((coe1βπ¦)β(( deg1
βπ
)βπ¦))) =
((1rβπ
)(.rβπ
)(1rβπ
))) |
56 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
57 | 56, 27 | ringidcl 19996 |
. . . . . . . . 9
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
58 | 56, 51, 27 | ringlidm 19999 |
. . . . . . . . 9
β’ ((π
β Ring β§
(1rβπ
)
β (Baseβπ
))
β ((1rβπ
)(.rβπ
)(1rβπ
)) = (1rβπ
)) |
59 | 23, 57, 58 | syl2anc2 586 |
. . . . . . . 8
β’ (π
β NzRing β
((1rβπ
)(.rβπ
)(1rβπ
)) = (1rβπ
)) |
60 | 59 | adantr 482 |
. . . . . . 7
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((1rβπ
)(.rβπ
)(1rβπ
)) = (1rβπ
)) |
61 | 55, 60 | eqtrd 2777 |
. . . . . 6
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (((coe1βπ₯)β(( deg1
βπ
)βπ₯))(.rβπ
)((coe1βπ¦)β(( deg1
βπ
)βπ¦))) = (1rβπ
)) |
62 | 52, 61 | eqtrd 2777 |
. . . . 5
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((coe1β(π₯(.rβπ)π¦))β((( deg1 βπ
)βπ₯) + (( deg1 βπ
)βπ¦))) = (1rβπ
)) |
63 | 50, 62 | eqtrd 2777 |
. . . 4
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β ((coe1β(π₯(.rβπ)π¦))β(( deg1 βπ
)β(π₯(.rβπ)π¦))) = (1rβπ
)) |
64 | 1, 2, 22, 8, 3, 27 | ismon1p 25523 |
. . . 4
β’ ((π₯(.rβπ)π¦) β π β ((π₯(.rβπ)π¦) β (Baseβπ) β§ (π₯(.rβπ)π¦) β (0gβπ) β§ ((coe1β(π₯(.rβπ)π¦))β(( deg1 βπ
)β(π₯(.rβπ)π¦))) = (1rβπ
))) |
65 | 20, 49, 63, 64 | syl3anbrc 1344 |
. . 3
β’ ((π
β NzRing β§ (π₯ β π β§ π¦ β π)) β (π₯(.rβπ)π¦) β π) |
66 | 65 | ralrimivva 3198 |
. 2
β’ (π
β NzRing β
βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π) |
67 | | mon1psubm.u |
. . . . 5
β’ π = (mulGrpβπ) |
68 | 67 | ringmgp 19977 |
. . . 4
β’ (π β Ring β π β Mnd) |
69 | 13, 68 | syl 17 |
. . 3
β’ (π
β NzRing β π β Mnd) |
70 | 67, 2 | mgpbas 19909 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
71 | 67, 7 | ringidval 19922 |
. . . 4
β’
(1rβπ) = (0gβπ) |
72 | 67, 18 | mgpplusg 19907 |
. . . 4
β’
(.rβπ) = (+gβπ) |
73 | 70, 71, 72 | issubm 18621 |
. . 3
β’ (π β Mnd β (π β (SubMndβπ) β (π β (Baseβπ) β§ (1rβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π))) |
74 | 69, 73 | syl 17 |
. 2
β’ (π
β NzRing β (π β (SubMndβπ) β (π β (Baseβπ) β§ (1rβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π))) |
75 | 6, 10, 66, 74 | mpbir3and 1343 |
1
β’ (π
β NzRing β π β (SubMndβπ)) |