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 ‘ 𝑅 ) )