Metamath Proof Explorer

Theorem inlidl

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

Ref Expression
Assertion inlidl 
|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> ( I i^i J ) e. ( LIdeal ` R ) )

Proof

Step Hyp Ref Expression
1 intprg 
 |-  ( ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> |^| { I , J } = ( I i^i J ) )
2 1 3adant1 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> |^| { I , J } = ( I i^i J ) )
3 simp1 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> R e. Ring )
4 prnzg 
 |-  ( I e. ( LIdeal ` R ) -> { I , J } =/= (/) )
5 4 3ad2ant2 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> { I , J } =/= (/) )
6 prssi 
 |-  ( ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> { I , J } C_ ( LIdeal ` R ) )
7 6 3adant1 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> { I , J } C_ ( LIdeal ` R ) )
8 intlidl 
 |-  ( ( R e. Ring /\ { I , J } =/= (/) /\ { I , J } C_ ( LIdeal ` R ) ) -> |^| { I , J } e. ( LIdeal ` R ) )
9 3 5 7 8 syl3anc 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> |^| { I , J } e. ( LIdeal ` R ) )
10 2 9 eqeltrrd 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> ( I i^i J ) e. ( LIdeal ` R ) )