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

Metamath Proof Explorer

Theorem rnglidl1

Description: The base set of every non-unital ring is an ideal. For unital rings, such ideals are called "unit ideals", see lidl1 . (Contributed by AV, 19-Feb-2025)

Ref Expression
Hypotheses rnglidl0.u 
|- U = ( LIdeal ` R )
rnglidl1.b 
|- B = ( Base ` R )
Assertion rnglidl1 
|- ( R e. Rng -> B e. U )

Proof

Step Hyp Ref Expression
1 rnglidl0.u 
 |-  U = ( LIdeal ` R )
2 rnglidl1.b 
 |-  B = ( Base ` R )
3 2 eqimssi 
 |-  B C_ ( Base ` R )
4 3 a1i 
 |-  ( R e. Rng -> B C_ ( Base ` R ) )
5 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
6 2 grpbn0 
 |-  ( R e. Grp -> B =/= (/) )
7 5 6 syl 
 |-  ( R e. Rng -> B =/= (/) )
8 eqid 
 |-  ( +g ` R ) = ( +g ` R )
9 5 adantr 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. B /\ z e. B ) ) -> R e. Grp )
10 simpl 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. B /\ z e. B ) ) -> R e. Rng )
11 2 eqcomi 
 |-  ( Base ` R ) = B
12 11 eleq2i 
 |-  ( x e. ( Base ` R ) <-> x e. B )
13 12 biimpi 
 |-  ( x e. ( Base ` R ) -> x e. B )
14 13 3ad2ant1 
 |-  ( ( x e. ( Base ` R ) /\ y e. B /\ z e. B ) -> x e. B )
15 14 adantl 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. B /\ z e. B ) ) -> x e. B )
16 simpr2 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. B /\ z e. B ) ) -> y e. B )
17 eqid 
 |-  ( .r ` R ) = ( .r ` R )
18 2 17 rngcl 
 |-  ( ( R e. Rng /\ x e. B /\ y e. B ) -> ( x ( .r ` R ) y ) e. B )
19 10 15 16 18 syl3anc 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. B /\ z e. B ) ) -> ( x ( .r ` R ) y ) e. B )
20 simpr3 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. B /\ z e. B ) ) -> z e. B )
21 2 8 9 19 20 grpcld 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. B /\ z e. B ) ) -> ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. B )
22 21 ralrimivvva 
 |-  ( R e. Rng -> A. x e. ( Base ` R ) A. y e. B A. z e. B ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. B )
23 eqid 
 |-  ( Base ` R ) = ( Base ` R )
24 1 23 8 17 islidl 
 |-  ( B e. U <-> ( B C_ ( Base ` R ) /\ B =/= (/) /\ A. x e. ( Base ` R ) A. y e. B A. z e. B ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. B ) )
25 4 7 22 24 syl3anbrc 
 |-  ( R e. Rng -> B e. U )