Metamath Proof Explorer

Theorem pridlval

Description: The class of prime ideals of a ring R . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses pridlval.1 ⊢ G = 1 st ⁡ R
pridlval.2 ⊢ H = 2 nd ⁡ R
pridlval.3 ⊢ X = ran ⁡ G
Assertion pridlval ⊢ R ∈ RingOps → PrIdl ⁡ R = i ∈ Idl ⁡ R | i ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i

Proof

Step Hyp Ref Expression
1 pridlval.1 ⊢ G = 1 st ⁡ R
2 pridlval.2 ⊢ H = 2 nd ⁡ R
3 pridlval.3 ⊢ X = ran ⁡ G
4 fveq2 ⊢ r = R → Idl ⁡ r = Idl ⁡ R
5 fveq2 ⊢ r = R → 1 st ⁡ r = 1 st ⁡ R
6 5 1 eqtr4di ⊢ r = R → 1 st ⁡ r = G
7 6 rneqd ⊢ r = R → ran ⁡ 1 st ⁡ r = ran ⁡ G
8 7 3 eqtr4di ⊢ r = R → ran ⁡ 1 st ⁡ r = X
9 8 neeq2d ⊢ r = R → i ≠ ran ⁡ 1 st ⁡ r ↔ i ≠ X
10 fveq2 ⊢ r = R → 2 nd ⁡ r = 2 nd ⁡ R
11 10 2 eqtr4di ⊢ r = R → 2 nd ⁡ r = H
12 11 oveqd ⊢ r = R → x 2 nd ⁡ r y = x H y
13 12 eleq1d ⊢ r = R → x 2 nd ⁡ r y ∈ i ↔ x H y ∈ i
14 13 2ralbidv ⊢ r = R → ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i ↔ ∀ x ∈ a ∀ y ∈ b x H y ∈ i
15 14 imbi1d ⊢ r = R → ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i
16 4 15 raleqbidv ⊢ r = R → ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i
17 4 16 raleqbidv ⊢ r = R → ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i
18 9 17 anbi12d ⊢ r = R → i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i ↔ i ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i
19 4 18 rabeqbidv ⊢ r = R → i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i = i ∈ Idl ⁡ R | i ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i
20 df-pridl ⊢ PrIdl = r ∈ RingOps ⟼ i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i
21 fvex ⊢ Idl ⁡ R ∈ V
22 21 rabex ⊢ i ∈ Idl ⁡ R | i ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i ∈ V
23 19 20 22 fvmpt ⊢ R ∈ RingOps → PrIdl ⁡ R = i ∈ Idl ⁡ R | i ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i