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