Metamath Proof Explorer


Theorem lsmidl

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

Ref Expression
Hypotheses lsmidl.1 B = Base R
lsmidl.3 ˙ = LSSum R
lsmidl.4 K = RSpan R
lsmidl.5 φ R Ring
lsmidl.6 φ I LIdeal R
lsmidl.7 φ J LIdeal R
Assertion lsmidl φ I ˙ J LIdeal R

Proof

Step Hyp Ref Expression
1 lsmidl.1 B = Base R
2 lsmidl.3 ˙ = LSSum R
3 lsmidl.4 K = RSpan R
4 lsmidl.5 φ R Ring
5 lsmidl.6 φ I LIdeal R
6 lsmidl.7 φ J LIdeal R
7 1 2 3 4 5 6 lsmidllsp φ I ˙ J = K I J
8 rlmlmod R Ring ringLMod R LMod
9 4 8 syl φ ringLMod R LMod
10 eqid LIdeal R = LIdeal R
11 1 10 lidlss I LIdeal R I B
12 5 11 syl φ I B
13 1 10 lidlss J LIdeal R J B
14 6 13 syl φ J B
15 12 14 unssd φ I J B
16 rlmbas Base R = Base ringLMod R
17 1 16 eqtri B = Base ringLMod R
18 lidlval LIdeal R = LSubSp ringLMod R
19 rspval RSpan R = LSpan ringLMod R
20 3 19 eqtri K = LSpan ringLMod R
21 17 18 20 lspcl ringLMod R LMod I J B K I J LIdeal R
22 9 15 21 syl2anc φ K I J LIdeal R
23 7 22 eqeltrd φ I ˙ J LIdeal R