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 ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
rnglidl1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion rnglidl1 ( 𝑅 ∈ Rng → 𝐵 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 rnglidl0.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 rnglidl1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 2 eqimssi ⊢ 𝐵 ⊆ ( Base ‘ 𝑅 )
4 3 a1i ⊢ ( 𝑅 ∈ Rng → 𝐵 ⊆ ( Base ‘ 𝑅 ) )
5 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
6 2 grpbn0 ⊢ ( 𝑅 ∈ Grp → 𝐵 ≠ ∅ )
7 5 6 syl ⊢ ( 𝑅 ∈ Rng → 𝐵 ≠ ∅ )
8 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
9 5 adantr ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 ∈ Grp )
10 simpl ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 ∈ Rng )
11 2 eqcomi ⊢ ( Base ‘ 𝑅 ) = 𝐵
12 11 eleq2i ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↔ 𝑥 ∈ 𝐵 )
13 12 biimpi ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) → 𝑥 ∈ 𝐵 )
14 13 3ad2ant1 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
15 14 adantl ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
16 simpr2 ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
17 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
18 2 17 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 )
19 10 15 16 18 syl3anc ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 )
20 simpr3 ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
21 2 8 9 19 20 grpcld ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
22 21 ralrimivvva ⊢ ( 𝑅 ∈ Rng → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
23 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
24 1 23 8 17 islidl ⊢ ( 𝐵 ∈ 𝑈 ↔ ( 𝐵 ⊆ ( Base ‘ 𝑅 ) ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 ) )
25 4 7 22 24 syl3anbrc ⊢ ( 𝑅 ∈ Rng → 𝐵 ∈ 𝑈 )