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 = 1 st R
Assertion idladdcl R RingOps I Idl R A I B I A G B I

Proof

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