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	|- L = ( LIdeal ` R )
	lidlabl.i	|- I = ( R |`s U )
Assertion	lidlrng	|- ( ( R e. Ring /\ U e. L ) -> I e. Rng )

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	|- L = ( LIdeal ` R )
2		lidlabl.i	|- I = ( R |`s U )
3		ringrng	|- ( R e. Ring -> R e. Rng )
4	3	adantr	|- ( ( R e. Ring /\ U e. L ) -> R e. Rng )
5		simpr	|- ( ( R e. Ring /\ U e. L ) -> U e. L )
6	1	lidlsubg	|- ( ( R e. Ring /\ U e. L ) -> U e. ( SubGrp ` R ) )
7	1 2	rnglidlrng	|- ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> I e. Rng )
8	4 5 6 7	syl3anc	|- ( ( R e. Ring /\ U e. L ) -> I e. Rng )