Theorem lsmidllsp

Description: The sum of two ideals is the ideal generated by their union. (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	lsmidllsp	$$⊢\phi \to I\underset{\dot{}}{\oplus }J=K\left(I\cup J\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		rlmlsm	$$⊢R\in \mathrm{Ring}\to \mathrm{LSSum}\left(R\right)=\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)$$
8	4 7	syl	$$⊢\phi \to \mathrm{LSSum}\left(R\right)=\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)$$
9	2 8	eqtrid	$$⊢\phi \to \underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)$$
10	9	oveqd	$$⊢\phi \to I\underset{\dot{}}{\oplus }J=I\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)J$$
11		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
12	4 11	syl	$$⊢\phi \to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
13		lidlval	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left(R\right)\right)$$
14		rspval	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
15	3 14	eqtri	$$⊢K=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
16		eqid	$$⊢\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)$$
17	13 15 16	lsmsp	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\wedge I\in \mathrm{LIdeal}\left(R\right)\wedge J\in \mathrm{LIdeal}\left(R\right)\right)\to I\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)J=K\left(I\cup J\right)$$
18	12 5 6 17	syl3anc	$$⊢\phi \to I\mathrm{LSSum}\left(\mathrm{ringLMod}\left(R\right)\right)J=K\left(I\cup J\right)$$
19	10 18	eqtrd	$$⊢\phi \to I\underset{\dot{}}{\oplus }J=K\left(I\cup J\right)$$