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 )