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 ‘ 𝑅 ) )