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