This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- .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 )