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

Metamath Proof Explorer

Theorem lsmidl

Description: The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Hypotheses lsmidl.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
lsmidl.3 ⊢ ⊕ = ( LSSum ‘ 𝑅 )
lsmidl.4 ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
lsmidl.5 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
lsmidl.6 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
lsmidl.7 ⊢ ( 𝜑 → 𝐽 ∈ ( LIdeal ‘ 𝑅 ) )
Assertion lsmidl ( 𝜑 → ( 𝐼 ⊕ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 lsmidl.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 lsmidl.3 ⊢ ⊕ = ( LSSum ‘ 𝑅 )
3 lsmidl.4 ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
4 lsmidl.5 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 lsmidl.6 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
6 lsmidl.7 ⊢ ( 𝜑 → 𝐽 ∈ ( LIdeal ‘ 𝑅 ) )
7 1 2 3 4 5 6 lsmidllsp ⊢ ( 𝜑 → ( 𝐼 ⊕ 𝐽 ) = ( 𝐾 ‘ ( 𝐼 ∪ 𝐽 ) ) )
8 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
9 4 8 syl ⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ LMod )
10 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
11 1 10 lidlss ⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
12 5 11 syl ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
13 1 10 lidlss ⊢ ( 𝐽 ∈ ( LIdeal ‘ 𝑅 ) → 𝐽 ⊆ 𝐵 )
14 6 13 syl ⊢ ( 𝜑 → 𝐽 ⊆ 𝐵 )
15 12 14 unssd ⊢ ( 𝜑 → ( 𝐼 ∪ 𝐽 ) ⊆ 𝐵 )
16 rlmbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
17 1 16 eqtri ⊢ 𝐵 = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
18 lidlval ⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
19 rspval ⊢ ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
20 3 19 eqtri ⊢ 𝐾 = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
21 17 18 20 lspcl ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ ( 𝐼 ∪ 𝐽 ) ⊆ 𝐵 ) → ( 𝐾 ‘ ( 𝐼 ∪ 𝐽 ) ) ∈ ( LIdeal ‘ 𝑅 ) )
22 9 15 21 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐼 ∪ 𝐽 ) ) ∈ ( LIdeal ‘ 𝑅 ) )
23 7 22 eqeltrd ⊢ ( 𝜑 → ( 𝐼 ⊕ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) )