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 ⊢ 𝑈 = ( 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 ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 − 𝑌 ) ∈ 𝐼 )