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

Metamath Proof Explorer

Theorem df2idl2

Description: Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025) (Proof shortened by AV, 18-Apr-2025)

Ref Expression
Hypotheses df2idl2rng.u 
|- U = ( 2Ideal ` R )
df2idl2rng.b 
|- B = ( Base ` R )
df2idl2rng.t 
|- .x. = ( .r ` R )
Assertion df2idl2 
|- ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) ) )

Proof

Step Hyp Ref Expression
1 df2idl2rng.u 
 |-  U = ( 2Ideal ` R )
2 df2idl2rng.b 
 |-  B = ( Base ` R )
3 df2idl2rng.t 
 |-  .x. = ( .r ` R )
4 1 eleq2i 
 |-  ( I e. U <-> I e. ( 2Ideal ` R ) )
5 4 biimpi 
 |-  ( I e. U -> I e. ( 2Ideal ` R ) )
6 5 2idllidld 
 |-  ( I e. U -> I e. ( LIdeal ` R ) )
7 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
8 7 lidlsubg 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( SubGrp ` R ) )
9 6 8 sylan2 
 |-  ( ( R e. Ring /\ I e. U ) -> I e. ( SubGrp ` R ) )
10 ringrng 
 |-  ( R e. Ring -> R e. Rng )
11 1 2 3 df2idl2rng 
 |-  ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) )
12 10 11 sylan 
 |-  ( ( R e. Ring /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) )
13 9 12 biadanid 
 |-  ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) ) )