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