| Step |
Hyp |
Ref |
Expression |
| 1 |
|
frlmsubval.y |
|- Y = ( R freeLMod I ) |
| 2 |
|
frlmsubval.b |
|- B = ( Base ` Y ) |
| 3 |
|
frlmsubval.r |
|- ( ph -> R e. Ring ) |
| 4 |
|
frlmsubval.i |
|- ( ph -> I e. W ) |
| 5 |
|
frlmsubval.f |
|- ( ph -> F e. B ) |
| 6 |
|
frlmsubval.g |
|- ( ph -> G e. B ) |
| 7 |
|
frlmsubval.a |
|- .- = ( -g ` R ) |
| 8 |
|
frlmsubval.p |
|- M = ( -g ` Y ) |
| 9 |
1 2
|
frlmpws |
|- ( ( R e. Ring /\ I e. W ) -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) |
| 10 |
3 4 9
|
syl2anc |
|- ( ph -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) |
| 11 |
10
|
fveq2d |
|- ( ph -> ( -g ` Y ) = ( -g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) ) |
| 12 |
8 11
|
eqtrid |
|- ( ph -> M = ( -g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) ) |
| 13 |
12
|
oveqd |
|- ( ph -> ( F M G ) = ( F ( -g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) G ) ) |
| 14 |
|
rlmlmod |
|- ( R e. Ring -> ( ringLMod ` R ) e. LMod ) |
| 15 |
3 14
|
syl |
|- ( ph -> ( ringLMod ` R ) e. LMod ) |
| 16 |
|
eqid |
|- ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I ) |
| 17 |
16
|
pwslmod |
|- ( ( ( ringLMod ` R ) e. LMod /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) e. LMod ) |
| 18 |
15 4 17
|
syl2anc |
|- ( ph -> ( ( ringLMod ` R ) ^s I ) e. LMod ) |
| 19 |
|
eqid |
|- ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) = ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) |
| 20 |
1 2 19
|
frlmlss |
|- ( ( R e. Ring /\ I e. W ) -> B e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) ) |
| 21 |
3 4 20
|
syl2anc |
|- ( ph -> B e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) ) |
| 22 |
19
|
lsssubg |
|- ( ( ( ( ringLMod ` R ) ^s I ) e. LMod /\ B e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) ) -> B e. ( SubGrp ` ( ( ringLMod ` R ) ^s I ) ) ) |
| 23 |
18 21 22
|
syl2anc |
|- ( ph -> B e. ( SubGrp ` ( ( ringLMod ` R ) ^s I ) ) ) |
| 24 |
|
eqid |
|- ( -g ` ( ( ringLMod ` R ) ^s I ) ) = ( -g ` ( ( ringLMod ` R ) ^s I ) ) |
| 25 |
|
eqid |
|- ( ( ( ringLMod ` R ) ^s I ) |`s B ) = ( ( ( ringLMod ` R ) ^s I ) |`s B ) |
| 26 |
|
eqid |
|- ( -g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) = ( -g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) |
| 27 |
24 25 26
|
subgsub |
|- ( ( B e. ( SubGrp ` ( ( ringLMod ` R ) ^s I ) ) /\ F e. B /\ G e. B ) -> ( F ( -g ` ( ( ringLMod ` R ) ^s I ) ) G ) = ( F ( -g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) G ) ) |
| 28 |
23 5 6 27
|
syl3anc |
|- ( ph -> ( F ( -g ` ( ( ringLMod ` R ) ^s I ) ) G ) = ( F ( -g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) G ) ) |
| 29 |
|
lmodgrp |
|- ( ( ringLMod ` R ) e. LMod -> ( ringLMod ` R ) e. Grp ) |
| 30 |
3 14 29
|
3syl |
|- ( ph -> ( ringLMod ` R ) e. Grp ) |
| 31 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
| 32 |
1 31 2
|
frlmbasmap |
|- ( ( I e. W /\ F e. B ) -> F e. ( ( Base ` R ) ^m I ) ) |
| 33 |
4 5 32
|
syl2anc |
|- ( ph -> F e. ( ( Base ` R ) ^m I ) ) |
| 34 |
|
rlmbas |
|- ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) |
| 35 |
16 34
|
pwsbas |
|- ( ( ( ringLMod ` R ) e. Grp /\ I e. W ) -> ( ( Base ` R ) ^m I ) = ( Base ` ( ( ringLMod ` R ) ^s I ) ) ) |
| 36 |
30 4 35
|
syl2anc |
|- ( ph -> ( ( Base ` R ) ^m I ) = ( Base ` ( ( ringLMod ` R ) ^s I ) ) ) |
| 37 |
33 36
|
eleqtrd |
|- ( ph -> F e. ( Base ` ( ( ringLMod ` R ) ^s I ) ) ) |
| 38 |
1 31 2
|
frlmbasmap |
|- ( ( I e. W /\ G e. B ) -> G e. ( ( Base ` R ) ^m I ) ) |
| 39 |
4 6 38
|
syl2anc |
|- ( ph -> G e. ( ( Base ` R ) ^m I ) ) |
| 40 |
39 36
|
eleqtrd |
|- ( ph -> G e. ( Base ` ( ( ringLMod ` R ) ^s I ) ) ) |
| 41 |
|
eqid |
|- ( Base ` ( ( ringLMod ` R ) ^s I ) ) = ( Base ` ( ( ringLMod ` R ) ^s I ) ) |
| 42 |
|
rlmsub |
|- ( -g ` R ) = ( -g ` ( ringLMod ` R ) ) |
| 43 |
7 42
|
eqtri |
|- .- = ( -g ` ( ringLMod ` R ) ) |
| 44 |
16 41 43 24
|
pwssub |
|- ( ( ( ( ringLMod ` R ) e. Grp /\ I e. W ) /\ ( F e. ( Base ` ( ( ringLMod ` R ) ^s I ) ) /\ G e. ( Base ` ( ( ringLMod ` R ) ^s I ) ) ) ) -> ( F ( -g ` ( ( ringLMod ` R ) ^s I ) ) G ) = ( F oF .- G ) ) |
| 45 |
30 4 37 40 44
|
syl22anc |
|- ( ph -> ( F ( -g ` ( ( ringLMod ` R ) ^s I ) ) G ) = ( F oF .- G ) ) |
| 46 |
13 28 45
|
3eqtr2d |
|- ( ph -> ( F M G ) = ( F oF .- G ) ) |