Metamath Proof Explorer

Theorem lidlmcl

Description: An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Stefan O'Rear, 3-Jan-2015) (Proof shortened by AV, 31-Mar-2025)

		Ref	Expression
	Hypotheses	lidlcl.u	$⊢ U = LIdeal (R)$
		lidlcl.b	$⊢ B = {Base}_{R}$
		lidlmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	Assertion	lidlmcl	$⊢ ((R \in Ring \land I \in U) \land (X \in B \land Y \in I)) \to X \underset{˙}{\cdot} Y \in I$

Proof

Step	Hyp	Ref	Expression
1		lidlcl.u	$⊢ U = LIdeal (R)$
2		lidlcl.b	$⊢ B = {Base}_{R}$
3		lidlmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		ringrng	$⊢ R \in Ring \to R \in Rng$
5	4	adantr	$⊢ (R \in Ring \land I \in U) \to R \in Rng$
6		simpr	$⊢ (R \in Ring \land I \in U) \to I \in U$
7		eqid	$⊢ 0_{R} = 0_{R}$
8	1 7	lidl0cl	$⊢ (R \in Ring \land I \in U) \to 0_{R} \in I$
9	5 6 8	3jca	$⊢ (R \in Ring \land I \in U) \to (R \in Rng \land I \in U \land 0_{R} \in I)$
10	7 2 3 1	rnglidlmcl	$⊢ ((R \in Rng \land I \in U \land 0_{R} \in I) \land (X \in B \land Y \in I)) \to X \underset{˙}{\cdot} Y \in I$
11	9 10	sylan	$⊢ ((R \in Ring \land I \in U) \land (X \in B \land Y \in I)) \to X \underset{˙}{\cdot} Y \in I$