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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	lsmidl.3	⊢ ⊕ = ( LSSum ‘ 𝑅 )
	lsmidl.4	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	lsmidl.5	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	lsmidl.6	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
	lsmidl.7	⊢ ( 𝜑 → 𝐽 ∈ ( LIdeal ‘ 𝑅 ) )
Assertion	lsmidllsp	⊢ ( 𝜑 → ( 𝐼 ⊕ 𝐽 ) = ( 𝐾 ‘ ( 𝐼 ∪ 𝐽 ) ) )

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		rlmlsm	⊢ ( 𝑅 ∈ Ring → ( LSSum ‘ 𝑅 ) = ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) )
8	4 7	syl	⊢ ( 𝜑 → ( LSSum ‘ 𝑅 ) = ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) )
9	2 8	eqtrid	⊢ ( 𝜑 → ⊕ = ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) )
10	9	oveqd	⊢ ( 𝜑 → ( 𝐼 ⊕ 𝐽 ) = ( 𝐼 ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) 𝐽 ) )
11		rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
12	4 11	syl	⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ LMod )
13		lidlval	⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
14		rspval	⊢ ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
15	3 14	eqtri	⊢ 𝐾 = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
16		eqid	⊢ ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSSum ‘ ( ringLMod ‘ 𝑅 ) )
17	13 15 16	lsmsp	⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝐼 ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) 𝐽 ) = ( 𝐾 ‘ ( 𝐼 ∪ 𝐽 ) ) )
18	12 5 6 17	syl3anc	⊢ ( 𝜑 → ( 𝐼 ( LSSum ‘ ( ringLMod ‘ 𝑅 ) ) 𝐽 ) = ( 𝐾 ‘ ( 𝐼 ∪ 𝐽 ) ) )
19	10 18	eqtrd	⊢ ( 𝜑 → ( 𝐼 ⊕ 𝐽 ) = ( 𝐾 ‘ ( 𝐼 ∪ 𝐽 ) ) )