lidlsubg

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

		Ref	Expression
	Hypothesis	lidlcl.u	$⊢ U = LIdeal (R)$
	Assertion	lidlsubg	$⊢ (R \in Ring \land I \in U) \to I \in SubGrp (R)$

Proof

Step	Hyp	Ref	Expression
1		lidlcl.u	$⊢ U = LIdeal (R)$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	2 1	lidlss	$⊢ I \in U \to I \subseteq {Base}_{R}$
4	3	adantl	$⊢ (R \in Ring \land I \in U) \to I \subseteq {Base}_{R}$
5		eqid	$⊢ 0_{R} = 0_{R}$
6	1 5	lidl0cl	$⊢ (R \in Ring \land I \in U) \to 0_{R} \in I$
7	6	ne0d	$⊢ (R \in Ring \land I \in U) \to I \neq \emptyset$
8		eqid	$⊢ +_{R} = +_{R}$
9	1 8	lidlacl	$⊢ ((R \in Ring \land I \in U) \land (x \in I \land y \in I)) \to x +_{R} y \in I$
10	9	anassrs	$⊢ (((R \in Ring \land I \in U) \land x \in I) \land y \in I) \to x +_{R} y \in I$
11	10	ralrimiva	$⊢ ((R \in Ring \land I \in U) \land x \in I) \to \forall y \in I x +_{R} y \in I$
12		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
13	1 12	lidlnegcl	$⊢ (R \in Ring \land I \in U \land x \in I) \to {inv}_{g} (R) (x) \in I$
14	13	3expa	$⊢ ((R \in Ring \land I \in U) \land x \in I) \to {inv}_{g} (R) (x) \in I$
15	11 14	jca	$⊢ ((R \in Ring \land I \in U) \land x \in I) \to (\forall y \in I x +_{R} y \in I \land {inv}_{g} (R) (x) \in I)$
16	15	ralrimiva	$⊢ (R \in Ring \land I \in U) \to \forall x \in I (\forall y \in I x +_{R} y \in I \land {inv}_{g} (R) (x) \in I)$
17		ringgrp	$⊢ R \in Ring \to R \in Grp$
18	17	adantr	$⊢ (R \in Ring \land I \in U) \to R \in Grp$
19	2 8 12	issubg2	$⊢ R \in Grp \to (I \in SubGrp (R) \leftrightarrow (I \subseteq {Base}_{R} \land I \neq \emptyset \land \forall x \in I (\forall y \in I x +_{R} y \in I \land {inv}_{g} (R) (x) \in I)))$
20	18 19	syl	$⊢ (R \in Ring \land I \in U) \to (I \in SubGrp (R) \leftrightarrow (I \subseteq {Base}_{R} \land I \neq \emptyset \land \forall x \in I (\forall y \in I x +_{R} y \in I \land {inv}_{g} (R) (x) \in I)))$
21	4 7 16 20	mpbir3and	$⊢ (R \in Ring \land I \in U) \to I \in SubGrp (R)$

Metamath Proof Explorer

Theorem lidlsubg

Proof