| 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 ) ) |