Step | Hyp | Ref
| Expression |
1 | | crngring 19983 |
. . . 4
β’ (π
β CRing β π
β Ring) |
2 | 1 | ad2antrr 725 |
. . 3
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β π
β Ring) |
3 | | simplr 768 |
. . . . 5
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β π β π΅) |
4 | | zarclssn.1 |
. . . . 5
β’ π΅ = (LIdealβπ
) |
5 | 3, 4 | eleqtrdi 2848 |
. . . 4
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β π β (LIdealβπ
)) |
6 | | simpr 486 |
. . . . . 6
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β {π} = (πβπ)) |
7 | 3 | snn0d 4741 |
. . . . . 6
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β {π} β β
) |
8 | 6, 7 | eqnetrrd 3013 |
. . . . 5
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β (πβπ) β β
) |
9 | | simpll 766 |
. . . . . 6
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β π
β CRing) |
10 | | zarclsx.1 |
. . . . . . . 8
β’ π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
11 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
12 | 10, 11 | zarcls1 32490 |
. . . . . . 7
β’ ((π
β CRing β§ π β (LIdealβπ
)) β ((πβπ) = β
β π = (Baseβπ
))) |
13 | 12 | necon3bid 2989 |
. . . . . 6
β’ ((π
β CRing β§ π β (LIdealβπ
)) β ((πβπ) β β
β π β (Baseβπ
))) |
14 | 9, 5, 13 | syl2anc 585 |
. . . . 5
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β ((πβπ) β β
β π β (Baseβπ
))) |
15 | 8, 14 | mpbid 231 |
. . . 4
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β π β (Baseβπ
)) |
16 | | simpr 486 |
. . . . . . . . . . . 12
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β π β π) |
17 | 9 | ad5antr 733 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β π
β CRing) |
18 | | simplr 768 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β π β (MaxIdealβπ
)) |
19 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(LSSumβ(mulGrpβπ
)) = (LSSumβ(mulGrpβπ
)) |
20 | 19 | mxidlprm 32277 |
. . . . . . . . . . . . . 14
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β π β (PrmIdealβπ
)) |
21 | 17, 18, 20 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β π β (PrmIdealβπ
)) |
22 | | simp-4r 783 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β π β π) |
23 | 22, 16 | sstrd 3959 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β π β π) |
24 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
25 | | sseq1 3974 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π β π β π β π)) |
26 | 25 | rabbidv 3418 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π β π}) |
27 | 26 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π = π) β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π β π}) |
28 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . 20
β’
(PrmIdealβπ
)
β V |
29 | 28 | rabex 5294 |
. . . . . . . . . . . . . . . . . . 19
β’ {π β (PrmIdealβπ
) β£ π β π} β V |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β {π β (PrmIdealβπ
) β£ π β π} β V) |
31 | 24, 27, 5, 30 | fvmptd 6960 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β (πβπ) = {π β (PrmIdealβπ
) β£ π β π}) |
32 | 6, 31 | eqtr2d 2778 |
. . . . . . . . . . . . . . . 16
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β {π β (PrmIdealβπ
) β£ π β π} = {π}) |
33 | | rabeqsn 4632 |
. . . . . . . . . . . . . . . 16
β’ ({π β (PrmIdealβπ
) β£ π β π} = {π} β βπ((π β (PrmIdealβπ
) β§ π β π) β π = π)) |
34 | 32, 33 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β βπ((π β (PrmIdealβπ
) β§ π β π) β π = π)) |
35 | 34 | ad5antr 733 |
. . . . . . . . . . . . . 14
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β βπ((π β (PrmIdealβπ
) β§ π β π) β π = π)) |
36 | | vex 3452 |
. . . . . . . . . . . . . . 15
β’ π β V |
37 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β (PrmIdealβπ
) β π β (PrmIdealβπ
))) |
38 | | sseq2 3975 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β π β π β π)) |
39 | 37, 38 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π β (PrmIdealβπ
) β§ π β π) β (π β (PrmIdealβπ
) β§ π β π))) |
40 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π = π β π = π)) |
41 | 39, 40 | bibi12d 346 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π β (PrmIdealβπ
) β§ π β π) β π = π) β ((π β (PrmIdealβπ
) β§ π β π) β π = π))) |
42 | 36, 41 | spcv 3567 |
. . . . . . . . . . . . . 14
β’
(βπ((π β (PrmIdealβπ
) β§ π β π) β π = π) β ((π β (PrmIdealβπ
) β§ π β π) β π = π)) |
43 | 35, 42 | syl 17 |
. . . . . . . . . . . . 13
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β ((π β (PrmIdealβπ
) β§ π β π) β π = π)) |
44 | 21, 23, 43 | mpbi2and 711 |
. . . . . . . . . . . 12
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β π = π) |
45 | 16, 44 | sseqtrd 3989 |
. . . . . . . . . . 11
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β π β π) |
46 | 45, 22 | eqssd 3966 |
. . . . . . . . . 10
β’
((((((((π
β
CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β§ π β (MaxIdealβπ
)) β§ π β π) β π = π) |
47 | 1 | ad5antr 733 |
. . . . . . . . . . 11
β’
((((((π
β CRing
β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β π
β Ring) |
48 | | simpllr 775 |
. . . . . . . . . . 11
β’
((((((π
β CRing
β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β π β (LIdealβπ
)) |
49 | | simpr 486 |
. . . . . . . . . . . 12
β’
((((((π
β CRing
β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β Β¬ π = (Baseβπ
)) |
50 | 49 | neqned 2951 |
. . . . . . . . . . 11
β’
((((((π
β CRing
β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β π β (Baseβπ
)) |
51 | 11 | ssmxidl 32279 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ π β (LIdealβπ
) β§ π β (Baseβπ
)) β βπ β (MaxIdealβπ
)π β π) |
52 | 47, 48, 50, 51 | syl3anc 1372 |
. . . . . . . . . 10
β’
((((((π
β CRing
β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β βπ β (MaxIdealβπ
)π β π) |
53 | 46, 52 | r19.29a 3160 |
. . . . . . . . 9
β’
((((((π
β CRing
β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β§ Β¬ π = (Baseβπ
)) β π = π) |
54 | 53 | ex 414 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β (Β¬ π = (Baseβπ
) β π = π)) |
55 | 54 | orrd 862 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β (π = (Baseβπ
) β¨ π = π)) |
56 | 55 | orcomd 870 |
. . . . . 6
β’
(((((π
β CRing
β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β§ π β π) β (π = π β¨ π = (Baseβπ
))) |
57 | 56 | ex 414 |
. . . . 5
β’ ((((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β§ π β (LIdealβπ
)) β (π β π β (π = π β¨ π = (Baseβπ
)))) |
58 | 57 | ralrimiva 3144 |
. . . 4
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β βπ β (LIdealβπ
)(π β π β (π = π β¨ π = (Baseβπ
)))) |
59 | 5, 15, 58 | 3jca 1129 |
. . 3
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β (π β (LIdealβπ
) β§ π β (Baseβπ
) β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = (Baseβπ
))))) |
60 | 11 | ismxidl 32271 |
. . . 4
β’ (π
β Ring β (π β (MaxIdealβπ
) β (π β (LIdealβπ
) β§ π β (Baseβπ
) β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = (Baseβπ
)))))) |
61 | 60 | biimpar 479 |
. . 3
β’ ((π
β Ring β§ (π β (LIdealβπ
) β§ π β (Baseβπ
) β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = (Baseβπ
))))) β π β (MaxIdealβπ
)) |
62 | 2, 59, 61 | syl2anc 585 |
. 2
β’ (((π
β CRing β§ π β π΅) β§ {π} = (πβπ)) β π β (MaxIdealβπ
)) |
63 | 10 | a1i 11 |
. . . . 5
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
64 | 26 | adantl 483 |
. . . . 5
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ π = π) β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π β π}) |
65 | 11 | mxidlidl 32272 |
. . . . . 6
β’ ((π
β Ring β§ π β (MaxIdealβπ
)) β π β (LIdealβπ
)) |
66 | 1, 65 | sylan 581 |
. . . . 5
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β π β (LIdealβπ
)) |
67 | 29 | a1i 11 |
. . . . 5
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β {π β (PrmIdealβπ
) β£ π β π} β V) |
68 | 63, 64, 66, 67 | fvmptd 6960 |
. . . 4
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β (πβπ) = {π β (PrmIdealβπ
) β£ π β π}) |
69 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β π
β Ring) |
70 | | simplr 768 |
. . . . . . . . 9
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β π β (MaxIdealβπ
)) |
71 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β π β (PrmIdealβπ
)) |
72 | | prmidlidl 32256 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ π β (PrmIdealβπ
)) β π β (LIdealβπ
)) |
73 | 69, 71, 72 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β π β (LIdealβπ
)) |
74 | | simprr 772 |
. . . . . . . . . 10
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β π β π) |
75 | 73, 74 | jca 513 |
. . . . . . . . 9
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β (π β (LIdealβπ
) β§ π β π)) |
76 | 11 | mxidlmax 32274 |
. . . . . . . . 9
β’ (((π
β Ring β§ π β (MaxIdealβπ
)) β§ (π β (LIdealβπ
) β§ π β π)) β (π = π β¨ π = (Baseβπ
))) |
77 | 69, 70, 75, 76 | syl21anc 837 |
. . . . . . . 8
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β (π = π β¨ π = (Baseβπ
))) |
78 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.rβπ
) = (.rβπ
) |
79 | 11, 78 | prmidlnr 32251 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π β (PrmIdealβπ
)) β π β (Baseβπ
)) |
80 | 69, 71, 79 | syl2anc 585 |
. . . . . . . . 9
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β π β (Baseβπ
)) |
81 | 80 | neneqd 2949 |
. . . . . . . 8
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β Β¬ π = (Baseβπ
)) |
82 | 77, 81 | olcnd 876 |
. . . . . . 7
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ (π β (PrmIdealβπ
) β§ π β π)) β π = π) |
83 | | simpr 486 |
. . . . . . . . 9
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ π = π) β π = π) |
84 | 19 | mxidlprm 32277 |
. . . . . . . . . 10
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β π β (PrmIdealβπ
)) |
85 | 84 | adantr 482 |
. . . . . . . . 9
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ π = π) β π β (PrmIdealβπ
)) |
86 | 83, 85 | eqeltrd 2838 |
. . . . . . . 8
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ π = π) β π β (PrmIdealβπ
)) |
87 | | ssidd 3972 |
. . . . . . . . 9
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ π = π) β π β π) |
88 | 83, 87 | eqsstrrd 3988 |
. . . . . . . 8
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ π = π) β π β π) |
89 | 86, 88 | jca 513 |
. . . . . . 7
β’ (((π
β CRing β§ π β (MaxIdealβπ
)) β§ π = π) β (π β (PrmIdealβπ
) β§ π β π)) |
90 | 82, 89 | impbida 800 |
. . . . . 6
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β ((π β (PrmIdealβπ
) β§ π β π) β π = π)) |
91 | 90 | alrimiv 1931 |
. . . . 5
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β βπ((π β (PrmIdealβπ
) β§ π β π) β π = π)) |
92 | 91, 33 | sylibr 233 |
. . . 4
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β {π β (PrmIdealβπ
) β£ π β π} = {π}) |
93 | 68, 92 | eqtr2d 2778 |
. . 3
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β {π} = (πβπ)) |
94 | 93 | adantlr 714 |
. 2
β’ (((π
β CRing β§ π β π΅) β§ π β (MaxIdealβπ
)) β {π} = (πβπ)) |
95 | 62, 94 | impbida 800 |
1
β’ ((π
β CRing β§ π β π΅) β ({π} = (πβπ) β π β (MaxIdealβπ
))) |