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

Metamath Proof Explorer

Theorem lidlacl

Description: An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
lidlacl.p ⊢ + = ( +g ‘ 𝑅 )
Assertion lidlacl ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 lidlacl.p ⊢ + = ( +g ‘ 𝑅 )
3 rlmplusg ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
4 2 3 eqtri ⊢ + = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
5 4 oveqi ⊢ ( 𝑋 + 𝑌 ) = ( 𝑋 ( +g ‘ ( ringLMod ‘ 𝑅 ) ) 𝑌 )
6 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
7 6 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( ringLMod ‘ 𝑅 ) ∈ LMod )
8 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ 𝑈 )
9 lidlval ⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
10 1 9 eqtri ⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
11 8 10 eleqtrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
12 7 11 jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ) )
13 eqid ⊢ ( +g ‘ ( ringLMod ‘ 𝑅 ) ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
14 eqid ⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
15 13 14 lssvacl ⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( +g ‘ ( ringLMod ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 )
16 12 15 sylan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( +g ‘ ( ringLMod ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 )
17 5 16 eqeltrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐼 )