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 )