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

Metamath Proof Explorer

Theorem lidlsubcl

Description: An ideal is closed under subtraction. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by OpenAI, 25-Mar-2020)

Ref Expression
Hypotheses lidlcl.u 
|- U = ( LIdeal ` R )
lidlsubcl.m 
|- .- = ( -g ` R )
Assertion lidlsubcl 
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X .- Y ) e. I )

Proof

Step Hyp Ref Expression
1 lidlcl.u 
 |-  U = ( LIdeal ` R )
2 lidlsubcl.m 
 |-  .- = ( -g ` R )
3 1 lidlsubg 
 |-  ( ( R e. Ring /\ I e. U ) -> I e. ( SubGrp ` R ) )
4 3 3adant3 
 |-  ( ( R e. Ring /\ I e. U /\ ( X e. I /\ Y e. I ) ) -> I e. ( SubGrp ` R ) )
5 simp3l 
 |-  ( ( R e. Ring /\ I e. U /\ ( X e. I /\ Y e. I ) ) -> X e. I )
6 simp3r 
 |-  ( ( R e. Ring /\ I e. U /\ ( X e. I /\ Y e. I ) ) -> Y e. I )
7 2 subgsubcl 
 |-  ( ( I e. ( SubGrp ` R ) /\ X e. I /\ Y e. I ) -> ( X .- Y ) e. I )
8 4 5 6 7 syl3anc 
 |-  ( ( R e. Ring /\ I e. U /\ ( X e. I /\ Y e. I ) ) -> ( X .- Y ) e. I )
9 8 3expa 
 |-  ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X .- Y ) e. I )