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 
|- ( ph -> R e. Ring )
lsmidl.6 
|- ( ph -> I e. ( LIdeal ` R ) )
lsmidl.7 
|- ( ph -> J e. ( LIdeal ` R ) )
Assertion lsmidl 
|- ( ph -> ( I .(+) J ) e. ( 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 
 |-  ( ph -> R e. Ring )
5 lsmidl.6 
 |-  ( ph -> I e. ( LIdeal ` R ) )
6 lsmidl.7 
 |-  ( ph -> J e. ( LIdeal ` R ) )
7 1 2 3 4 5 6 lsmidllsp 
 |-  ( ph -> ( I .(+) J ) = ( K ` ( I u. J ) ) )
8 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
9 4 8 syl 
 |-  ( ph -> ( ringLMod ` R ) e. LMod )
10 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
11 1 10 lidlss 
 |-  ( I e. ( LIdeal ` R ) -> I C_ B )
12 5 11 syl 
 |-  ( ph -> I C_ B )
13 1 10 lidlss 
 |-  ( J e. ( LIdeal ` R ) -> J C_ B )
14 6 13 syl 
 |-  ( ph -> J C_ B )
15 12 14 unssd 
 |-  ( ph -> ( I u. J ) C_ 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 ) e. LMod /\ ( I u. J ) C_ B ) -> ( K ` ( I u. J ) ) e. ( LIdeal ` R ) )
22 9 15 21 syl2anc 
 |-  ( ph -> ( K ` ( I u. J ) ) e. ( LIdeal ` R ) )
23 7 22 eqeltrd 
 |-  ( ph -> ( I .(+) J ) e. ( LIdeal ` R ) )