Theorem lsmidl

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

	Ref	Expression
Hypotheses	lsmidl.1	$$⊢B={\mathrm{Base}}_R$$
	lsmidl.3	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(R\right)$$
	lsmidl.4	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	lsmidl.5	$$⊢\phi \to R\in \mathrm{Ring}$$
	lsmidl.6	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
	lsmidl.7	$$⊢\phi \to J\in \mathrm{LIdeal}\left(R\right)$$
Assertion	lsmidl	$$⊢\phi \to I\underset{\dot{}}{\oplus }J\in \mathrm{LIdeal}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsmidl.1	$$⊢B={\mathrm{Base}}_R$$
2		lsmidl.3	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(R\right)$$
3		lsmidl.4	$$⊢K=\mathrm{RSpan}\left(R\right)$$
4		lsmidl.5	$$⊢\phi \to R\in \mathrm{Ring}$$
5		lsmidl.6	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
6		lsmidl.7	$$⊢\phi \to J\in \mathrm{LIdeal}\left(R\right)$$
7	1 2 3 4 5 6	lsmidllsp	$$⊢\phi \to I\underset{\dot{}}{\oplus }J=K\left(I\cup J\right)$$
8		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
9	4 8	syl	$$⊢\phi \to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
10		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
11	1 10	lidlss	$$⊢I\in \mathrm{LIdeal}\left(R\right)\to I\subseteq B$$
12	5 11	syl	$$⊢\phi \to I\subseteq B$$
13	1 10	lidlss	$$⊢J\in \mathrm{LIdeal}\left(R\right)\to J\subseteq B$$
14	6 13	syl	$$⊢\phi \to J\subseteq B$$
15	12 14	unssd	$$⊢\phi \to I\cup J\subseteq B$$
16		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
17	1 16	eqtri	$$⊢B={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
18		lidlval	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
19		rspval	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
20	3 19	eqtri	$$⊢K=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
21	17 18 20	lspcl	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\wedge I\cup J\subseteq B\right)\to K\left(I\cup J\right)\in \mathrm{LIdeal}\left(R\right)$$
22	9 15 21	syl2anc	$$⊢\phi \to K\left(I\cup J\right)\in \mathrm{LIdeal}\left(R\right)$$
23	7 22	eqeltrd	$$⊢\phi \to I\underset{\dot{}}{\oplus }J\in \mathrm{LIdeal}\left(R\right)$$