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 ∈ 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