Metamath Proof Explorer

Theorem zarcls0

Description: The closure of the identity ideal in the Zariski topology. Proposition 1.1.2(i) of EGA p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zarclsx.1 ⊢ V = i ∈ LIdeal ⁡ R ⟼ j ∈ PrmIdeal ⁡ R | i ⊆ j
zarcls0.1 ⊢ P = PrmIdeal ⁡ R
zarcls0.2 ⊢ 0 ˙ = 0 R
Assertion zarcls0 ⊢ R ∈ Ring → V ⁡ 0 ˙ = P

Proof

Step Hyp Ref Expression
1 zarclsx.1 ⊢ V = i ∈ LIdeal ⁡ R ⟼ j ∈ PrmIdeal ⁡ R | i ⊆ j
2 zarcls0.1 ⊢ P = PrmIdeal ⁡ R
3 zarcls0.2 ⊢ 0 ˙ = 0 R
4 1 a1i ⊢ R ∈ Ring → V = i ∈ LIdeal ⁡ R ⟼ j ∈ PrmIdeal ⁡ R | i ⊆ j
5 simplr ⊢ R ∈ Ring ∧ i = 0 ˙ ∧ j ∈ PrmIdeal ⁡ R → i = 0 ˙
6 simpll ⊢ R ∈ Ring ∧ i = 0 ˙ ∧ j ∈ PrmIdeal ⁡ R → R ∈ Ring
7 prmidlidl ⊢ R ∈ Ring ∧ j ∈ PrmIdeal ⁡ R → j ∈ LIdeal ⁡ R
8 6 7 sylancom ⊢ R ∈ Ring ∧ i = 0 ˙ ∧ j ∈ PrmIdeal ⁡ R → j ∈ LIdeal ⁡ R
9 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
10 9 3 lidl0cl ⊢ R ∈ Ring ∧ j ∈ LIdeal ⁡ R → 0 ˙ ∈ j
11 6 8 10 syl2anc ⊢ R ∈ Ring ∧ i = 0 ˙ ∧ j ∈ PrmIdeal ⁡ R → 0 ˙ ∈ j
12 11 snssd ⊢ R ∈ Ring ∧ i = 0 ˙ ∧ j ∈ PrmIdeal ⁡ R → 0 ˙ ⊆ j
13 5 12 eqsstrd ⊢ R ∈ Ring ∧ i = 0 ˙ ∧ j ∈ PrmIdeal ⁡ R → i ⊆ j
14 13 ralrimiva ⊢ R ∈ Ring ∧ i = 0 ˙ → ∀ j ∈ PrmIdeal ⁡ R i ⊆ j
15 rabid2 ⊢ PrmIdeal ⁡ R = j ∈ PrmIdeal ⁡ R | i ⊆ j ↔ ∀ j ∈ PrmIdeal ⁡ R i ⊆ j
16 14 15 sylibr ⊢ R ∈ Ring ∧ i = 0 ˙ → PrmIdeal ⁡ R = j ∈ PrmIdeal ⁡ R | i ⊆ j
17 2 16 eqtr2id ⊢ R ∈ Ring ∧ i = 0 ˙ → j ∈ PrmIdeal ⁡ R | i ⊆ j = P
18 9 3 lidl0 ⊢ R ∈ Ring → 0 ˙ ∈ LIdeal ⁡ R
19 2 fvexi ⊢ P ∈ V
20 19 a1i ⊢ R ∈ Ring → P ∈ V
21 4 17 18 20 fvmptd ⊢ R ∈ Ring → V ⁡ 0 ˙ = P