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	|- .x. = ( .r ` R )
Assertion	lidlmcl	|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )

Proof

Step	Hyp	Ref	Expression
1		lidlcl.u	|- U = ( LIdeal ` R )
2		lidlcl.b	|- B = ( Base ` R )
3		lidlmcl.t	|- .x. = ( .r ` R )
4		ringrng	|- ( R e. Ring -> R e. Rng )
5	4	adantr	|- ( ( R e. Ring /\ I e. U ) -> R e. Rng )
6		simpr	|- ( ( R e. Ring /\ I e. U ) -> I e. U )
7		eqid	|- ( 0g ` R ) = ( 0g ` R )
8	1 7	lidl0cl	|- ( ( R e. Ring /\ I e. U ) -> ( 0g ` R ) e. I )
9	5 6 8	3jca	|- ( ( R e. Ring /\ I e. U ) -> ( R e. Rng /\ I e. U /\ ( 0g ` R ) e. I ) )
10	7 2 3 1	rnglidlmcl	|- ( ( ( R e. Rng /\ I e. U /\ ( 0g ` R ) e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )
11	9 10	sylan	|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )