Metamath Proof Explorer

Theorem idl0cl

Description: An ideal contains 0 . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idl0cl.1 ⊢ G = 1 st ⁡ R
idl0cl.2 ⊢ Z = GId ⁡ G
Assertion idl0cl ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → Z ∈ I

Proof

Step Hyp Ref Expression
1 idl0cl.1 ⊢ G = 1 st ⁡ R
2 idl0cl.2 ⊢ Z = GId ⁡ G
3 eqid ⊢ 2 nd ⁡ R = 2 nd ⁡ R
4 eqid ⊢ ran ⁡ G = ran ⁡ G
5 1 3 4 2 isidl ⊢ R ∈ RingOps → I ∈ Idl ⁡ R ↔ I ⊆ ran ⁡ G ∧ Z ∈ I ∧ ∀ x ∈ I ∀ y ∈ I x G y ∈ I ∧ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R x ∈ I ∧ x 2 nd ⁡ R z ∈ I
6 5 biimpa ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → I ⊆ ran ⁡ G ∧ Z ∈ I ∧ ∀ x ∈ I ∀ y ∈ I x G y ∈ I ∧ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R x ∈ I ∧ x 2 nd ⁡ R z ∈ I
7 6 simp2d ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → Z ∈ I