Metamath Proof Explorer


Theorem rspectopn

Description: The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024)

Ref Expression
Hypotheses rspecbas.1
|- S = ( Spec ` R )
rspectopn.1
|- I = ( LIdeal ` R )
rspectopn.2
|- P = ( PrmIdeal ` R )
rspectopn.3
|- J = ran ( i e. I |-> { j e. P | -. i C_ j } )
Assertion rspectopn
|- ( R e. Ring -> J = ( TopOpen ` S ) )

Proof

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 ) )