Metamath Proof Explorer

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)

Step	Hyp	Ref	Expression
1		lidlabl.l	$⊢ L = LIdeal (R)$
2		lidlabl.i	$⊢ I = R ↾_{𝑠} U$
3		ringrng	$⊢ R \in Ring \to R \in Rng$
4	3	adantr	$⊢ (R \in Ring \land U \in L) \to R \in Rng$
5		simpr	$⊢ (R \in Ring \land U \in L) \to U \in L$
6	1	lidlsubg	$⊢ (R \in Ring \land U \in L) \to U \in SubGrp (R)$
7	1 2	rnglidlrng	$⊢ (R \in Rng \land U \in L \land U \in SubGrp (R)) \to I \in Rng$
8	4 5 6 7	syl3anc	$⊢ (R \in Ring \land U \in L) \to I \in Rng$