Metamath Proof Explorer


Theorem idladdcl

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

Ref Expression
Hypothesis idladdcl.1 𝐺 = ( 1st𝑅 )
Assertion idladdcl ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴𝐼𝐵𝐼 ) ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 idladdcl.1 𝐺 = ( 1st𝑅 )
2 eqid ( 2nd𝑅 ) = ( 2nd𝑅 )
3 eqid ran 𝐺 = ran 𝐺
4 eqid ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
5 1 2 3 4 isidl ( 𝑅 ∈ RingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ ran 𝐺 ∧ ( GId ‘ 𝐺 ) ∈ 𝐼 ∧ ∀ 𝑥𝐼 ( ∀ 𝑦𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2nd𝑅 ) 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 ( 2nd𝑅 ) 𝑧 ) ∈ 𝐼 ) ) ) ) )
6 5 biimpa ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝐼 ⊆ ran 𝐺 ∧ ( GId ‘ 𝐺 ) ∈ 𝐼 ∧ ∀ 𝑥𝐼 ( ∀ 𝑦𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2nd𝑅 ) 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 ( 2nd𝑅 ) 𝑧 ) ∈ 𝐼 ) ) ) )
7 6 simp3d ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ∀ 𝑥𝐼 ( ∀ 𝑦𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2nd𝑅 ) 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 ( 2nd𝑅 ) 𝑧 ) ∈ 𝐼 ) ) )
8 simpl ( ( ∀ 𝑦𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2nd𝑅 ) 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 ( 2nd𝑅 ) 𝑧 ) ∈ 𝐼 ) ) → ∀ 𝑦𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 )
9 8 ralimi ( ∀ 𝑥𝐼 ( ∀ 𝑦𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑧 ( 2nd𝑅 ) 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 ( 2nd𝑅 ) 𝑧 ) ∈ 𝐼 ) ) → ∀ 𝑥𝐼𝑦𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 )
10 7 9 syl ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ∀ 𝑥𝐼𝑦𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 )
11 oveq1 ( 𝑥 = 𝐴 → ( 𝑥 𝐺 𝑦 ) = ( 𝐴 𝐺 𝑦 ) )
12 11 eleq1d ( 𝑥 = 𝐴 → ( ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ↔ ( 𝐴 𝐺 𝑦 ) ∈ 𝐼 ) )
13 oveq2 ( 𝑦 = 𝐵 → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 𝐵 ) )
14 13 eleq1d ( 𝑦 = 𝐵 → ( ( 𝐴 𝐺 𝑦 ) ∈ 𝐼 ↔ ( 𝐴 𝐺 𝐵 ) ∈ 𝐼 ) )
15 12 14 rspc2v ( ( 𝐴𝐼𝐵𝐼 ) → ( ∀ 𝑥𝐼𝑦𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 → ( 𝐴 𝐺 𝐵 ) ∈ 𝐼 ) )
16 10 15 mpan9 ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴𝐼𝐵𝐼 ) ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝐼 )