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