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 ‘ 𝑅 ) )