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 
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) -> ( I i^i J ) e. ( Idl ` R ) )

Proof

Step Hyp Ref Expression
1 intprg 
 |-  ( ( I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) -> |^| { I , J } = ( I i^i J ) )
2 1 3adant1 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) -> |^| { I , J } = ( I i^i J ) )
3 prnzg 
 |-  ( I e. ( Idl ` R ) -> { I , J } =/= (/) )
4 3 adantr 
 |-  ( ( I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) -> { I , J } =/= (/) )
5 prssi 
 |-  ( ( I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) -> { I , J } C_ ( Idl ` R ) )
6 4 5 jca 
 |-  ( ( I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) -> ( { I , J } =/= (/) /\ { I , J } C_ ( Idl ` R ) ) )
7 intidl 
 |-  ( ( R e. RingOps /\ { I , J } =/= (/) /\ { I , J } C_ ( Idl ` R ) ) -> |^| { I , J } e. ( Idl ` R ) )
8 7 3expb 
 |-  ( ( R e. RingOps /\ ( { I , J } =/= (/) /\ { I , J } C_ ( Idl ` R ) ) ) -> |^| { I , J } e. ( Idl ` R ) )
9 6 8 sylan2 
 |-  ( ( R e. RingOps /\ ( I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) ) -> |^| { I , J } e. ( Idl ` R ) )
10 9 3impb 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) -> |^| { I , J } e. ( Idl ` R ) )
11 2 10 eqeltrrd 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ J e. ( Idl ` R ) ) -> ( I i^i J ) e. ( Idl ` R ) )