| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lidlcl.u |
|- U = ( LIdeal ` R ) |
| 2 |
|
lidl0cl.z |
|- .0. = ( 0g ` R ) |
| 3 |
|
rlm0 |
|- ( 0g ` R ) = ( 0g ` ( ringLMod ` R ) ) |
| 4 |
2 3
|
eqtri |
|- .0. = ( 0g ` ( ringLMod ` R ) ) |
| 5 |
|
rlmlmod |
|- ( R e. Ring -> ( ringLMod ` R ) e. LMod ) |
| 6 |
|
simpr |
|- ( ( R e. Ring /\ I e. U ) -> I e. U ) |
| 7 |
|
lidlval |
|- ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) ) |
| 8 |
1 7
|
eqtri |
|- U = ( LSubSp ` ( ringLMod ` R ) ) |
| 9 |
6 8
|
eleqtrdi |
|- ( ( R e. Ring /\ I e. U ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) ) |
| 10 |
|
eqid |
|- ( 0g ` ( ringLMod ` R ) ) = ( 0g ` ( ringLMod ` R ) ) |
| 11 |
|
eqid |
|- ( LSubSp ` ( ringLMod ` R ) ) = ( LSubSp ` ( ringLMod ` R ) ) |
| 12 |
10 11
|
lss0cl |
|- ( ( ( ringLMod ` R ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) ) -> ( 0g ` ( ringLMod ` R ) ) e. I ) |
| 13 |
5 9 12
|
syl2an2r |
|- ( ( R e. Ring /\ I e. U ) -> ( 0g ` ( ringLMod ` R ) ) e. I ) |
| 14 |
4 13
|
eqeltrid |
|- ( ( R e. Ring /\ I e. U ) -> .0. e. I ) |