Theorem 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 e. Ring /\ I e. U ) -> I e. ( SubGrp ` R ) )

Proof

Step	Hyp	Ref	Expression
1		lidlcl.u	|- U = ( LIdeal ` R )
2		eqid	|- ( Base ` R ) = ( Base ` R )
3	2 1	lidlss	|- ( I e. U -> I C_ ( Base ` R ) )
4	3	adantl	|- ( ( R e. Ring /\ I e. U ) -> I C_ ( Base ` R ) )
5		eqid	|- ( 0g ` R ) = ( 0g ` R )
6	1 5	lidl0cl	|- ( ( R e. Ring /\ I e. U ) -> ( 0g ` R ) e. I )
7	6	ne0d	|- ( ( R e. Ring /\ I e. U ) -> I =/= (/) )
8		eqid	|- ( +g ` R ) = ( +g ` R )
9	1 8	lidlacl	|- ( ( ( R e. Ring /\ I e. U ) /\ ( x e. I /\ y e. I ) ) -> ( x ( +g ` R ) y ) e. I )
10	9	anassrs	|- ( ( ( ( R e. Ring /\ I e. U ) /\ x e. I ) /\ y e. I ) -> ( x ( +g ` R ) y ) e. I )
11	10	ralrimiva	|- ( ( ( R e. Ring /\ I e. U ) /\ x e. I ) -> A. y e. I ( x ( +g ` R ) y ) e. I )
12		eqid	|- ( invg ` R ) = ( invg ` R )
13	1 12	lidlnegcl	|- ( ( R e. Ring /\ I e. U /\ x e. I ) -> ( ( invg ` R ) ` x ) e. I )
14	13	3expa	|- ( ( ( R e. Ring /\ I e. U ) /\ x e. I ) -> ( ( invg ` R ) ` x ) e. I )
15	11 14	jca	|- ( ( ( R e. Ring /\ I e. U ) /\ x e. I ) -> ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I ) )
16	15	ralrimiva	|- ( ( R e. Ring /\ I e. U ) -> A. x e. I ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I ) )
17		ringgrp	|- ( R e. Ring -> R e. Grp )
18	17	adantr	|- ( ( R e. Ring /\ I e. U ) -> R e. Grp )
19	2 8 12	issubg2	|- ( R e. Grp -> ( I e. ( SubGrp ` R ) <-> ( I C_ ( Base ` R ) /\ I =/= (/) /\ A. x e. I ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I ) ) ) )
20	18 19	syl	|- ( ( R e. Ring /\ I e. U ) -> ( I e. ( SubGrp ` R ) <-> ( I C_ ( Base ` R ) /\ I =/= (/) /\ A. x e. I ( A. y e. I ( x ( +g ` R ) y ) e. I /\ ( ( invg ` R ) ` x ) e. I ) ) ) )
21	4 7 16 20	mpbir3and	|- ( ( R e. Ring /\ I e. U ) -> I e. ( SubGrp ` R ) )