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

Proof

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