Metamath Proof Explorer

Theorem idladdcl

Description: An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypothesis idladdcl.1 
|- G = ( 1st ` R )
Assertion idladdcl 
|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A G B ) e. I )

Proof

Step Hyp Ref Expression
1 idladdcl.1 
 |-  G = ( 1st ` R )
2 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
3 eqid 
 |-  ran G = ran G
4 eqid 
 |-  ( GId ` G ) = ( GId ` G )
5 1 2 3 4 isidl 
 |-  ( R e. RingOps -> ( I e. ( Idl ` R ) <-> ( I C_ ran G /\ ( GId ` G ) e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. I /\ ( x ( 2nd ` R ) z ) e. I ) ) ) ) )
6 5 biimpa 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( I C_ ran G /\ ( GId ` G ) e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. I /\ ( x ( 2nd ` R ) z ) e. I ) ) ) )
7 6 simp3d 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. I /\ ( x ( 2nd ` R ) z ) e. I ) ) )
8 simpl 
 |-  ( ( A. y e. I ( x G y ) e. I /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. I /\ ( x ( 2nd ` R ) z ) e. I ) ) -> A. y e. I ( x G y ) e. I )
9 8 ralimi 
 |-  ( A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. I /\ ( x ( 2nd ` R ) z ) e. I ) ) -> A. x e. I A. y e. I ( x G y ) e. I )
10 7 9 syl 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> A. x e. I A. y e. I ( x G y ) e. I )
11 oveq1 
 |-  ( x = A -> ( x G y ) = ( A G y ) )
12 11 eleq1d 
 |-  ( x = A -> ( ( x G y ) e. I <-> ( A G y ) e. I ) )
13 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
14 13 eleq1d 
 |-  ( y = B -> ( ( A G y ) e. I <-> ( A G B ) e. I ) )
15 12 14 rspc2v 
 |-  ( ( A e. I /\ B e. I ) -> ( A. x e. I A. y e. I ( x G y ) e. I -> ( A G B ) e. I ) )
16 10 15 mpan9 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A G B ) e. I )