Metamath Proof Explorer

Theorem pridl

Description: The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypothesis pridl.1 ⊢H=2nd⁡R
Assertion pridl ⊢R∈RingOps∧P∈PrIdl⁡R∧A∈Idl⁡R∧B∈Idl⁡R∧∀x∈A∀y∈BxHy∈P→A⊆P∨B⊆P

Proof

Step Hyp Ref Expression
1 pridl.1 ⊢H=2nd⁡R
2 eqid ⊢1st⁡R=1st⁡R
3 eqid ⊢ran⁡1st⁡R=ran⁡1st⁡R
4 2 1 3 ispridl ⊢R∈RingOps→P∈PrIdl⁡R↔P∈Idl⁡R∧P≠ran⁡1st⁡R∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P
5 df-3an ⊢P∈Idl⁡R∧P≠ran⁡1st⁡R∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P↔P∈Idl⁡R∧P≠ran⁡1st⁡R∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P
6 4 5 bitrdi ⊢R∈RingOps→P∈PrIdl⁡R↔P∈Idl⁡R∧P≠ran⁡1st⁡R∧∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P
7 6 simplbda ⊢R∈RingOps∧P∈PrIdl⁡R→∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P
8 raleq ⊢a=A→∀x∈a∀y∈bxHy∈P↔∀x∈A∀y∈bxHy∈P
9 sseq1 ⊢a=A→a⊆P↔A⊆P
10 9 orbi1d ⊢a=A→a⊆P∨b⊆P↔A⊆P∨b⊆P
11 8 10 imbi12d ⊢a=A→∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P↔∀x∈A∀y∈bxHy∈P→A⊆P∨b⊆P
12 raleq ⊢b=B→∀y∈bxHy∈P↔∀y∈BxHy∈P
13 12 ralbidv ⊢b=B→∀x∈A∀y∈bxHy∈P↔∀x∈A∀y∈BxHy∈P
14 sseq1 ⊢b=B→b⊆P↔B⊆P
15 14 orbi2d ⊢b=B→A⊆P∨b⊆P↔A⊆P∨B⊆P
16 13 15 imbi12d ⊢b=B→∀x∈A∀y∈bxHy∈P→A⊆P∨b⊆P↔∀x∈A∀y∈BxHy∈P→A⊆P∨B⊆P
17 11 16 rspc2v ⊢A∈Idl⁡R∧B∈Idl⁡R→∀a∈Idl⁡R∀b∈Idl⁡R∀x∈a∀y∈bxHy∈P→a⊆P∨b⊆P→∀x∈A∀y∈BxHy∈P→A⊆P∨B⊆P
18 7 17 syl5com ⊢R∈RingOps∧P∈PrIdl⁡R→A∈Idl⁡R∧B∈Idl⁡R→∀x∈A∀y∈BxHy∈P→A⊆P∨B⊆P
19 18 expd ⊢R∈RingOps∧P∈PrIdl⁡R→A∈Idl⁡R→B∈Idl⁡R→∀x∈A∀y∈BxHy∈P→A⊆P∨B⊆P
20 19 3imp2 ⊢R∈RingOps∧P∈PrIdl⁡R∧A∈Idl⁡R∧B∈Idl⁡R∧∀x∈A∀y∈BxHy∈P→A⊆P∨B⊆P