Step |
Hyp |
Ref |
Expression |
1 |
|
rspecbas.1 |
|- S = ( Spec ` R ) |
2 |
|
rspectopn.1 |
|- I = ( LIdeal ` R ) |
3 |
|
rspectopn.2 |
|- P = ( PrmIdeal ` R ) |
4 |
|
rspectopn.3 |
|- J = ran ( i e. I |-> { j e. P | -. i C_ j } ) |
5 |
|
rspecval |
|- ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) |
6 |
3
|
oveq2i |
|- ( ( IDLsrg ` R ) |`s P ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) |
7 |
5 1 6
|
3eqtr4g |
|- ( R e. Ring -> S = ( ( IDLsrg ` R ) |`s P ) ) |
8 |
7
|
fveq2d |
|- ( R e. Ring -> ( TopOpen ` S ) = ( TopOpen ` ( ( IDLsrg ` R ) |`s P ) ) ) |
9 |
|
eqid |
|- ( ( IDLsrg ` R ) |`s P ) = ( ( IDLsrg ` R ) |`s P ) |
10 |
|
eqid |
|- ( TopOpen ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) |
11 |
9 10
|
resstopn |
|- ( ( TopOpen ` ( IDLsrg ` R ) ) |`t P ) = ( TopOpen ` ( ( IDLsrg ` R ) |`s P ) ) |
12 |
8 11
|
eqtr4di |
|- ( R e. Ring -> ( TopOpen ` S ) = ( ( TopOpen ` ( IDLsrg ` R ) ) |`t P ) ) |
13 |
|
eqid |
|- ( IDLsrg ` R ) = ( IDLsrg ` R ) |
14 |
|
eqid |
|- ran ( i e. I |-> { j e. I | -. i C_ j } ) = ran ( i e. I |-> { j e. I | -. i C_ j } ) |
15 |
13 2 14
|
idlsrgtset |
|- ( R e. Ring -> ran ( i e. I |-> { j e. I | -. i C_ j } ) = ( TopSet ` ( IDLsrg ` R ) ) ) |
16 |
2
|
fvexi |
|- I e. _V |
17 |
16
|
rabex |
|- { j e. I | -. i C_ j } e. _V |
18 |
17
|
a1i |
|- ( ( R e. Ring /\ i e. I ) -> { j e. I | -. i C_ j } e. _V ) |
19 |
|
simp2 |
|- ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> j e. I ) |
20 |
13 2
|
idlsrgbas |
|- ( R e. Ring -> I = ( Base ` ( IDLsrg ` R ) ) ) |
21 |
20
|
adantr |
|- ( ( R e. Ring /\ i e. I ) -> I = ( Base ` ( IDLsrg ` R ) ) ) |
22 |
21
|
3ad2ant1 |
|- ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> I = ( Base ` ( IDLsrg ` R ) ) ) |
23 |
19 22
|
eleqtrd |
|- ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> j e. ( Base ` ( IDLsrg ` R ) ) ) |
24 |
23
|
rabssdv |
|- ( ( R e. Ring /\ i e. I ) -> { j e. I | -. i C_ j } C_ ( Base ` ( IDLsrg ` R ) ) ) |
25 |
18 24
|
elpwd |
|- ( ( R e. Ring /\ i e. I ) -> { j e. I | -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) ) |
26 |
25
|
ralrimiva |
|- ( R e. Ring -> A. i e. I { j e. I | -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) ) |
27 |
|
eqid |
|- ( i e. I |-> { j e. I | -. i C_ j } ) = ( i e. I |-> { j e. I | -. i C_ j } ) |
28 |
27
|
rnmptss |
|- ( A. i e. I { j e. I | -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) -> ran ( i e. I |-> { j e. I | -. i C_ j } ) C_ ~P ( Base ` ( IDLsrg ` R ) ) ) |
29 |
26 28
|
syl |
|- ( R e. Ring -> ran ( i e. I |-> { j e. I | -. i C_ j } ) C_ ~P ( Base ` ( IDLsrg ` R ) ) ) |
30 |
15 29
|
eqsstrrd |
|- ( R e. Ring -> ( TopSet ` ( IDLsrg ` R ) ) C_ ~P ( Base ` ( IDLsrg ` R ) ) ) |
31 |
|
eqid |
|- ( Base ` ( IDLsrg ` R ) ) = ( Base ` ( IDLsrg ` R ) ) |
32 |
|
eqid |
|- ( TopSet ` ( IDLsrg ` R ) ) = ( TopSet ` ( IDLsrg ` R ) ) |
33 |
31 32
|
topnid |
|- ( ( TopSet ` ( IDLsrg ` R ) ) C_ ~P ( Base ` ( IDLsrg ` R ) ) -> ( TopSet ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) ) |
34 |
30 33
|
syl |
|- ( R e. Ring -> ( TopSet ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) ) |
35 |
15 34
|
eqtrd |
|- ( R e. Ring -> ran ( i e. I |-> { j e. I | -. i C_ j } ) = ( TopOpen ` ( IDLsrg ` R ) ) ) |
36 |
35
|
oveq1d |
|- ( R e. Ring -> ( ran ( i e. I |-> { j e. I | -. i C_ j } ) |`t P ) = ( ( TopOpen ` ( IDLsrg ` R ) ) |`t P ) ) |
37 |
16
|
mptex |
|- ( i e. I |-> { j e. I | -. i C_ j } ) e. _V |
38 |
37
|
rnex |
|- ran ( i e. I |-> { j e. I | -. i C_ j } ) e. _V |
39 |
3
|
fvexi |
|- P e. _V |
40 |
|
elrest |
|- ( ( ran ( i e. I |-> { j e. I | -. i C_ j } ) e. _V /\ P e. _V ) -> ( x e. ( ran ( i e. I |-> { j e. I | -. i C_ j } ) |`t P ) <-> E. y e. ran ( i e. I |-> { j e. I | -. i C_ j } ) x = ( y i^i P ) ) ) |
41 |
38 39 40
|
mp2an |
|- ( x e. ( ran ( i e. I |-> { j e. I | -. i C_ j } ) |`t P ) <-> E. y e. ran ( i e. I |-> { j e. I | -. i C_ j } ) x = ( y i^i P ) ) |
42 |
17
|
rgenw |
|- A. i e. I { j e. I | -. i C_ j } e. _V |
43 |
|
ineq1 |
|- ( y = { j e. I | -. i C_ j } -> ( y i^i P ) = ( { j e. I | -. i C_ j } i^i P ) ) |
44 |
43
|
eqeq2d |
|- ( y = { j e. I | -. i C_ j } -> ( x = ( y i^i P ) <-> x = ( { j e. I | -. i C_ j } i^i P ) ) ) |
45 |
27 44
|
rexrnmptw |
|- ( A. i e. I { j e. I | -. i C_ j } e. _V -> ( E. y e. ran ( i e. I |-> { j e. I | -. i C_ j } ) x = ( y i^i P ) <-> E. i e. I x = ( { j e. I | -. i C_ j } i^i P ) ) ) |
46 |
42 45
|
ax-mp |
|- ( E. y e. ran ( i e. I |-> { j e. I | -. i C_ j } ) x = ( y i^i P ) <-> E. i e. I x = ( { j e. I | -. i C_ j } i^i P ) ) |
47 |
|
inrab2 |
|- ( { j e. I | -. i C_ j } i^i P ) = { j e. ( I i^i P ) | -. i C_ j } |
48 |
|
prmidlssidl |
|- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) |
49 |
48 3 2
|
3sstr4g |
|- ( R e. Ring -> P C_ I ) |
50 |
|
sseqin2 |
|- ( P C_ I <-> ( I i^i P ) = P ) |
51 |
49 50
|
sylib |
|- ( R e. Ring -> ( I i^i P ) = P ) |
52 |
51
|
rabeqdv |
|- ( R e. Ring -> { j e. ( I i^i P ) | -. i C_ j } = { j e. P | -. i C_ j } ) |
53 |
47 52
|
syl5eq |
|- ( R e. Ring -> ( { j e. I | -. i C_ j } i^i P ) = { j e. P | -. i C_ j } ) |
54 |
53
|
eqeq2d |
|- ( R e. Ring -> ( x = ( { j e. I | -. i C_ j } i^i P ) <-> x = { j e. P | -. i C_ j } ) ) |
55 |
54
|
rexbidv |
|- ( R e. Ring -> ( E. i e. I x = ( { j e. I | -. i C_ j } i^i P ) <-> E. i e. I x = { j e. P | -. i C_ j } ) ) |
56 |
46 55
|
syl5bb |
|- ( R e. Ring -> ( E. y e. ran ( i e. I |-> { j e. I | -. i C_ j } ) x = ( y i^i P ) <-> E. i e. I x = { j e. P | -. i C_ j } ) ) |
57 |
41 56
|
syl5bb |
|- ( R e. Ring -> ( x e. ( ran ( i e. I |-> { j e. I | -. i C_ j } ) |`t P ) <-> E. i e. I x = { j e. P | -. i C_ j } ) ) |
58 |
4
|
eleq2i |
|- ( x e. J <-> x e. ran ( i e. I |-> { j e. P | -. i C_ j } ) ) |
59 |
|
eqid |
|- ( i e. I |-> { j e. P | -. i C_ j } ) = ( i e. I |-> { j e. P | -. i C_ j } ) |
60 |
39
|
rabex |
|- { j e. P | -. i C_ j } e. _V |
61 |
59 60
|
elrnmpti |
|- ( x e. ran ( i e. I |-> { j e. P | -. i C_ j } ) <-> E. i e. I x = { j e. P | -. i C_ j } ) |
62 |
58 61
|
bitri |
|- ( x e. J <-> E. i e. I x = { j e. P | -. i C_ j } ) |
63 |
57 62
|
bitr4di |
|- ( R e. Ring -> ( x e. ( ran ( i e. I |-> { j e. I | -. i C_ j } ) |`t P ) <-> x e. J ) ) |
64 |
63
|
eqrdv |
|- ( R e. Ring -> ( ran ( i e. I |-> { j e. I | -. i C_ j } ) |`t P ) = J ) |
65 |
12 36 64
|
3eqtr2rd |
|- ( R e. Ring -> J = ( TopOpen ` S ) ) |