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 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 lsmidllsp φ I ˙ J = K I J

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 rlmlsm R Ring LSSum R = LSSum ringLMod R
8 4 7 syl φ LSSum R = LSSum ringLMod R
9 2 8 syl5eq φ ˙ = LSSum ringLMod R
10 9 oveqd φ I ˙ J = I LSSum ringLMod R J
11 rlmlmod R Ring ringLMod R LMod
12 4 11 syl φ ringLMod R LMod
13 lidlval LIdeal R = LSubSp ringLMod R
14 rspval RSpan R = LSpan ringLMod R
15 3 14 eqtri K = LSpan ringLMod R
16 eqid LSSum ringLMod R = LSSum ringLMod R
17 13 15 16 lsmsp ringLMod R LMod I LIdeal R J LIdeal R I LSSum ringLMod R J = K I J
18 12 5 6 17 syl3anc φ I LSSum ringLMod R J = K I J
19 10 18 eqtrd φ I ˙ J = K I J