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	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	lidlsubcl.m	⊢ − = ( -g ‘ 𝑅 )
Assertion	lidlsubcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 − 𝑌 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		lidlcl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		lidlsubcl.m	⊢ − = ( -g ‘ 𝑅 )
3	1	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
4	3	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
5		simp3l	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑋 ∈ 𝐼 )
6		simp3r	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑌 ∈ 𝐼 )
7	2	subgsubcl	⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 − 𝑌 ) ∈ 𝐼 )
8	4 5 6 7	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 − 𝑌 ) ∈ 𝐼 )
9	8	3expa	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 − 𝑌 ) ∈ 𝐼 )