Metamath Proof Explorer

Theorem frlmsubgval

Description: Subtraction in a free module. (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypotheses frlmsubval.y 
|- Y = ( R freeLMod I )
frlmsubval.b 
|- B = ( Base ` Y )
frlmsubval.r 
|- ( ph -> R e. Ring )
frlmsubval.i 
|- ( ph -> I e. W )
frlmsubval.f 
|- ( ph -> F e. B )
frlmsubval.g 
|- ( ph -> G e. B )
frlmsubval.a 
|- .- = ( -g ` R )
frlmsubval.p 
|- M = ( -g ` Y )
Assertion frlmsubgval 
|- ( ph -> ( F M G ) = ( F oF .- G ) )

Proof

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 ) )