Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . 4
β’ ((((π
β CRing β§ πΌ β (LIdealβπ
)) β§ (πβπΌ) = β
) β§ πΌ β π΅) β (πβπΌ) = β
) |
2 | | sseq2 3975 |
. . . . . . . . . 10
β’ (π = π β (πΌ β π β πΌ β π)) |
3 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(LSSumβ(mulGrpβπ
)) = (LSSumβ(mulGrpβπ
)) |
4 | 3 | mxidlprm 32277 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π β (MaxIdealβπ
)) β π β (PrmIdealβπ
)) |
5 | 4 | ad5ant14 757 |
. . . . . . . . . 10
β’
(((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β π β (PrmIdealβπ
)) |
6 | | simpr 486 |
. . . . . . . . . 10
β’
(((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β πΌ β π) |
7 | 2, 5, 6 | elrabd 3652 |
. . . . . . . . 9
β’
(((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β π β {π β (PrmIdealβπ
) β£ πΌ β π}) |
8 | | zarclsx.1 |
. . . . . . . . . . 11
β’ π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
9 | 8 | a1i 11 |
. . . . . . . . . 10
β’
(((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
10 | | sseq1 3974 |
. . . . . . . . . . . 12
β’ (π = πΌ β (π β π β πΌ β π)) |
11 | 10 | rabbidv 3418 |
. . . . . . . . . . 11
β’ (π = πΌ β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ πΌ β π}) |
12 | 11 | adantl 483 |
. . . . . . . . . 10
β’
((((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β§ π = πΌ) β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ πΌ β π}) |
13 | | simp-4r 783 |
. . . . . . . . . 10
β’
(((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β πΌ β (LIdealβπ
)) |
14 | | fvex 6860 |
. . . . . . . . . . . 12
β’
(PrmIdealβπ
)
β V |
15 | 14 | rabex 5294 |
. . . . . . . . . . 11
β’ {π β (PrmIdealβπ
) β£ πΌ β π} β V |
16 | 15 | a1i 11 |
. . . . . . . . . 10
β’
(((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β {π β (PrmIdealβπ
) β£ πΌ β π} β V) |
17 | 9, 12, 13, 16 | fvmptd 6960 |
. . . . . . . . 9
β’
(((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β (πβπΌ) = {π β (PrmIdealβπ
) β£ πΌ β π}) |
18 | 7, 17 | eleqtrrd 2841 |
. . . . . . . 8
β’
(((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β π β (πβπΌ)) |
19 | | ne0i 4299 |
. . . . . . . 8
β’ (π β (πβπΌ) β (πβπΌ) β β
) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’
(((((π
β CRing
β§ πΌ β
(LIdealβπ
)) β§
πΌ β π΅) β§ π β (MaxIdealβπ
)) β§ πΌ β π) β (πβπΌ) β β
) |
21 | | crngring 19983 |
. . . . . . . 8
β’ (π
β CRing β π
β Ring) |
22 | | zarcls1.1 |
. . . . . . . . . 10
β’ π΅ = (Baseβπ
) |
23 | 22 | ssmxidl 32279 |
. . . . . . . . 9
β’ ((π
β Ring β§ πΌ β (LIdealβπ
) β§ πΌ β π΅) β βπ β (MaxIdealβπ
)πΌ β π) |
24 | 23 | 3expa 1119 |
. . . . . . . 8
β’ (((π
β Ring β§ πΌ β (LIdealβπ
)) β§ πΌ β π΅) β βπ β (MaxIdealβπ
)πΌ β π) |
25 | 21, 24 | sylanl1 679 |
. . . . . . 7
β’ (((π
β CRing β§ πΌ β (LIdealβπ
)) β§ πΌ β π΅) β βπ β (MaxIdealβπ
)πΌ β π) |
26 | 20, 25 | r19.29a 3160 |
. . . . . 6
β’ (((π
β CRing β§ πΌ β (LIdealβπ
)) β§ πΌ β π΅) β (πβπΌ) β β
) |
27 | 26 | adantlr 714 |
. . . . 5
β’ ((((π
β CRing β§ πΌ β (LIdealβπ
)) β§ (πβπΌ) = β
) β§ πΌ β π΅) β (πβπΌ) β β
) |
28 | 27 | neneqd 2949 |
. . . 4
β’ ((((π
β CRing β§ πΌ β (LIdealβπ
)) β§ (πβπΌ) = β
) β§ πΌ β π΅) β Β¬ (πβπΌ) = β
) |
29 | 1, 28 | pm2.65da 816 |
. . 3
β’ (((π
β CRing β§ πΌ β (LIdealβπ
)) β§ (πβπΌ) = β
) β Β¬ πΌ β π΅) |
30 | | nne 2948 |
. . 3
β’ (Β¬
πΌ β π΅ β πΌ = π΅) |
31 | 29, 30 | sylib 217 |
. 2
β’ (((π
β CRing β§ πΌ β (LIdealβπ
)) β§ (πβπΌ) = β
) β πΌ = π΅) |
32 | | fveq2 6847 |
. . . 4
β’ (πΌ = π΅ β (πβπΌ) = (πβπ΅)) |
33 | 32 | adantl 483 |
. . 3
β’ (((π
β CRing β§ πΌ β (LIdealβπ
)) β§ πΌ = π΅) β (πβπΌ) = (πβπ΅)) |
34 | 8 | a1i 11 |
. . . . . . 7
β’ (π
β Ring β π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
35 | | sseq1 3974 |
. . . . . . . . 9
β’ (π = π΅ β (π β π β π΅ β π)) |
36 | 35 | adantl 483 |
. . . . . . . 8
β’ ((π
β Ring β§ π = π΅) β (π β π β π΅ β π)) |
37 | 36 | rabbidv 3418 |
. . . . . . 7
β’ ((π
β Ring β§ π = π΅) β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π΅ β π}) |
38 | | eqid 2737 |
. . . . . . . 8
β’
(LIdealβπ
) =
(LIdealβπ
) |
39 | 38, 22 | lidl1 20706 |
. . . . . . 7
β’ (π
β Ring β π΅ β (LIdealβπ
)) |
40 | 14 | rabex 5294 |
. . . . . . . 8
β’ {π β (PrmIdealβπ
) β£ π΅ β π} β V |
41 | 40 | a1i 11 |
. . . . . . 7
β’ (π
β Ring β {π β (PrmIdealβπ
) β£ π΅ β π} β V) |
42 | 34, 37, 39, 41 | fvmptd 6960 |
. . . . . 6
β’ (π
β Ring β (πβπ΅) = {π β (PrmIdealβπ
) β£ π΅ β π}) |
43 | | prmidlidl 32256 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π β (PrmIdealβπ
)) β π β (LIdealβπ
)) |
44 | 22, 38 | lidlss 20696 |
. . . . . . . . . . . 12
β’ (π β (LIdealβπ
) β π β π΅) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ π β (PrmIdealβπ
)) β π β π΅) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ π΅ β π) β π β π΅) |
47 | | simpr 486 |
. . . . . . . . . 10
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ π΅ β π) β π΅ β π) |
48 | 46, 47 | eqssd 3966 |
. . . . . . . . 9
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ π΅ β π) β π = π΅) |
49 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(.rβπ
) = (.rβπ
) |
50 | 22, 49 | prmidlnr 32251 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ π β (PrmIdealβπ
)) β π β π΅) |
51 | 50 | adantr 482 |
. . . . . . . . . 10
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ π΅ β π) β π β π΅) |
52 | 51 | neneqd 2949 |
. . . . . . . . 9
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ π΅ β π) β Β¬ π = π΅) |
53 | 48, 52 | pm2.65da 816 |
. . . . . . . 8
β’ ((π
β Ring β§ π β (PrmIdealβπ
)) β Β¬ π΅ β π) |
54 | 53 | ralrimiva 3144 |
. . . . . . 7
β’ (π
β Ring β
βπ β
(PrmIdealβπ
) Β¬
π΅ β π) |
55 | | rabeq0 4349 |
. . . . . . 7
β’ ({π β (PrmIdealβπ
) β£ π΅ β π} = β
β βπ β (PrmIdealβπ
) Β¬ π΅ β π) |
56 | 54, 55 | sylibr 233 |
. . . . . 6
β’ (π
β Ring β {π β (PrmIdealβπ
) β£ π΅ β π} = β
) |
57 | 42, 56 | eqtrd 2777 |
. . . . 5
β’ (π
β Ring β (πβπ΅) = β
) |
58 | 21, 57 | syl 17 |
. . . 4
β’ (π
β CRing β (πβπ΅) = β
) |
59 | 58 | ad2antrr 725 |
. . 3
β’ (((π
β CRing β§ πΌ β (LIdealβπ
)) β§ πΌ = π΅) β (πβπ΅) = β
) |
60 | 33, 59 | eqtrd 2777 |
. 2
β’ (((π
β CRing β§ πΌ β (LIdealβπ
)) β§ πΌ = π΅) β (πβπΌ) = β
) |
61 | 31, 60 | impbida 800 |
1
β’ ((π
β CRing β§ πΌ β (LIdealβπ
)) β ((πβπΌ) = β
β πΌ = π΅)) |