Metamath Proof Explorer

Theorem prmidlval

Description: The class of prime ideals of a ring R . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses prmidlval.1 ⊢ B = Base R
prmidlval.2 ⊢ · ˙ = ⋅ R
Assertion prmidlval ⊢ R ∈ Ring → PrmIdeal ⁡ R = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i

Proof

Step Hyp Ref Expression
1 prmidlval.1 ⊢ B = Base R
2 prmidlval.2 ⊢ · ˙ = ⋅ R
3 df-prmidl ⊢ PrmIdeal = r ∈ Ring ⟼ i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i
4 fveq2 ⊢ r = R → LIdeal ⁡ r = LIdeal ⁡ R
5 fveq2 ⊢ r = R → Base r = Base R
6 5 1 eqtr4di ⊢ r = R → Base r = B
7 6 neeq2d ⊢ r = R → i ≠ Base r ↔ i ≠ B
8 fveq2 ⊢ r = R → ⋅ r = ⋅ R
9 8 2 eqtr4di ⊢ r = R → ⋅ r = · ˙
10 9 oveqd ⊢ r = R → x ⋅ r y = x · ˙ y
11 10 eleq1d ⊢ r = R → x ⋅ r y ∈ i ↔ x · ˙ y ∈ i
12 11 2ralbidv ⊢ r = R → ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i ↔ ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i
13 12 imbi1d ⊢ r = R → ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
14 4 13 raleqbidv ⊢ r = R → ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
15 4 14 raleqbidv ⊢ r = R → ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
16 7 15 anbi12d ⊢ r = R → i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
17 4 16 rabeqbidv ⊢ r = R → i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ a ∈ LIdeal ⁡ r ∀ b ∈ LIdeal ⁡ r ∀ x ∈ a ∀ y ∈ b x ⋅ r y ∈ i → a ⊆ i ∨ b ⊆ i = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
18 id ⊢ R ∈ Ring → R ∈ Ring
19 eqid ⊢ i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i
20 fvexd ⊢ R ∈ Ring → LIdeal ⁡ R ∈ V
21 19 20 rabexd ⊢ R ∈ Ring → i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i ∈ V
22 3 17 18 21 fvmptd3 ⊢ R ∈ Ring → PrmIdeal ⁡ R = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ a ∈ LIdeal ⁡ R ∀ b ∈ LIdeal ⁡ R ∀ x ∈ a ∀ y ∈ b x · ˙ y ∈ i → a ⊆ i ∨ b ⊆ i