Metamath Proof Explorer

Theorem isidl

Description: The predicate "is an ideal of the ring R ". (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idlval.1 ⊢G=1st⁡R
idlval.2 ⊢H=2nd⁡R
idlval.3 ⊢X=ran⁡G
idlval.4 ⊢Z=GId⁡G
Assertion isidl ⊢R∈RingOps→I∈Idl⁡R↔I⊆X∧Z∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I

Proof

Step Hyp Ref Expression
1 idlval.1 ⊢G=1st⁡R
2 idlval.2 ⊢H=2nd⁡R
3 idlval.3 ⊢X=ran⁡G
4 idlval.4 ⊢Z=GId⁡G
5 1 2 3 4 idlval ⊢R∈RingOps→Idl⁡R=i∈𝒫X|Z∈i∧∀x∈i∀y∈ixGy∈i∧∀z∈XzHx∈i∧xHz∈i
6 5 eleq2d ⊢R∈RingOps→I∈Idl⁡R↔I∈i∈𝒫X|Z∈i∧∀x∈i∀y∈ixGy∈i∧∀z∈XzHx∈i∧xHz∈i
7 1 fvexi ⊢G∈V
8 7 rnex ⊢ran⁡G∈V
9 3 8 eqeltri ⊢X∈V
10 9 elpw2 ⊢I∈𝒫X↔I⊆X
11 10 anbi1i ⊢I∈𝒫X∧Z∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I↔I⊆X∧Z∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
12 eleq2 ⊢i=I→Z∈i↔Z∈I
13 eleq2 ⊢i=I→xGy∈i↔xGy∈I
14 13 raleqbi1dv ⊢i=I→∀y∈ixGy∈i↔∀y∈IxGy∈I
15 eleq2 ⊢i=I→zHx∈i↔zHx∈I
16 eleq2 ⊢i=I→xHz∈i↔xHz∈I
17 15 16 anbi12d ⊢i=I→zHx∈i∧xHz∈i↔zHx∈I∧xHz∈I
18 17 ralbidv ⊢i=I→∀z∈XzHx∈i∧xHz∈i↔∀z∈XzHx∈I∧xHz∈I
19 14 18 anbi12d ⊢i=I→∀y∈ixGy∈i∧∀z∈XzHx∈i∧xHz∈i↔∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
20 19 raleqbi1dv ⊢i=I→∀x∈i∀y∈ixGy∈i∧∀z∈XzHx∈i∧xHz∈i↔∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
21 12 20 anbi12d ⊢i=I→Z∈i∧∀x∈i∀y∈ixGy∈i∧∀z∈XzHx∈i∧xHz∈i↔Z∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
22 21 elrab ⊢I∈i∈𝒫X|Z∈i∧∀x∈i∀y∈ixGy∈i∧∀z∈XzHx∈i∧xHz∈i↔I∈𝒫X∧Z∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
23 3anass ⊢I⊆X∧Z∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I↔I⊆X∧Z∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
24 11 22 23 3bitr4i ⊢I∈i∈𝒫X|Z∈i∧∀x∈i∀y∈ixGy∈i∧∀z∈XzHx∈i∧xHz∈i↔I⊆X∧Z∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
25 6 24 bitrdi ⊢R∈RingOps→I∈Idl⁡R↔I⊆X∧Z∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I