Metamath Proof Explorer

Theorem df2idl2crng

Description: The predicate "is an ideal of the commutative ring R ". (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 27-Jun-2026)

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

Proof

Step Hyp Ref Expression
1 df2idl2crng.u 
 |-  U = ( 2Ideal ` R )
2 df2idl2crng.b 
 |-  B = ( Base ` R )
3 df2idl2crng.t 
 |-  .x. = ( .r ` R )
4 crngring 
 |-  ( R e. CRing -> R e. Ring )
5 1 2 3 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 ) ) ) )
6 4 5 syl 
 |-  ( R e. CRing -> ( 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 ) ) ) )
7 simpll 
 |-  ( ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) -> R e. CRing )
8 simpl 
 |-  ( ( x e. B /\ y e. I ) -> x e. B )
9 8 adantl 
 |-  ( ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) -> x e. B )
10 2 subgss 
 |-  ( I e. ( SubGrp ` R ) -> I C_ B )
11 10 adantl 
 |-  ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) -> I C_ B )
12 11 sseld 
 |-  ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) -> ( y e. I -> y e. B ) )
13 12 adantld 
 |-  ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) -> ( ( x e. B /\ y e. I ) -> y e. B ) )
14 13 imp 
 |-  ( ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) -> y e. B )
15 2 3 7 9 14 crngcomd 
 |-  ( ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) -> ( x .x. y ) = ( y .x. x ) )
16 15 eleq1d 
 |-  ( ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) -> ( ( x .x. y ) e. I <-> ( y .x. x ) e. I ) )
17 16 pm4.71da 
 |-  ( ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) -> ( ( x .x. y ) e. I <-> ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) )
18 17 bicomd 
 |-  ( ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) /\ ( x e. B /\ y e. I ) ) -> ( ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) <-> ( x .x. y ) e. I ) )
19 18 2ralbidva 
 |-  ( ( R e. CRing /\ I e. ( SubGrp ` R ) ) -> ( A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) <-> A. x e. B A. y e. I ( x .x. y ) e. I ) )
20 19 pm5.32da 
 |-  ( R e. CRing -> ( ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) ) )
21 6 20 bitrd 
 |-  ( R e. CRing -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) ) )