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 → 𝐵 ∈ 𝑈 )