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=1st⁡R
pridlval.2 ⊢H=2nd⁡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∈bxHy∈P→a⊆P∨b⊆P

Proof

Step Hyp Ref Expression
1 pridlval.1 ⊢G=1st⁡R
2 pridlval.2 ⊢H=2nd⁡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∈bxHy∈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∈bxHy∈i→a⊆i∨b⊆i
6 neeq1 ⊢i=P→i≠X↔P≠X
7 eleq2 ⊢i=P→xHy∈i↔xHy∈P
8 7 2ralbidv ⊢i=P→∀x∈a∀y∈bxHy∈i↔∀x∈a∀y∈bxHy∈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∈bxHy∈i→a⊆i∨b⊆i↔∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P
13 12 2ralbidv ⊢i=P→∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈i→a⊆i∨b⊆i↔∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P
14 6 13 anbi12d ⊢i=P→i≠X∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈i→a⊆i∨b⊆i↔P≠X∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P
15 14 elrab ⊢P∈i∈Idl⁡R|i≠X∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈i→a⊆i∨b⊆i↔P∈Idl⁡R∧P≠X∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P
16 3anass ⊢P∈Idl⁡R∧P≠X∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P↔P∈Idl⁡R∧P≠X∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P
17 15 16 bitr4i ⊢P∈i∈Idl⁡R|i≠X∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈i→a⊆i∨b⊆i↔P∈Idl⁡R∧P≠X∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈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∈bxHy∈P→a⊆P∨b⊆P