Step |
Hyp |
Ref |
Expression |
1 |
|
lidlcl.u |
|- U = ( LIdeal ` R ) |
2 |
|
lidlacl.p |
|- .+ = ( +g ` R ) |
3 |
|
rlmplusg |
|- ( +g ` R ) = ( +g ` ( ringLMod ` R ) ) |
4 |
2 3
|
eqtri |
|- .+ = ( +g ` ( ringLMod ` R ) ) |
5 |
4
|
oveqi |
|- ( X .+ Y ) = ( X ( +g ` ( ringLMod ` R ) ) Y ) |
6 |
|
rlmlmod |
|- ( R e. Ring -> ( ringLMod ` R ) e. LMod ) |
7 |
6
|
adantr |
|- ( ( R e. Ring /\ I e. U ) -> ( ringLMod ` R ) e. LMod ) |
8 |
|
simpr |
|- ( ( R e. Ring /\ I e. U ) -> I e. U ) |
9 |
|
lidlval |
|- ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) ) |
10 |
1 9
|
eqtri |
|- U = ( LSubSp ` ( ringLMod ` R ) ) |
11 |
8 10
|
eleqtrdi |
|- ( ( R e. Ring /\ I e. U ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) ) |
12 |
7 11
|
jca |
|- ( ( R e. Ring /\ I e. U ) -> ( ( ringLMod ` R ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) ) ) |
13 |
|
eqid |
|- ( +g ` ( ringLMod ` R ) ) = ( +g ` ( ringLMod ` R ) ) |
14 |
|
eqid |
|- ( LSubSp ` ( ringLMod ` R ) ) = ( LSubSp ` ( ringLMod ` R ) ) |
15 |
13 14
|
lssvacl |
|- ( ( ( ( ringLMod ` R ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) ) /\ ( X e. I /\ Y e. I ) ) -> ( X ( +g ` ( ringLMod ` R ) ) Y ) e. I ) |
16 |
12 15
|
sylan |
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X ( +g ` ( ringLMod ` R ) ) Y ) e. I ) |
17 |
5 16
|
eqeltrid |
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X .+ Y ) e. I ) |