Step |
Hyp |
Ref |
Expression |
1 |
|
lidlcl.u |
|- U = ( LIdeal ` R ) |
2 |
|
lidlnegcl.n |
|- N = ( invg ` R ) |
3 |
|
rlmvneg |
|- ( invg ` R ) = ( invg ` ( ringLMod ` R ) ) |
4 |
2 3
|
eqtri |
|- N = ( invg ` ( ringLMod ` R ) ) |
5 |
4
|
fveq1i |
|- ( N ` X ) = ( ( invg ` ( ringLMod ` R ) ) ` X ) |
6 |
|
rlmlmod |
|- ( R e. Ring -> ( ringLMod ` R ) e. LMod ) |
7 |
6
|
3ad2ant1 |
|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> ( 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 |
11
|
3adant3 |
|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) ) |
13 |
|
simp3 |
|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> X e. I ) |
14 |
|
eqid |
|- ( LSubSp ` ( ringLMod ` R ) ) = ( LSubSp ` ( ringLMod ` R ) ) |
15 |
|
eqid |
|- ( invg ` ( ringLMod ` R ) ) = ( invg ` ( ringLMod ` R ) ) |
16 |
14 15
|
lssvnegcl |
|- ( ( ( ringLMod ` R ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) /\ X e. I ) -> ( ( invg ` ( ringLMod ` R ) ) ` X ) e. I ) |
17 |
7 12 13 16
|
syl3anc |
|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> ( ( invg ` ( ringLMod ` R ) ) ` X ) e. I ) |
18 |
5 17
|
eqeltrid |
|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> ( N ` X ) e. I ) |