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

Metamath Proof Explorer

Theorem dflidl2rng

Description: Alternate (the usual textbook) definition of a (left) ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025)

Ref Expression
Hypotheses dflidl2rng.u 
|- U = ( LIdeal ` R )
dflidl2rng.b 
|- B = ( Base ` R )
dflidl2rng.t 
|- .x. = ( .r ` R )
Assertion dflidl2rng 
|- ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( x .x. y ) e. I ) )

Proof

Step Hyp Ref Expression
1 dflidl2rng.u 
 |-  U = ( LIdeal ` R )
2 dflidl2rng.b 
 |-  B = ( Base ` R )
3 dflidl2rng.t 
 |-  .x. = ( .r ` R )
4 simpll 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ I e. U ) -> R e. Rng )
5 simpr 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ I e. U ) -> I e. U )
6 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
7 6 subg0cl 
 |-  ( I e. ( SubGrp ` R ) -> ( 0g ` R ) e. I )
8 7 ad2antlr 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ I e. U ) -> ( 0g ` R ) e. I )
9 4 5 8 3jca 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ I e. U ) -> ( R e. Rng /\ I e. U /\ ( 0g ` R ) e. I ) )
10 6 2 3 1 rnglidlmcl 
 |-  ( ( ( R e. Rng /\ I e. U /\ ( 0g ` R ) e. I ) /\ ( x e. B /\ y e. I ) ) -> ( x .x. y ) e. I )
11 9 10 sylan 
 |-  ( ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ I e. U ) /\ ( x e. B /\ y e. I ) ) -> ( x .x. y ) e. I )
12 11 ralrimivva 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ I e. U ) -> A. x e. B A. y e. I ( x .x. y ) e. I )
13 2 subgss 
 |-  ( I e. ( SubGrp ` R ) -> I C_ B )
14 13 ad2antlr 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) -> I C_ B )
15 7 ne0d 
 |-  ( I e. ( SubGrp ` R ) -> I =/= (/) )
16 15 ad2antlr 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) -> I =/= (/) )
17 eqid 
 |-  ( +g ` R ) = ( +g ` R )
18 17 subgcl 
 |-  ( ( I e. ( SubGrp ` R ) /\ ( x .x. y ) e. I /\ z e. I ) -> ( ( x .x. y ) ( +g ` R ) z ) e. I )
19 18 ad5ant245 
 |-  ( ( ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) /\ ( x .x. y ) e. I ) /\ z e. I ) -> ( ( x .x. y ) ( +g ` R ) z ) e. I )
20 19 ralrimiva 
 |-  ( ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) /\ ( x .x. y ) e. I ) -> A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I )
21 20 ex 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) -> ( ( x .x. y ) e. I -> A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I ) )
22 21 ralimdvva 
 |-  ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( A. x e. B A. y e. I ( x .x. y ) e. I -> A. x e. B A. y e. I A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I ) )
23 22 imp 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) -> A. x e. B A. y e. I A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I )
24 1 2 17 3 islidl 
 |-  ( I e. U <-> ( I C_ B /\ I =/= (/) /\ A. x e. B A. y e. I A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I ) )
25 14 16 23 24 syl3anbrc 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) -> I e. U )
26 12 25 impbida 
 |-  ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( x .x. y ) e. I ) )