This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lidlsubg

Description: An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypothesis lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion lidlsubg ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 2 1 lidlss ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
4 3 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
5 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6 1 5 lidl0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
7 6 ne0d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ≠ ∅ )
8 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
9 1 8 lidlacl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
10 9 anassrs ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
11 10 ralrimiva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝐼 ) → ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
12 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
13 1 12 lidlnegcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑥 ∈ 𝐼 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 )
14 13 3expa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 )
15 11 14 jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝐼 ) → ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 ) )
16 15 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 ) )
17 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
18 17 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝑅 ∈ Grp )
19 2 8 12 issubg2 ⊢ ( 𝑅 ∈ Grp → ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ↔ ( 𝐼 ⊆ ( Base ‘ 𝑅 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 ) ) ) )
20 18 19 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ↔ ( 𝐼 ⊆ ( Base ‘ 𝑅 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 ) ) ) )
21 4 7 16 20 mpbir3and ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )