Step |
Hyp |
Ref |
Expression |
1 |
|
lidlcl.u |
|- U = ( LIdeal ` R ) |
2 |
|
lidlcl.b |
|- B = ( Base ` R ) |
3 |
|
lidlmcl.t |
|- .x. = ( .r ` R ) |
4 |
|
rlmvsca |
|- ( .r ` R ) = ( .s ` ( ringLMod ` R ) ) |
5 |
3 4
|
eqtri |
|- .x. = ( .s ` ( ringLMod ` R ) ) |
6 |
5
|
oveqi |
|- ( X .x. Y ) = ( X ( .s ` ( ringLMod ` R ) ) Y ) |
7 |
|
rlmlmod |
|- ( R e. Ring -> ( ringLMod ` R ) e. LMod ) |
8 |
7
|
ad2antrr |
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( ringLMod ` R ) e. LMod ) |
9 |
|
simpr |
|- ( ( R e. Ring /\ I e. U ) -> I e. U ) |
10 |
|
lidlval |
|- ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) ) |
11 |
1 10
|
eqtri |
|- U = ( LSubSp ` ( ringLMod ` R ) ) |
12 |
9 11
|
eleqtrdi |
|- ( ( R e. Ring /\ I e. U ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) ) |
13 |
12
|
adantr |
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) ) |
14 |
|
rlmsca |
|- ( R e. Ring -> R = ( Scalar ` ( ringLMod ` R ) ) ) |
15 |
14
|
fveq2d |
|- ( R e. Ring -> ( Base ` R ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ) |
16 |
2 15
|
eqtrid |
|- ( R e. Ring -> B = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ) |
17 |
16
|
eleq2d |
|- ( R e. Ring -> ( X e. B <-> X e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ) ) |
18 |
17
|
biimpa |
|- ( ( R e. Ring /\ X e. B ) -> X e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ) |
19 |
18
|
ad2ant2r |
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> X e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ) |
20 |
|
simprr |
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> Y e. I ) |
21 |
|
eqid |
|- ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) ) |
22 |
|
eqid |
|- ( .s ` ( ringLMod ` R ) ) = ( .s ` ( ringLMod ` R ) ) |
23 |
|
eqid |
|- ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) |
24 |
|
eqid |
|- ( LSubSp ` ( ringLMod ` R ) ) = ( LSubSp ` ( ringLMod ` R ) ) |
25 |
21 22 23 24
|
lssvscl |
|- ( ( ( ( ringLMod ` R ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) ) /\ ( X e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) /\ Y e. I ) ) -> ( X ( .s ` ( ringLMod ` R ) ) Y ) e. I ) |
26 |
8 13 19 20 25
|
syl22anc |
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( X ( .s ` ( ringLMod ` R ) ) Y ) e. I ) |
27 |
6 26
|
eqeltrid |
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I ) |