Metamath Proof Explorer

Theorem zarcls1

Description: The unit ideal B is the only ideal whose closure in the Zariski topology is the empty set. Stronger form of the Proposition 1.1.2(i) of EGA p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zarclsx.1 ⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
zarcls1.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion zarcls1 ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑉 ‘ 𝐼 ) = ∅ ↔ 𝐼 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 zarclsx.1 ⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
2 zarcls1.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 simplr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑉 ‘ 𝐼 ) = ∅ ) ∧ 𝐼 ≠ 𝐵 ) → ( 𝑉 ‘ 𝐼 ) = ∅ )
4 sseq2 ⊢ ( 𝑗 = 𝑚 → ( 𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ 𝑚 ) )
5 eqid ⊢ ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
6 5 mxidlprm ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ∈ ( PrmIdeal ‘ 𝑅 ) )
7 6 ad5ant14 ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) → 𝑚 ∈ ( PrmIdeal ‘ 𝑅 ) )
8 simpr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) → 𝐼 ⊆ 𝑚 )
9 4 7 8 elrabd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) → 𝑚 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } )
10 1 a1i ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) → 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
11 sseq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ⊆ 𝑗 ↔ 𝐼 ⊆ 𝑗 ) )
12 11 rabbidv ⊢ ( 𝑖 = 𝐼 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } )
13 12 adantl ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) ∧ 𝑖 = 𝐼 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } )
14 simp-4r ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
15 fvex ⊢ ( PrmIdeal ‘ 𝑅 ) ∈ V
16 15 rabex ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } ∈ V
17 16 a1i ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } ∈ V )
18 10 13 14 17 fvmptd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) → ( 𝑉 ‘ 𝐼 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } )
19 9 18 eleqtrrd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) → 𝑚 ∈ ( 𝑉 ‘ 𝐼 ) )
20 ne0i ⊢ ( 𝑚 ∈ ( 𝑉 ‘ 𝐼 ) → ( 𝑉 ‘ 𝐼 ) ≠ ∅ )
21 19 20 syl ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ⊆ 𝑚 ) → ( 𝑉 ‘ 𝐼 ) ≠ ∅ )
22 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
23 2 ssmxidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝐼 ⊆ 𝑚 )
24 23 3expa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝐼 ⊆ 𝑚 )
25 22 24 sylanl1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝐼 ⊆ 𝑚 )
26 21 25 r19.29a ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ≠ 𝐵 ) → ( 𝑉 ‘ 𝐼 ) ≠ ∅ )
27 26 adantlr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑉 ‘ 𝐼 ) = ∅ ) ∧ 𝐼 ≠ 𝐵 ) → ( 𝑉 ‘ 𝐼 ) ≠ ∅ )
28 27 neneqd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑉 ‘ 𝐼 ) = ∅ ) ∧ 𝐼 ≠ 𝐵 ) → ¬ ( 𝑉 ‘ 𝐼 ) = ∅ )
29 3 28 pm2.65da ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑉 ‘ 𝐼 ) = ∅ ) → ¬ 𝐼 ≠ 𝐵 )
30 nne ⊢ ( ¬ 𝐼 ≠ 𝐵 ↔ 𝐼 = 𝐵 )
31 29 30 sylib ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑉 ‘ 𝐼 ) = ∅ ) → 𝐼 = 𝐵 )
32 fveq2 ⊢ ( 𝐼 = 𝐵 → ( 𝑉 ‘ 𝐼 ) = ( 𝑉 ‘ 𝐵 ) )
33 32 adantl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 = 𝐵 ) → ( 𝑉 ‘ 𝐼 ) = ( 𝑉 ‘ 𝐵 ) )
34 1 a1i ⊢ ( 𝑅 ∈ Ring → 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
35 sseq1 ⊢ ( 𝑖 = 𝐵 → ( 𝑖 ⊆ 𝑗 ↔ 𝐵 ⊆ 𝑗 ) )
36 35 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 = 𝐵 ) → ( 𝑖 ⊆ 𝑗 ↔ 𝐵 ⊆ 𝑗 ) )
37 36 rabbidv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 = 𝐵 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐵 ⊆ 𝑗 } )
38 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
39 38 2 lidl1 ⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( LIdeal ‘ 𝑅 ) )
40 15 rabex ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐵 ⊆ 𝑗 } ∈ V
41 40 a1i ⊢ ( 𝑅 ∈ Ring → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐵 ⊆ 𝑗 } ∈ V )
42 34 37 39 41 fvmptd ⊢ ( 𝑅 ∈ Ring → ( 𝑉 ‘ 𝐵 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐵 ⊆ 𝑗 } )
43 prmidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑗 ∈ ( LIdeal ‘ 𝑅 ) )
44 2 38 lidlss ⊢ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) → 𝑗 ⊆ 𝐵 )
45 43 44 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑗 ⊆ 𝐵 )
46 45 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝐵 ⊆ 𝑗 ) → 𝑗 ⊆ 𝐵 )
47 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝐵 ⊆ 𝑗 ) → 𝐵 ⊆ 𝑗 )
48 46 47 eqssd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝐵 ⊆ 𝑗 ) → 𝑗 = 𝐵 )
49 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
50 2 49 prmidlnr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑗 ≠ 𝐵 )
51 50 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝐵 ⊆ 𝑗 ) → 𝑗 ≠ 𝐵 )
52 51 neneqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝐵 ⊆ 𝑗 ) → ¬ 𝑗 = 𝐵 )
53 48 52 pm2.65da ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ¬ 𝐵 ⊆ 𝑗 )
54 53 ralrimiva ⊢ ( 𝑅 ∈ Ring → ∀ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ¬ 𝐵 ⊆ 𝑗 )
55 rabeq0 ⊢ ( { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐵 ⊆ 𝑗 } = ∅ ↔ ∀ 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ¬ 𝐵 ⊆ 𝑗 )
56 54 55 sylibr ⊢ ( 𝑅 ∈ Ring → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝐵 ⊆ 𝑗 } = ∅ )
57 42 56 eqtrd ⊢ ( 𝑅 ∈ Ring → ( 𝑉 ‘ 𝐵 ) = ∅ )
58 22 57 syl ⊢ ( 𝑅 ∈ CRing → ( 𝑉 ‘ 𝐵 ) = ∅ )
59 58 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 = 𝐵 ) → ( 𝑉 ‘ 𝐵 ) = ∅ )
60 33 59 eqtrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 = 𝐵 ) → ( 𝑉 ‘ 𝐼 ) = ∅ )
61 31 60 impbida ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑉 ‘ 𝐼 ) = ∅ ↔ 𝐼 = 𝐵 ) )