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 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
rspectopn.1 ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
rspectopn.2 ⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
rspectopn.3 ⊢ 𝐽 = ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
Assertion rspectopn ( 𝑅 ∈ Ring → 𝐽 = ( TopOpen ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 rspecbas.1 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
2 rspectopn.1 ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
3 rspectopn.2 ⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
4 rspectopn.3 ⊢ 𝐽 = ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
5 rspecval ⊢ ( 𝑅 ∈ Ring → ( Spec ‘ 𝑅 ) = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) )
6 3 oveq2i ⊢ ( ( IDLsrg ‘ 𝑅 ) ↾s 𝑃 ) = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) )
7 5 1 6 3eqtr4g ⊢ ( 𝑅 ∈ Ring → 𝑆 = ( ( IDLsrg ‘ 𝑅 ) ↾s 𝑃 ) )
8 7 fveq2d ⊢ ( 𝑅 ∈ Ring → ( TopOpen ‘ 𝑆 ) = ( TopOpen ‘ ( ( IDLsrg ‘ 𝑅 ) ↾s 𝑃 ) ) )
9 eqid ⊢ ( ( IDLsrg ‘ 𝑅 ) ↾s 𝑃 ) = ( ( IDLsrg ‘ 𝑅 ) ↾s 𝑃 )
10 eqid ⊢ ( TopOpen ‘ ( IDLsrg ‘ 𝑅 ) ) = ( TopOpen ‘ ( IDLsrg ‘ 𝑅 ) )
11 9 10 resstopn ⊢ ( ( TopOpen ‘ ( IDLsrg ‘ 𝑅 ) ) ↾t 𝑃 ) = ( TopOpen ‘ ( ( IDLsrg ‘ 𝑅 ) ↾s 𝑃 ) )
12 8 11 eqtr4di ⊢ ( 𝑅 ∈ Ring → ( TopOpen ‘ 𝑆 ) = ( ( TopOpen ‘ ( IDLsrg ‘ 𝑅 ) ) ↾t 𝑃 ) )
13 eqid ⊢ ( IDLsrg ‘ 𝑅 ) = ( IDLsrg ‘ 𝑅 )
14 eqid ⊢ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } )
15 13 2 14 idlsrgtset ⊢ ( 𝑅 ∈ Ring → ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) )
16 2 fvexi ⊢ 𝐼 ∈ V
17 16 rabex ⊢ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ V
18 17 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼 ) → { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ V )
19 simp2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ∧ ¬ 𝑖 ⊆ 𝑗 ) → 𝑗 ∈ 𝐼 )
20 13 2 idlsrgbas ⊢ ( 𝑅 ∈ Ring → 𝐼 = ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
21 20 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼 ) → 𝐼 = ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
22 21 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ∧ ¬ 𝑖 ⊆ 𝑗 ) → 𝐼 = ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
23 19 22 eleqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ∧ ¬ 𝑖 ⊆ 𝑗 ) → 𝑗 ∈ ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
24 23 rabssdv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼 ) → { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ⊆ ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
25 18 24 elpwd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼 ) → { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ 𝒫 ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
26 25 ralrimiva ⊢ ( 𝑅 ∈ Ring → ∀ 𝑖 ∈ 𝐼 { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ 𝒫 ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
27 eqid ⊢ ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } )
28 27 rnmptss ⊢ ( ∀ 𝑖 ∈ 𝐼 { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ 𝒫 ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) → ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⊆ 𝒫 ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
29 26 28 syl ⊢ ( 𝑅 ∈ Ring → ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⊆ 𝒫 ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
30 15 29 eqsstrrd ⊢ ( 𝑅 ∈ Ring → ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) ⊆ 𝒫 ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) )
31 eqid ⊢ ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) = ( Base ‘ ( IDLsrg ‘ 𝑅 ) )
32 eqid ⊢ ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) = ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) )
33 31 32 topnid ⊢ ( ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) ⊆ 𝒫 ( Base ‘ ( IDLsrg ‘ 𝑅 ) ) → ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) = ( TopOpen ‘ ( IDLsrg ‘ 𝑅 ) ) )
34 30 33 syl ⊢ ( 𝑅 ∈ Ring → ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) = ( TopOpen ‘ ( IDLsrg ‘ 𝑅 ) ) )
35 15 34 eqtrd ⊢ ( 𝑅 ∈ Ring → ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( TopOpen ‘ ( IDLsrg ‘ 𝑅 ) ) )
36 35 oveq1d ⊢ ( 𝑅 ∈ Ring → ( ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↾t 𝑃 ) = ( ( TopOpen ‘ ( IDLsrg ‘ 𝑅 ) ) ↾t 𝑃 ) )
37 16 mptex ⊢ ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ∈ V
38 37 rnex ⊢ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ∈ V
39 3 fvexi ⊢ 𝑃 ∈ V
40 elrest ⊢ ( ( ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ∈ V ∧ 𝑃 ∈ V ) → ( 𝑥 ∈ ( ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↾t 𝑃 ) ↔ ∃ 𝑦 ∈ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) 𝑥 = ( 𝑦 ∩ 𝑃 ) ) )
41 38 39 40 mp2an ⊢ ( 𝑥 ∈ ( ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↾t 𝑃 ) ↔ ∃ 𝑦 ∈ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) 𝑥 = ( 𝑦 ∩ 𝑃 ) )
42 17 rgenw ⊢ ∀ 𝑖 ∈ 𝐼 { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ V
43 ineq1 ⊢ ( 𝑦 = { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } → ( 𝑦 ∩ 𝑃 ) = ( { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∩ 𝑃 ) )
44 43 eqeq2d ⊢ ( 𝑦 = { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } → ( 𝑥 = ( 𝑦 ∩ 𝑃 ) ↔ 𝑥 = ( { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∩ 𝑃 ) ) )
45 27 44 rexrnmptw ⊢ ( ∀ 𝑖 ∈ 𝐼 { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ V → ( ∃ 𝑦 ∈ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) 𝑥 = ( 𝑦 ∩ 𝑃 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = ( { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∩ 𝑃 ) ) )
46 42 45 ax-mp ⊢ ( ∃ 𝑦 ∈ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) 𝑥 = ( 𝑦 ∩ 𝑃 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = ( { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∩ 𝑃 ) )
47 inrab2 ⊢ ( { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∩ 𝑃 ) = { 𝑗 ∈ ( 𝐼 ∩ 𝑃 ) ∣ ¬ 𝑖 ⊆ 𝑗 }
48 prmidlssidl ⊢ ( 𝑅 ∈ Ring → ( PrmIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
49 48 3 2 3sstr4g ⊢ ( 𝑅 ∈ Ring → 𝑃 ⊆ 𝐼 )
50 sseqin2 ⊢ ( 𝑃 ⊆ 𝐼 ↔ ( 𝐼 ∩ 𝑃 ) = 𝑃 )
51 49 50 sylib ⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∩ 𝑃 ) = 𝑃 )
52 51 rabeqdv ⊢ ( 𝑅 ∈ Ring → { 𝑗 ∈ ( 𝐼 ∩ 𝑃 ) ∣ ¬ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
53 47 52 syl5eq ⊢ ( 𝑅 ∈ Ring → ( { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∩ 𝑃 ) = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
54 53 eqeq2d ⊢ ( 𝑅 ∈ Ring → ( 𝑥 = ( { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∩ 𝑃 ) ↔ 𝑥 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
55 54 rexbidv ⊢ ( 𝑅 ∈ Ring → ( ∃ 𝑖 ∈ 𝐼 𝑥 = ( { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ∩ 𝑃 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
56 46 55 syl5bb ⊢ ( 𝑅 ∈ Ring → ( ∃ 𝑦 ∈ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) 𝑥 = ( 𝑦 ∩ 𝑃 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
57 41 56 syl5bb ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↾t 𝑃 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
58 4 eleq2i ⊢ ( 𝑥 ∈ 𝐽 ↔ 𝑥 ∈ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
59 eqid ⊢ ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
60 39 rabex ⊢ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ V
61 59 60 elrnmpti ⊢ ( 𝑥 ∈ ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
62 58 61 bitri ⊢ ( 𝑥 ∈ 𝐽 ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
63 57 62 bitr4di ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↾t 𝑃 ) ↔ 𝑥 ∈ 𝐽 ) )
64 63 eqrdv ⊢ ( 𝑅 ∈ Ring → ( ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↾t 𝑃 ) = 𝐽 )
65 12 36 64 3eqtr2rd ⊢ ( 𝑅 ∈ Ring → 𝐽 = ( TopOpen ‘ 𝑆 ) )