Step | Hyp | Ref
| Expression |
1 | | simpllr 775 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π = {π β (PrmIdealβπ
) β£ π β π}) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β π = {π β (PrmIdealβπ
) β£ π β π}) |
2 | | simpr 486 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π = {π β (PrmIdealβπ
) β£ π β π}) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β π = {π β (PrmIdealβπ
) β£ π β π}) |
3 | 1, 2 | uneq12d 4129 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π = {π β (PrmIdealβπ
) β£ π β π}) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β (π βͺ π) = ({π β (PrmIdealβπ
) β£ π β π} βͺ {π β (PrmIdealβπ
) β£ π β π})) |
4 | | unrab 4270 |
. . . . . . . . . 10
β’ ({π β (PrmIdealβπ
) β£ π β π} βͺ {π β (PrmIdealβπ
) β£ π β π}) = {π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} |
5 | | zarclsx.1 |
. . . . . . . . . . 11
β’ π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
6 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(IDLsrgβπ
) =
(IDLsrgβπ
) |
7 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(LIdealβπ
) =
(LIdealβπ
) |
8 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(.rβ(IDLsrgβπ
)) =
(.rβ(IDLsrgβπ
)) |
9 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β π
β CRing) |
10 | 9 | crngringd 19984 |
. . . . . . . . . . . . 13
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β π
β Ring) |
11 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β π β (LIdealβπ
)) |
12 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β π β (LIdealβπ
)) |
13 | 6, 7, 8, 10, 11, 12 | idlsrgmulrcl 32292 |
. . . . . . . . . . . 12
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β (π(.rβ(IDLsrgβπ
))π) β (LIdealβπ
)) |
14 | | sseq1 3974 |
. . . . . . . . . . . . . . 15
β’ (π = (π(.rβ(IDLsrgβπ
))π) β (π β π β (π(.rβ(IDLsrgβπ
))π) β π)) |
15 | 14 | rabbidv 3418 |
. . . . . . . . . . . . . 14
β’ (π = (π(.rβ(IDLsrgβπ
))π) β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ (π(.rβ(IDLsrgβπ
))π) β π}) |
16 | 15 | eqeq2d 2748 |
. . . . . . . . . . . . 13
β’ (π = (π(.rβ(IDLsrgβπ
))π) β ({π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} = {π β (PrmIdealβπ
) β£ π β π} β {π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} = {π β (PrmIdealβπ
) β£ (π(.rβ(IDLsrgβπ
))π) β π})) |
17 | 16 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β§ π = (π(.rβ(IDLsrgβπ
))π)) β ({π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} = {π β (PrmIdealβπ
) β£ π β π} β {π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} = {π β (PrmIdealβπ
) β£ (π(.rβ(IDLsrgβπ
))π) β π})) |
18 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(.rβπ
) = (.rβπ
) |
19 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β π
β CRing) |
20 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β π β (LIdealβπ
)) |
21 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β π β (LIdealβπ
)) |
22 | 6, 7, 8, 18, 19, 20, 21 | idlsrgmulrss1 32293 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β (π(.rβ(IDLsrgβπ
))π) β π) |
23 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β π β π) |
24 | 22, 23 | sstrd 3959 |
. . . . . . . . . . . . . . 15
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β (π(.rβ(IDLsrgβπ
))π) β π) |
25 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β π
β Ring) |
26 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β π β (LIdealβπ
)) |
27 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β π β (LIdealβπ
)) |
28 | 6, 7, 8, 18, 25, 26, 27 | idlsrgmulrss2 32294 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β (π(.rβ(IDLsrgβπ
))π) β π) |
29 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β π β π) |
30 | 28, 29 | sstrd 3959 |
. . . . . . . . . . . . . . 15
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
π β π) β (π(.rβ(IDLsrgβπ
))π) β π) |
31 | 24, 30 | jaodan 957 |
. . . . . . . . . . . . . 14
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π β π β¨ π β π)) β (π(.rβ(IDLsrgβπ
))π) β π) |
32 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(LSSumβ(mulGrpβπ
)) = (LSSumβ(mulGrpβπ
)) |
33 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β π
β Ring) |
34 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β π β (PrmIdealβπ
)) |
35 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β π β (LIdealβπ
)) |
36 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β π β (LIdealβπ
)) |
37 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβπ
) =
(Baseβπ
) |
38 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
39 | 37, 7 | lidlss 20696 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (LIdealβπ
) β π β (Baseβπ
)) |
40 | 35, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β π β (Baseβπ
)) |
41 | 37, 7 | lidlss 20696 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (LIdealβπ
) β π β (Baseβπ
)) |
42 | 36, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β π β (Baseβπ
)) |
43 | 37, 38, 32, 33, 40, 42 | ringlsmss 32216 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β (π(LSSumβ(mulGrpβπ
))π) β (Baseβπ
)) |
44 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(RSpanβπ
) =
(RSpanβπ
) |
45 | 44, 37 | rspssid 20709 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
β Ring β§ (π(LSSumβ(mulGrpβπ
))π) β (Baseβπ
)) β (π(LSSumβ(mulGrpβπ
))π) β ((RSpanβπ
)β(π(LSSumβ(mulGrpβπ
))π))) |
46 | 33, 43, 45 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β (π(LSSumβ(mulGrpβπ
))π) β ((RSpanβπ
)β(π(LSSumβ(mulGrpβπ
))π))) |
47 | 6, 7, 8, 38, 32, 33, 35, 36 | idlsrgmulrval 32291 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β (π(.rβ(IDLsrgβπ
))π) = ((RSpanβπ
)β(π(LSSumβ(mulGrpβπ
))π))) |
48 | 46, 47 | sseqtrrd 3990 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β (π(LSSumβ(mulGrpβπ
))π) β (π(.rβ(IDLsrgβπ
))π)) |
49 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β (π(.rβ(IDLsrgβπ
))π) β π) |
50 | 48, 49 | sstrd 3959 |
. . . . . . . . . . . . . . 15
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β (π(LSSumβ(mulGrpβπ
))π) β π) |
51 | 32, 33, 34, 35, 36, 50 | idlmulssprm 32254 |
. . . . . . . . . . . . . 14
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π β
(LIdealβπ
)) β§
π β
(PrmIdealβπ
)) β§
(π(.rβ(IDLsrgβπ
))π) β π) β (π β π β¨ π β π)) |
52 | 31, 51 | impbida 800 |
. . . . . . . . . . . . 13
β’ ((((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β§ π β (PrmIdealβπ
)) β ((π β π β¨ π β π) β (π(.rβ(IDLsrgβπ
))π) β π)) |
53 | 52 | rabbidva 3417 |
. . . . . . . . . . . 12
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β {π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} = {π β (PrmIdealβπ
) β£ (π(.rβ(IDLsrgβπ
))π) β π}) |
54 | 13, 17, 53 | rspcedvd 3586 |
. . . . . . . . . . 11
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β βπ β (LIdealβπ
){π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} = {π β (PrmIdealβπ
) β£ π β π}) |
55 | | fvex 6860 |
. . . . . . . . . . . . 13
β’
(PrmIdealβπ
)
β V |
56 | 55 | rabex 5294 |
. . . . . . . . . . . 12
β’ {π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} β V |
57 | 56 | a1i 11 |
. . . . . . . . . . 11
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β {π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} β V) |
58 | 5, 54, 57 | elrnmptd 5921 |
. . . . . . . . . 10
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β {π β (PrmIdealβπ
) β£ (π β π β¨ π β π)} β ran π) |
59 | 4, 58 | eqeltrid 2842 |
. . . . . . . . 9
β’ (((π
β CRing β§ π β (LIdealβπ
)) β§ π β (LIdealβπ
)) β ({π β (PrmIdealβπ
) β£ π β π} βͺ {π β (PrmIdealβπ
) β£ π β π}) β ran π) |
60 | 59 | adantlr 714 |
. . . . . . . 8
β’ ((((π
β CRing β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β§ π β (LIdealβπ
)) β ({π β (PrmIdealβπ
) β£ π β π} βͺ {π β (PrmIdealβπ
) β£ π β π}) β ran π) |
61 | 60 | adantr 482 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π = {π β (PrmIdealβπ
) β£ π β π}) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β ({π β (PrmIdealβπ
) β£ π β π} βͺ {π β (PrmIdealβπ
) β£ π β π}) β ran π) |
62 | 3, 61 | eqeltrd 2838 |
. . . . . 6
β’
(((((π
β CRing
β§ π β
(LIdealβπ
)) β§
π = {π β (PrmIdealβπ
) β£ π β π}) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β (π βͺ π) β ran π) |
63 | 62 | adantl4r 754 |
. . . . 5
β’
((((((π
β CRing
β§ π β ran π) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β (π βͺ π) β ran π) |
64 | 55 | rabex 5294 |
. . . . . . . . 9
β’ {π β (PrmIdealβπ
) β£ π β π} β V |
65 | 5, 64 | elrnmpti 5920 |
. . . . . . . 8
β’ (π β ran π β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
66 | | sseq1 3974 |
. . . . . . . . . . 11
β’ (π = π β (π β π β π β π)) |
67 | 66 | rabbidv 3418 |
. . . . . . . . . 10
β’ (π = π β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π β π}) |
68 | 67 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π = π β (π = {π β (PrmIdealβπ
) β£ π β π} β π = {π β (PrmIdealβπ
) β£ π β π})) |
69 | 68 | cbvrexvw 3229 |
. . . . . . . 8
β’
(βπ β
(LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π} β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
70 | | biid 261 |
. . . . . . . 8
β’
(βπ β
(LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π} β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
71 | 65, 69, 70 | 3bitri 297 |
. . . . . . 7
β’ (π β ran π β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
72 | 71 | biimpi 215 |
. . . . . 6
β’ (π β ran π β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
73 | 72 | ad3antlr 730 |
. . . . 5
β’ ((((π
β CRing β§ π β ran π) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
74 | 63, 73 | r19.29a 3160 |
. . . 4
β’ ((((π
β CRing β§ π β ran π) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β (π βͺ π) β ran π) |
75 | 74 | adantl3r 749 |
. . 3
β’
(((((π
β CRing
β§ π β ran π) β§ π β ran π) β§ π β (LIdealβπ
)) β§ π = {π β (PrmIdealβπ
) β£ π β π}) β (π βͺ π) β ran π) |
76 | 5, 64 | elrnmpti 5920 |
. . . . . 6
β’ (π β ran π β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
77 | | sseq1 3974 |
. . . . . . . . 9
β’ (π = π β (π β π β π β π)) |
78 | 77 | rabbidv 3418 |
. . . . . . . 8
β’ (π = π β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ π β π}) |
79 | 78 | eqeq2d 2748 |
. . . . . . 7
β’ (π = π β (π = {π β (PrmIdealβπ
) β£ π β π} β π = {π β (PrmIdealβπ
) β£ π β π})) |
80 | 79 | cbvrexvw 3229 |
. . . . . 6
β’
(βπ β
(LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π} β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
81 | | biid 261 |
. . . . . 6
β’
(βπ β
(LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π} β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
82 | 76, 80, 81 | 3bitri 297 |
. . . . 5
β’ (π β ran π β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
83 | 82 | biimpi 215 |
. . . 4
β’ (π β ran π β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
84 | 83 | ad2antlr 726 |
. . 3
β’ (((π
β CRing β§ π β ran π) β§ π β ran π) β βπ β (LIdealβπ
)π = {π β (PrmIdealβπ
) β£ π β π}) |
85 | 75, 84 | r19.29a 3160 |
. 2
β’ (((π
β CRing β§ π β ran π) β§ π β ran π) β (π βͺ π) β ran π) |
86 | 85 | 3impa 1111 |
1
β’ ((π
β CRing β§ π β ran π β§ π β ran π) β (π βͺ π) β ran π) |