Step | Hyp | Ref
| Expression |
1 | | crngring 19983 |
. . . . . . 7
β’ (π
β CRing β π
β Ring) |
2 | 1 | ad4antr 731 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π
β Ring) |
3 | | elpwi 4572 |
. . . . . . . . . . . 12
β’ (π β π«
(LIdealβπ
) β
π β
(LIdealβπ
)) |
4 | 3 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π
β CRing β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β π β (LIdealβπ
)) |
5 | 4 | adantr 482 |
. . . . . . . . . 10
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π β (LIdealβπ
)) |
6 | 5 | sselda 3949 |
. . . . . . . . 9
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π β π) β π β (LIdealβπ
)) |
7 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
8 | | eqid 2737 |
. . . . . . . . . 10
β’
(LIdealβπ
) =
(LIdealβπ
) |
9 | 7, 8 | lidlss 20696 |
. . . . . . . . 9
β’ (π β (LIdealβπ
) β π β (Baseβπ
)) |
10 | 6, 9 | syl 17 |
. . . . . . . 8
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π β π) β π β (Baseβπ
)) |
11 | 10 | ralrimiva 3144 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β βπ β π π β (Baseβπ
)) |
12 | | unissb 4905 |
. . . . . . 7
β’ (βͺ π
β (Baseβπ
)
β βπ β
π π β (Baseβπ
)) |
13 | 11, 12 | sylibr 233 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β βͺ π β (Baseβπ
)) |
14 | | eqid 2737 |
. . . . . . 7
β’
(RSpanβπ
) =
(RSpanβπ
) |
15 | 14, 7, 8 | rspcl 20708 |
. . . . . 6
β’ ((π
β Ring β§ βͺ π
β (Baseβπ
))
β ((RSpanβπ
)ββͺ π) β (LIdealβπ
)) |
16 | 2, 13, 15 | syl2anc 585 |
. . . . 5
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β ((RSpanβπ
)ββͺ π) β (LIdealβπ
)) |
17 | | sseq1 3974 |
. . . . . . . 8
β’ (π = ((RSpanβπ
)ββͺ π)
β (π β π β ((RSpanβπ
)ββͺ π)
β π)) |
18 | 17 | rabbidv 3418 |
. . . . . . 7
β’ (π = ((RSpanβπ
)ββͺ π)
β {π β
(PrmIdealβπ
) β£
π β π} = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π}) |
19 | 18 | eqeq2d 2748 |
. . . . . 6
β’ (π = ((RSpanβπ
)ββͺ π)
β (β© π = {π β (PrmIdealβπ
) β£ π β π} β β© π = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π})) |
20 | 19 | adantl 483 |
. . . . 5
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = ((RSpanβπ
)ββͺ π)) β (β© π =
{π β
(PrmIdealβπ
) β£
π β π} β β© π =
{π β
(PrmIdealβπ
) β£
((RSpanβπ
)ββͺ π) β π})) |
21 | | simpr 486 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π = (π β π)) |
22 | 21 | inteqd 4917 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© π = β©
(π β π)) |
23 | | zarclsx.1 |
. . . . . . . . . 10
β’ π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
24 | 23 | funmpt2 6545 |
. . . . . . . . 9
β’ Fun π |
25 | 24 | a1i 11 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β Fun π) |
26 | | fvex 6860 |
. . . . . . . . . . 11
β’
(PrmIdealβπ
)
β V |
27 | 26 | rabex 5294 |
. . . . . . . . . 10
β’ {π β (PrmIdealβπ
) β£ π β π} β V |
28 | 27, 23 | dmmpti 6650 |
. . . . . . . . 9
β’ dom π = (LIdealβπ
) |
29 | 5, 28 | sseqtrrdi 4000 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π β dom π) |
30 | | intimafv 31666 |
. . . . . . . 8
β’ ((Fun
π β§ π β dom π) β β© (π β π) = β© π β π (πβπ)) |
31 | 25, 29, 30 | syl2anc 585 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© (π β π) = β© π β π (πβπ)) |
32 | 22, 31 | eqtrd 2777 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© π = β© π β π (πβπ)) |
33 | | simplr 768 |
. . . . . . . . . 10
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β π = (π β π)) |
34 | | simpr 486 |
. . . . . . . . . . . 12
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β π = β
) |
35 | 34 | imaeq2d 6018 |
. . . . . . . . . . 11
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β (π β π) = (π β β
)) |
36 | | ima0 6034 |
. . . . . . . . . . 11
β’ (π β β
) =
β
|
37 | 35, 36 | eqtrdi 2793 |
. . . . . . . . . 10
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β (π β π) = β
) |
38 | 33, 37 | eqtrd 2777 |
. . . . . . . . 9
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β π = β
) |
39 | | simp-4r 783 |
. . . . . . . . . 10
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β π β β
) |
40 | 39 | neneqd 2949 |
. . . . . . . . 9
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β Β¬ π = β
) |
41 | 38, 40 | pm2.65da 816 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β Β¬ π = β
) |
42 | 41 | neqned 2951 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π β β
) |
43 | 23, 14 | zarclsiin 32492 |
. . . . . . 7
β’ ((π
β Ring β§ π β (LIdealβπ
) β§ π β β
) β β© π β π (πβπ) = (πβ((RSpanβπ
)ββͺ π))) |
44 | 2, 5, 42, 43 | syl3anc 1372 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β©
π β π (πβπ) = (πβ((RSpanβπ
)ββͺ π))) |
45 | 23 | a1i 11 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
46 | 18 | adantl 483 |
. . . . . . 7
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = ((RSpanβπ
)ββͺ π)) β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π}) |
47 | 26 | rabex 5294 |
. . . . . . . 8
β’ {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π)
β π} β
V |
48 | 47 | a1i 11 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π} β V) |
49 | 45, 46, 16, 48 | fvmptd 6960 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β (πβ((RSpanβπ
)ββͺ π)) = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π}) |
50 | 32, 44, 49 | 3eqtrd 2781 |
. . . . 5
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© π = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π}) |
51 | 16, 20, 50 | rspcedvd 3586 |
. . . 4
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β βπ β (LIdealβπ
)β© π = {π β (PrmIdealβπ
) β£ π β π}) |
52 | | intex 5299 |
. . . . . . . 8
β’ (π β β
β β© π
β V) |
53 | 52 | biimpi 215 |
. . . . . . 7
β’ (π β β
β β© π
β V) |
54 | 53 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π
β CRing β§ π β ran π β§ π β β
) β β© π
β V) |
55 | 23 | elrnmpt 5916 |
. . . . . 6
β’ (β© π
β V β (β© π β ran π β βπ β (LIdealβπ
)β© π = {π β (PrmIdealβπ
) β£ π β π})) |
56 | 54, 55 | syl 17 |
. . . . 5
β’ ((π
β CRing β§ π β ran π β§ π β β
) β (β© π
β ran π β
βπ β
(LIdealβπ
)β© π =
{π β
(PrmIdealβπ
) β£
π β π})) |
57 | 56 | ad5ant123 1365 |
. . . 4
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β (β© π β ran π β βπ β (LIdealβπ
)β© π = {π β (PrmIdealβπ
) β£ π β π})) |
58 | 51, 57 | mpbird 257 |
. . 3
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© π β ran π) |
59 | | fvexd 6862 |
. . . . . 6
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β (LIdealβπ
) β V) |
60 | 24 | a1i 11 |
. . . . . 6
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β Fun π) |
61 | | simplr 768 |
. . . . . . 7
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β π β ran π) |
62 | 27, 23 | fnmpti 6649 |
. . . . . . . 8
β’ π Fn (LIdealβπ
) |
63 | | fnima 6636 |
. . . . . . . 8
β’ (π Fn (LIdealβπ
) β (π β (LIdealβπ
)) = ran π) |
64 | 62, 63 | ax-mp 5 |
. . . . . . 7
β’ (π β (LIdealβπ
)) = ran π |
65 | 61, 64 | sseqtrrdi 4000 |
. . . . . 6
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β π β (π β (LIdealβπ
))) |
66 | | ssimaexg 6932 |
. . . . . 6
β’
(((LIdealβπ
)
β V β§ Fun π β§
π β (π β (LIdealβπ
))) β βπ(π β (LIdealβπ
) β§ π = (π β π))) |
67 | 59, 60, 65, 66 | syl3anc 1372 |
. . . . 5
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β βπ(π β (LIdealβπ
) β§ π = (π β π))) |
68 | | vex 3452 |
. . . . . . . . . 10
β’ π β V |
69 | 68 | a1i 11 |
. . . . . . . . 9
β’ ((((π
β CRing β§ π β ran π) β§ π β β
) β§ π β (LIdealβπ
)) β π β V) |
70 | | simpr 486 |
. . . . . . . . 9
β’ ((((π
β CRing β§ π β ran π) β§ π β β
) β§ π β (LIdealβπ
)) β π β (LIdealβπ
)) |
71 | 69, 70 | elpwd 4571 |
. . . . . . . 8
β’ ((((π
β CRing β§ π β ran π) β§ π β β
) β§ π β (LIdealβπ
)) β π β π« (LIdealβπ
)) |
72 | 71 | ex 414 |
. . . . . . 7
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β (π β (LIdealβπ
) β π β π« (LIdealβπ
))) |
73 | 72 | anim1d 612 |
. . . . . 6
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β ((π β (LIdealβπ
) β§ π = (π β π)) β (π β π« (LIdealβπ
) β§ π = (π β π)))) |
74 | 73 | eximdv 1921 |
. . . . 5
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β (βπ(π β (LIdealβπ
) β§ π = (π β π)) β βπ(π β π« (LIdealβπ
) β§ π = (π β π)))) |
75 | 67, 74 | mpd 15 |
. . . 4
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β βπ(π β π« (LIdealβπ
) β§ π = (π β π))) |
76 | | df-rex 3075 |
. . . 4
β’
(βπ β
π« (LIdealβπ
)π = (π β π) β βπ(π β π« (LIdealβπ
) β§ π = (π β π))) |
77 | 75, 76 | sylibr 233 |
. . 3
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β βπ β π«
(LIdealβπ
)π = (π β π)) |
78 | 58, 77 | r19.29a 3160 |
. 2
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β β© π
β ran π) |
79 | 78 | 3impa 1111 |
1
β’ ((π
β CRing β§ π β ran π β§ π β β
) β β© π
β ran π) |