Metamath Proof Explorer

Theorem zar0ring

Description: The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024)

Ref Expression
Hypotheses zartop.1 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
zartop.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
zar0ring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion zar0ring ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐽 = { ∅ } )

Proof

Step Hyp Ref Expression
1 zartop.1 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
2 zartop.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
3 zar0ring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5 eqid ⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
6 eqid ⊢ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } )
7 1 4 5 6 rspectopn ⊢ ( 𝑅 ∈ Ring → ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( TopOpen ‘ 𝑆 ) )
8 7 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( TopOpen ‘ 𝑆 ) )
9 2 8 eqtr4id ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐽 = ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
10 fvex ⊢ ( PrmIdeal ‘ 𝑅 ) ∈ V
11 10 rabex ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ V
12 eqid ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } )
13 11 12 fnmpti ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) Fn ( LIdeal ‘ 𝑅 )
14 13 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) Fn ( LIdeal ‘ 𝑅 ) )
15 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
16 3 15 0ringidl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( LIdeal ‘ 𝑅 ) = { { ( 0g ‘ 𝑅 ) } } )
17 snex ⊢ { ( 0g ‘ 𝑅 ) } ∈ V
18 17 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → { ( 0g ‘ 𝑅 ) } ∈ V )
19 18 snn0d ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → { { ( 0g ‘ 𝑅 ) } } ≠ ∅ )
20 16 19 eqnetrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( LIdeal ‘ 𝑅 ) ≠ ∅ )
21 3 0ringprmidl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( PrmIdeal ‘ 𝑅 ) = ∅ )
22 21 rabeqdv ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ∅ ∣ ¬ 𝑖 ⊆ 𝑗 } )
23 rab0 ⊢ { 𝑗 ∈ ∅ ∣ ¬ 𝑖 ⊆ 𝑗 } = ∅
24 22 23 eqtrdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } = ∅ )
25 24 mpteq2dv ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ ∅ ) )
26 fconstmpt ⊢ ( ( LIdeal ‘ 𝑅 ) × { ∅ } ) = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ ∅ )
27 25 26 eqtr4di ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( ( LIdeal ‘ 𝑅 ) × { ∅ } ) )
28 fconst5 ⊢ ( ( ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) Fn ( LIdeal ‘ 𝑅 ) ∧ ( LIdeal ‘ 𝑅 ) ≠ ∅ ) → ( ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( ( LIdeal ‘ 𝑅 ) × { ∅ } ) ↔ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = { ∅ } ) )
29 28 biimpa ⊢ ( ( ( ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) Fn ( LIdeal ‘ 𝑅 ) ∧ ( LIdeal ‘ 𝑅 ) ≠ ∅ ) ∧ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( ( LIdeal ‘ 𝑅 ) × { ∅ } ) ) → ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = { ∅ } )
30 14 20 27 29 syl21anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ¬ 𝑖 ⊆ 𝑗 } ) = { ∅ } )
31 9 30 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐽 = { ∅ } )