This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑅 IdlGen 𝐼 ) = 𝐼 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 )
2 eqid ⊢ ran ( 1st ‘ 𝑅 ) = ran ( 1st ‘ 𝑅 )
3 1 2 idlss ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝐼 ⊆ ran ( 1st ‘ 𝑅 ) )
4 1 2 igenval ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ⊆ ran ( 1st ‘ 𝑅 ) ) → ( 𝑅 IdlGen 𝐼 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } )
5 3 4 syldan ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑅 IdlGen 𝐼 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } )
6 intmin ⊢ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } = 𝐼 )
7 6 adantl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } = 𝐼 )
8 5 7 eqtrd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑅 IdlGen 𝐼 ) = 𝐼 )