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

Metamath Proof Explorer

Theorem inidl

Description: The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Assertion inidl ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐽 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝐼 ∩ 𝐽 ) ∈ ( Idl ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 intprg ⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐽 ∈ ( Idl ‘ 𝑅 ) ) → ∩ { 𝐼 , 𝐽 } = ( 𝐼 ∩ 𝐽 ) )
2 1 3adant1 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐽 ∈ ( Idl ‘ 𝑅 ) ) → ∩ { 𝐼 , 𝐽 } = ( 𝐼 ∩ 𝐽 ) )
3 prnzg ⊢ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) → { 𝐼 , 𝐽 } ≠ ∅ )
4 3 adantr ⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐽 ∈ ( Idl ‘ 𝑅 ) ) → { 𝐼 , 𝐽 } ≠ ∅ )
5 prssi ⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐽 ∈ ( Idl ‘ 𝑅 ) ) → { 𝐼 , 𝐽 } ⊆ ( Idl ‘ 𝑅 ) )
6 4 5 jca ⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐽 ∈ ( Idl ‘ 𝑅 ) ) → ( { 𝐼 , 𝐽 } ≠ ∅ ∧ { 𝐼 , 𝐽 } ⊆ ( Idl ‘ 𝑅 ) ) )
7 intidl ⊢ ( ( 𝑅 ∈ RingOps ∧ { 𝐼 , 𝐽 } ≠ ∅ ∧ { 𝐼 , 𝐽 } ⊆ ( Idl ‘ 𝑅 ) ) → ∩ { 𝐼 , 𝐽 } ∈ ( Idl ‘ 𝑅 ) )
8 7 3expb ⊢ ( ( 𝑅 ∈ RingOps ∧ ( { 𝐼 , 𝐽 } ≠ ∅ ∧ { 𝐼 , 𝐽 } ⊆ ( Idl ‘ 𝑅 ) ) ) → ∩ { 𝐼 , 𝐽 } ∈ ( Idl ‘ 𝑅 ) )
9 6 8 sylan2 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐽 ∈ ( Idl ‘ 𝑅 ) ) ) → ∩ { 𝐼 , 𝐽 } ∈ ( Idl ‘ 𝑅 ) )
10 9 3impb ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐽 ∈ ( Idl ‘ 𝑅 ) ) → ∩ { 𝐼 , 𝐽 } ∈ ( Idl ‘ 𝑅 ) )
11 2 10 eqeltrrd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐽 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝐼 ∩ 𝐽 ) ∈ ( Idl ‘ 𝑅 ) )