Step | Hyp | Ref
| Expression |
1 | | crngring 20070 |
. . . . . . 7
β’ (π
β CRing β π
β Ring) |
2 | 1 | ad4antr 730 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π
β Ring) |
3 | | elpwi 4609 |
. . . . . . . . . . . 12
β’ (π β π«
(LIdealβπ
) β
π β
(LIdealβπ
)) |
4 | 3 | adantl 482 |
. . . . . . . . . . 11
β’ ((((π
β CRing β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β π β (LIdealβπ
)) |
5 | 4 | adantr 481 |
. . . . . . . . . 10
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π β (LIdealβπ
)) |
6 | 5 | sselda 3982 |
. . . . . . . . 9
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π β π) β π β (LIdealβπ
)) |
7 | | eqid 2732 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
8 | | eqid 2732 |
. . . . . . . . . 10
β’
(LIdealβπ
) =
(LIdealβπ
) |
9 | 7, 8 | lidlss 20839 |
. . . . . . . . 9
β’ (π β (LIdealβπ
) β π β (Baseβπ
)) |
10 | 6, 9 | syl 17 |
. . . . . . . 8
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π β π) β π β (Baseβπ
)) |
11 | 10 | ralrimiva 3146 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β βπ β π π β (Baseβπ
)) |
12 | | unissb 4943 |
. . . . . . 7
β’ (βͺ π
β (Baseβπ
)
β βπ β
π π β (Baseβπ
)) |
13 | 11, 12 | sylibr 233 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β βͺ π β (Baseβπ
)) |
14 | | eqid 2732 |
. . . . . . 7
β’
(RSpanβπ
) =
(RSpanβπ
) |
15 | 14, 7, 8 | rspcl 20853 |
. . . . . 6
β’ ((π
β Ring β§ βͺ π
β (Baseβπ
))
β ((RSpanβπ
)ββͺ π) β (LIdealβπ
)) |
16 | 2, 13, 15 | syl2anc 584 |
. . . . 5
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β ((RSpanβπ
)ββͺ π) β (LIdealβπ
)) |
17 | | sseq1 4007 |
. . . . . . . 8
β’ (π = ((RSpanβπ
)ββͺ π)
β (π β π β ((RSpanβπ
)ββͺ π)
β π)) |
18 | 17 | rabbidv 3440 |
. . . . . . 7
β’ (π = ((RSpanβπ
)ββͺ π)
β {π β
(PrmIdealβπ
) β£
π β π} = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π}) |
19 | 18 | eqeq2d 2743 |
. . . . . 6
β’ (π = ((RSpanβπ
)ββͺ π)
β (β© π = {π β (PrmIdealβπ
) β£ π β π} β β© π = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π})) |
20 | 19 | adantl 482 |
. . . . 5
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = ((RSpanβπ
)ββͺ π)) β (β© π =
{π β
(PrmIdealβπ
) β£
π β π} β β© π =
{π β
(PrmIdealβπ
) β£
((RSpanβπ
)ββͺ π) β π})) |
21 | | simpr 485 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π = (π β π)) |
22 | 21 | inteqd 4955 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© π = β©
(π β π)) |
23 | | zarclsx.1 |
. . . . . . . . . 10
β’ π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π}) |
24 | 23 | funmpt2 6587 |
. . . . . . . . 9
β’ Fun π |
25 | 24 | a1i 11 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β Fun π) |
26 | | fvex 6904 |
. . . . . . . . . . 11
β’
(PrmIdealβπ
)
β V |
27 | 26 | rabex 5332 |
. . . . . . . . . 10
β’ {π β (PrmIdealβπ
) β£ π β π} β V |
28 | 27, 23 | dmmpti 6694 |
. . . . . . . . 9
β’ dom π = (LIdealβπ
) |
29 | 5, 28 | sseqtrrdi 4033 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π β dom π) |
30 | | intimafv 31970 |
. . . . . . . 8
β’ ((Fun
π β§ π β dom π) β β© (π β π) = β© π β π (πβπ)) |
31 | 25, 29, 30 | syl2anc 584 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© (π β π) = β© π β π (πβπ)) |
32 | 22, 31 | eqtrd 2772 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© π = β© π β π (πβπ)) |
33 | | simplr 767 |
. . . . . . . . . 10
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β π = (π β π)) |
34 | | simpr 485 |
. . . . . . . . . . . 12
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β π = β
) |
35 | 34 | imaeq2d 6059 |
. . . . . . . . . . 11
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β (π β π) = (π β β
)) |
36 | | ima0 6076 |
. . . . . . . . . . 11
β’ (π β β
) =
β
|
37 | 35, 36 | eqtrdi 2788 |
. . . . . . . . . 10
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β (π β π) = β
) |
38 | 33, 37 | eqtrd 2772 |
. . . . . . . . 9
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β π = β
) |
39 | | simp-4r 782 |
. . . . . . . . . 10
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β π β β
) |
40 | 39 | neneqd 2945 |
. . . . . . . . 9
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = β
) β Β¬ π = β
) |
41 | 38, 40 | pm2.65da 815 |
. . . . . . . 8
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β Β¬ π = β
) |
42 | 41 | neqned 2947 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π β β
) |
43 | 23, 14 | zarclsiin 32920 |
. . . . . . 7
β’ ((π
β Ring β§ π β (LIdealβπ
) β§ π β β
) β β© π β π (πβπ) = (πβ((RSpanβπ
)ββͺ π))) |
44 | 2, 5, 42, 43 | syl3anc 1371 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β©
π β π (πβπ) = (πβ((RSpanβπ
)ββͺ π))) |
45 | 23 | a1i 11 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β π = (π β (LIdealβπ
) β¦ {π β (PrmIdealβπ
) β£ π β π})) |
46 | 18 | adantl 482 |
. . . . . . 7
β’
((((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β§ π = ((RSpanβπ
)ββͺ π)) β {π β (PrmIdealβπ
) β£ π β π} = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π}) |
47 | 26 | rabex 5332 |
. . . . . . . 8
β’ {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π)
β π} β
V |
48 | 47 | a1i 11 |
. . . . . . 7
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π} β V) |
49 | 45, 46, 16, 48 | fvmptd 7005 |
. . . . . 6
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β (πβ((RSpanβπ
)ββͺ π)) = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π}) |
50 | 32, 44, 49 | 3eqtrd 2776 |
. . . . 5
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© π = {π β (PrmIdealβπ
) β£ ((RSpanβπ
)ββͺ π) β π}) |
51 | 16, 20, 50 | rspcedvd 3614 |
. . . 4
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β βπ β (LIdealβπ
)β© π = {π β (PrmIdealβπ
) β£ π β π}) |
52 | | intex 5337 |
. . . . . . . 8
β’ (π β β
β β© π
β V) |
53 | 52 | biimpi 215 |
. . . . . . 7
β’ (π β β
β β© π
β V) |
54 | 53 | 3ad2ant3 1135 |
. . . . . 6
β’ ((π
β CRing β§ π β ran π β§ π β β
) β β© π
β V) |
55 | 23 | elrnmpt 5955 |
. . . . . 6
β’ (β© π
β V β (β© π β ran π β βπ β (LIdealβπ
)β© π = {π β (PrmIdealβπ
) β£ π β π})) |
56 | 54, 55 | syl 17 |
. . . . 5
β’ ((π
β CRing β§ π β ran π β§ π β β
) β (β© π
β ran π β
βπ β
(LIdealβπ
)β© π =
{π β
(PrmIdealβπ
) β£
π β π})) |
57 | 56 | ad5ant123 1364 |
. . . 4
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β (β© π β ran π β βπ β (LIdealβπ
)β© π = {π β (PrmIdealβπ
) β£ π β π})) |
58 | 51, 57 | mpbird 256 |
. . 3
β’
(((((π
β CRing
β§ π β ran π) β§ π β β
) β§ π β π« (LIdealβπ
)) β§ π = (π β π)) β β© π β ran π) |
59 | | fvexd 6906 |
. . . . . 6
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β (LIdealβπ
) β V) |
60 | 24 | a1i 11 |
. . . . . 6
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β Fun π) |
61 | | simplr 767 |
. . . . . . 7
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β π β ran π) |
62 | 27, 23 | fnmpti 6693 |
. . . . . . . 8
β’ π Fn (LIdealβπ
) |
63 | | fnima 6680 |
. . . . . . . 8
β’ (π Fn (LIdealβπ
) β (π β (LIdealβπ
)) = ran π) |
64 | 62, 63 | ax-mp 5 |
. . . . . . 7
β’ (π β (LIdealβπ
)) = ran π |
65 | 61, 64 | sseqtrrdi 4033 |
. . . . . 6
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β π β (π β (LIdealβπ
))) |
66 | | ssimaexg 6977 |
. . . . . 6
β’
(((LIdealβπ
)
β V β§ Fun π β§
π β (π β (LIdealβπ
))) β βπ(π β (LIdealβπ
) β§ π = (π β π))) |
67 | 59, 60, 65, 66 | syl3anc 1371 |
. . . . 5
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β βπ(π β (LIdealβπ
) β§ π = (π β π))) |
68 | | vex 3478 |
. . . . . . . . . 10
β’ π β V |
69 | 68 | a1i 11 |
. . . . . . . . 9
β’ ((((π
β CRing β§ π β ran π) β§ π β β
) β§ π β (LIdealβπ
)) β π β V) |
70 | | simpr 485 |
. . . . . . . . 9
β’ ((((π
β CRing β§ π β ran π) β§ π β β
) β§ π β (LIdealβπ
)) β π β (LIdealβπ
)) |
71 | 69, 70 | elpwd 4608 |
. . . . . . . 8
β’ ((((π
β CRing β§ π β ran π) β§ π β β
) β§ π β (LIdealβπ
)) β π β π« (LIdealβπ
)) |
72 | 71 | ex 413 |
. . . . . . 7
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β (π β (LIdealβπ
) β π β π« (LIdealβπ
))) |
73 | 72 | anim1d 611 |
. . . . . 6
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β ((π β (LIdealβπ
) β§ π = (π β π)) β (π β π« (LIdealβπ
) β§ π = (π β π)))) |
74 | 73 | eximdv 1920 |
. . . . 5
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β (βπ(π β (LIdealβπ
) β§ π = (π β π)) β βπ(π β π« (LIdealβπ
) β§ π = (π β π)))) |
75 | 67, 74 | mpd 15 |
. . . 4
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β βπ(π β π« (LIdealβπ
) β§ π = (π β π))) |
76 | | df-rex 3071 |
. . . 4
β’
(βπ β
π« (LIdealβπ
)π = (π β π) β βπ(π β π« (LIdealβπ
) β§ π = (π β π))) |
77 | 75, 76 | sylibr 233 |
. . 3
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β βπ β π«
(LIdealβπ
)π = (π β π)) |
78 | 58, 77 | r19.29a 3162 |
. 2
β’ (((π
β CRing β§ π β ran π) β§ π β β
) β β© π
β ran π) |
79 | 78 | 3impa 1110 |
1
β’ ((π
β CRing β§ π β ran π β§ π β β
) β β© π
β ran π) |