Metamath Proof Explorer

Theorem ispridl

Description: The predicate "is a prime ideal". (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 ispridl ⊢ R ∈ RingOps → P ∈ PrIdl ⁡ R ↔ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ P → a ⊆ P ∨ b ⊆ P

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 1 2 3 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
5 4 eleq2d ⊢ R ∈ RingOps → P ∈ PrIdl ⁡ R ↔ P ∈ i ∈ Idl ⁡ R | i ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i
6 neeq1 ⊢ i = P → i ≠ X ↔ P ≠ X
7 eleq2 ⊢ i = P → x H y ∈ i ↔ x H y ∈ P
8 7 2ralbidv ⊢ i = P → ∀ x ∈ a ∀ y ∈ b x H y ∈ i ↔ ∀ x ∈ a ∀ y ∈ b x H y ∈ P
9 sseq2 ⊢ i = P → a ⊆ i ↔ a ⊆ P
10 sseq2 ⊢ i = P → b ⊆ i ↔ b ⊆ P
11 9 10 orbi12d ⊢ i = P → a ⊆ i ∨ b ⊆ i ↔ a ⊆ P ∨ b ⊆ P
12 8 11 imbi12d ⊢ i = P → ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ x ∈ a ∀ y ∈ b x H y ∈ P → a ⊆ P ∨ b ⊆ P
13 12 2ralbidv ⊢ i = P → ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i ↔ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ P → a ⊆ P ∨ b ⊆ P
14 6 13 anbi12d ⊢ i = P → i ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i ↔ P ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ P → a ⊆ P ∨ b ⊆ P
15 14 elrab ⊢ P ∈ i ∈ Idl ⁡ R | i ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i ↔ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ P → a ⊆ P ∨ b ⊆ P
16 3anass ⊢ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ P → a ⊆ P ∨ b ⊆ P ↔ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ P → a ⊆ P ∨ b ⊆ P
17 15 16 bitr4i ⊢ P ∈ i ∈ Idl ⁡ R | i ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ i → a ⊆ i ∨ b ⊆ i ↔ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ P → a ⊆ P ∨ b ⊆ P
18 5 17 bitrdi ⊢ R ∈ RingOps → P ∈ PrIdl ⁡ R ↔ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x H y ∈ P → a ⊆ P ∨ b ⊆ P