Metamath Proof Explorer

Theorem igenidl2

Description: The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion igenidl2 ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → R IdlGen I = I

Proof

Step Hyp Ref Expression
1 eqid ⊢ 1 st ⁡ R = 1 st ⁡ R
2 eqid ⊢ ran ⁡ 1 st ⁡ R = ran ⁡ 1 st ⁡ R
3 1 2 idlss ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → I ⊆ ran ⁡ 1 st ⁡ R
4 1 2 igenval ⊢ R ∈ RingOps ∧ I ⊆ ran ⁡ 1 st ⁡ R → R IdlGen I = ⋂ j ∈ Idl ⁡ R | I ⊆ j
5 3 4 syldan ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → R IdlGen I = ⋂ j ∈ Idl ⁡ R | I ⊆ j
6 intmin ⊢ I ∈ Idl ⁡ R → ⋂ j ∈ Idl ⁡ R | I ⊆ j = I
7 6 adantl ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → ⋂ j ∈ Idl ⁡ R | I ⊆ j = I
8 5 7 eqtrd ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → R IdlGen I = I