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