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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐼 ⊕ 𝐽 ) = ( 𝐾 ‘ ( 𝐼 ∪ 𝐽 ) ) )