Theorem lidlrng

Description: A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020) (Proof shortened by AV, 11-Mar-2025)

	Ref	Expression
Hypotheses	lidlabl.l	⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
	lidlabl.i	⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
Assertion	lidlrng	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Rng )

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2		lidlabl.i	⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3		ringrng	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
4	3	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝑅 ∈ Rng )
5		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝑈 ∈ 𝐿 )
6	1	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝑈 ∈ ( SubGrp ‘ 𝑅 ) )
7	1 2	rnglidlrng	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐼 ∈ Rng )
8	4 5 6 7	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Rng )