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 Rng B U

Proof

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