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 
|- ( ph -> R e. Ring )
lsmidl.6 
|- ( ph -> I e. ( LIdeal ` R ) )
lsmidl.7 
|- ( ph -> J e. ( LIdeal ` R ) )
Assertion lsmidllsp 
|- ( ph -> ( I .(+) J ) = ( K ` ( I u. 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 
 |-  ( ph -> R e. Ring )
5 lsmidl.6 
 |-  ( ph -> I e. ( LIdeal ` R ) )
6 lsmidl.7 
 |-  ( ph -> J e. ( LIdeal ` R ) )
7 rlmlsm 
 |-  ( R e. Ring -> ( LSSum ` R ) = ( LSSum ` ( ringLMod ` R ) ) )
8 4 7 syl 
 |-  ( ph -> ( LSSum ` R ) = ( LSSum ` ( ringLMod ` R ) ) )
9 2 8 syl5eq 
 |-  ( ph -> .(+) = ( LSSum ` ( ringLMod ` R ) ) )
10 9 oveqd 
 |-  ( ph -> ( I .(+) J ) = ( I ( LSSum ` ( ringLMod ` R ) ) J ) )
11 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
12 4 11 syl 
 |-  ( ph -> ( ringLMod ` R ) e. 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 ) e. LMod /\ I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) -> ( I ( LSSum ` ( ringLMod ` R ) ) J ) = ( K ` ( I u. J ) ) )
18 12 5 6 17 syl3anc 
 |-  ( ph -> ( I ( LSSum ` ( ringLMod ` R ) ) J ) = ( K ` ( I u. J ) ) )
19 10 18 eqtrd 
 |-  ( ph -> ( I .(+) J ) = ( K ` ( I u. J ) ) )