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=BaseR
Assertion rnglidl1 ⊢R∈Rng→B∈U

Proof

Step Hyp Ref Expression
1 rnglidl0.u ⊢U=LIdeal⁡R
2 rnglidl1.b ⊢B=BaseR
3 2 eqimssi ⊢B⊆BaseR
4 3 a1i ⊢R∈Rng→B⊆BaseR
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∈BaseR∧y∈B∧z∈B→R∈Grp
10 simpl ⊢R∈Rng∧x∈BaseR∧y∈B∧z∈B→R∈Rng
11 2 eqcomi ⊢BaseR=B
12 11 eleq2i ⊢x∈BaseR↔x∈B
13 12 biimpi ⊢x∈BaseR→x∈B
14 13 3ad2ant1 ⊢x∈BaseR∧y∈B∧z∈B→x∈B
15 14 adantl ⊢R∈Rng∧x∈BaseR∧y∈B∧z∈B→x∈B
16 simpr2 ⊢R∈Rng∧x∈BaseR∧y∈B∧z∈B→y∈B
17 eqid ⊢⋅R=⋅R
18 2 17 rngcl ⊢R∈Rng∧x∈B∧y∈B→x⋅Ry∈B
19 10 15 16 18 syl3anc ⊢R∈Rng∧x∈BaseR∧y∈B∧z∈B→x⋅Ry∈B
20 simpr3 ⊢R∈Rng∧x∈BaseR∧y∈B∧z∈B→z∈B
21 2 8 9 19 20 grpcld ⊢R∈Rng∧x∈BaseR∧y∈B∧z∈B→x⋅Ry+Rz∈B
22 21 ralrimivvva ⊢R∈Rng→∀x∈BaseR∀y∈B∀z∈Bx⋅Ry+Rz∈B
23 eqid ⊢BaseR=BaseR
24 1 23 8 17 islidl ⊢B∈U↔B⊆BaseR∧B≠∅∧∀x∈BaseR∀y∈B∀z∈Bx⋅Ry+Rz∈B
25 4 7 22 24 syl3anbrc ⊢R∈Rng→B∈U