Metamath Proof Explorer


Theorem gsumvsca1

Description: Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018)

Ref Expression
Hypotheses gsumvsca.b B=BaseW
gsumvsca.g G=ScalarW
gsumvsca.z 0˙=0W
gsumvsca.t ·˙=W
gsumvsca.p +˙=+W
gsumvsca.k φKBaseG
gsumvsca.a φAFin
gsumvsca.w φWSLMod
gsumvsca1.n φPK
gsumvsca1.c φkAQB
Assertion gsumvsca1 φWkAP·˙Q=P·˙WkAQ

Proof

Step Hyp Ref Expression
1 gsumvsca.b B=BaseW
2 gsumvsca.g G=ScalarW
3 gsumvsca.z 0˙=0W
4 gsumvsca.t ·˙=W
5 gsumvsca.p +˙=+W
6 gsumvsca.k φKBaseG
7 gsumvsca.a φAFin
8 gsumvsca.w φWSLMod
9 gsumvsca1.n φPK
10 gsumvsca1.c φkAQB
11 ssid AA
12 sseq1 a=aAA
13 12 anbi2d a=φaAφA
14 mpteq1 a=kaP·˙Q=kP·˙Q
15 14 oveq2d a=WkaP·˙Q=WkP·˙Q
16 mpteq1 a=kaQ=kQ
17 16 oveq2d a=WkaQ=WkQ
18 17 oveq2d a=P·˙WkaQ=P·˙WkQ
19 15 18 eqeq12d a=WkaP·˙Q=P·˙WkaQWkP·˙Q=P·˙WkQ
20 13 19 imbi12d a=φaAWkaP·˙Q=P·˙WkaQφAWkP·˙Q=P·˙WkQ
21 sseq1 a=eaAeA
22 21 anbi2d a=eφaAφeA
23 mpteq1 a=ekaP·˙Q=keP·˙Q
24 23 oveq2d a=eWkaP·˙Q=WkeP·˙Q
25 mpteq1 a=ekaQ=keQ
26 25 oveq2d a=eWkaQ=WkeQ
27 26 oveq2d a=eP·˙WkaQ=P·˙WkeQ
28 24 27 eqeq12d a=eWkaP·˙Q=P·˙WkaQWkeP·˙Q=P·˙WkeQ
29 22 28 imbi12d a=eφaAWkaP·˙Q=P·˙WkaQφeAWkeP·˙Q=P·˙WkeQ
30 sseq1 a=ezaAezA
31 30 anbi2d a=ezφaAφezA
32 mpteq1 a=ezkaP·˙Q=kezP·˙Q
33 32 oveq2d a=ezWkaP·˙Q=WkezP·˙Q
34 mpteq1 a=ezkaQ=kezQ
35 34 oveq2d a=ezWkaQ=WkezQ
36 35 oveq2d a=ezP·˙WkaQ=P·˙WkezQ
37 33 36 eqeq12d a=ezWkaP·˙Q=P·˙WkaQWkezP·˙Q=P·˙WkezQ
38 31 37 imbi12d a=ezφaAWkaP·˙Q=P·˙WkaQφezAWkezP·˙Q=P·˙WkezQ
39 sseq1 a=AaAAA
40 39 anbi2d a=AφaAφAA
41 mpteq1 a=AkaP·˙Q=kAP·˙Q
42 41 oveq2d a=AWkaP·˙Q=WkAP·˙Q
43 mpteq1 a=AkaQ=kAQ
44 43 oveq2d a=AWkaQ=WkAQ
45 44 oveq2d a=AP·˙WkaQ=P·˙WkAQ
46 42 45 eqeq12d a=AWkaP·˙Q=P·˙WkaQWkAP·˙Q=P·˙WkAQ
47 40 46 imbi12d a=AφaAWkaP·˙Q=P·˙WkaQφAAWkAP·˙Q=P·˙WkAQ
48 6 9 sseldd φPBaseG
49 eqid BaseG=BaseG
50 2 4 49 3 slmdvs0 WSLModPBaseGP·˙0˙=0˙
51 8 48 50 syl2anc φP·˙0˙=0˙
52 51 eqcomd φ0˙=P·˙0˙
53 mpt0 kP·˙Q=
54 53 oveq2i WkP·˙Q=W
55 3 gsum0 W=0˙
56 54 55 eqtri WkP·˙Q=0˙
57 mpt0 kQ=
58 57 oveq2i WkQ=W
59 58 55 eqtri WkQ=0˙
60 59 oveq2i P·˙WkQ=P·˙0˙
61 52 56 60 3eqtr4g φWkP·˙Q=P·˙WkQ
62 61 adantr φAWkP·˙Q=P·˙WkQ
63 ssun1 eez
64 sstr2 eezezAeA
65 63 64 ax-mp ezAeA
66 65 anim2i φezAφeA
67 66 imim1i φeAWkeP·˙Q=P·˙WkeQφezAWkeP·˙Q=P·˙WkeQ
68 8 ad2antrl eFin¬zeφezAWSLMod
69 48 ad2antrl eFin¬zeφezAPBaseG
70 slmdcmn WSLModWCMnd
71 68 70 syl eFin¬zeφezAWCMnd
72 vex eV
73 72 a1i eFin¬zeφezAeV
74 simplrl eFin¬zeφezAkeφ
75 simprr eFin¬zeφezAezA
76 75 unssad eFin¬zeφezAeA
77 76 sselda eFin¬zeφezAkekA
78 74 77 10 syl2anc eFin¬zeφezAkeQB
79 78 fmpttd eFin¬zeφezAkeQ:eB
80 eqid keQ=keQ
81 simpll eFin¬zeφezAeFin
82 3 fvexi 0˙V
83 82 a1i eFin¬zeφezA0˙V
84 80 81 78 83 fsuppmptdm eFin¬zeφezAfinSupp0˙keQ
85 1 3 71 73 79 84 gsumcl eFin¬zeφezAWkeQB
86 75 unssbd eFin¬zeφezAzA
87 vex zV
88 87 snss zAzA
89 86 88 sylibr eFin¬zeφezAzA
90 10 ralrimiva φkAQB
91 90 ad2antrl eFin¬zeφezAkAQB
92 rspcsbela zAkAQBz/kQB
93 89 91 92 syl2anc eFin¬zeφezAz/kQB
94 1 5 2 4 49 slmdvsdi WSLModPBaseGWkeQBz/kQBP·˙WkeQ+˙z/kQ=P·˙WkeQ+˙P·˙z/kQ
95 68 69 85 93 94 syl13anc eFin¬zeφezAP·˙WkeQ+˙z/kQ=P·˙WkeQ+˙P·˙z/kQ
96 95 adantr eFin¬zeφezAWkeP·˙Q=P·˙WkeQP·˙WkeQ+˙z/kQ=P·˙WkeQ+˙P·˙z/kQ
97 nfcsb1v _kz/kQ
98 87 a1i eFin¬zeφezAzV
99 simplr eFin¬zeφezA¬ze
100 csbeq1a k=zQ=z/kQ
101 97 1 5 71 81 78 98 99 93 100 gsumunsnf eFin¬zeφezAWkezQ=WkeQ+˙z/kQ
102 101 oveq2d eFin¬zeφezAP·˙WkezQ=P·˙WkeQ+˙z/kQ
103 102 adantr eFin¬zeφezAWkeP·˙Q=P·˙WkeQP·˙WkezQ=P·˙WkeQ+˙z/kQ
104 nfcv _kP
105 nfcv _k·˙
106 104 105 97 nfov _kP·˙z/kQ
107 74 8 syl eFin¬zeφezAkeWSLMod
108 74 48 syl eFin¬zeφezAkePBaseG
109 1 2 4 49 slmdvscl WSLModPBaseGQBP·˙QB
110 107 108 78 109 syl3anc eFin¬zeφezAkeP·˙QB
111 1 2 4 49 slmdvscl WSLModPBaseGz/kQBP·˙z/kQB
112 68 69 93 111 syl3anc eFin¬zeφezAP·˙z/kQB
113 100 oveq2d k=zP·˙Q=P·˙z/kQ
114 106 1 5 71 81 110 98 99 112 113 gsumunsnf eFin¬zeφezAWkezP·˙Q=WkeP·˙Q+˙P·˙z/kQ
115 114 adantr eFin¬zeφezAWkeP·˙Q=P·˙WkeQWkezP·˙Q=WkeP·˙Q+˙P·˙z/kQ
116 simpr eFin¬zeφezAWkeP·˙Q=P·˙WkeQWkeP·˙Q=P·˙WkeQ
117 116 oveq1d eFin¬zeφezAWkeP·˙Q=P·˙WkeQWkeP·˙Q+˙P·˙z/kQ=P·˙WkeQ+˙P·˙z/kQ
118 115 117 eqtrd eFin¬zeφezAWkeP·˙Q=P·˙WkeQWkezP·˙Q=P·˙WkeQ+˙P·˙z/kQ
119 96 103 118 3eqtr4rd eFin¬zeφezAWkeP·˙Q=P·˙WkeQWkezP·˙Q=P·˙WkezQ
120 119 exp31 eFin¬zeφezAWkeP·˙Q=P·˙WkeQWkezP·˙Q=P·˙WkezQ
121 120 a2d eFin¬zeφezAWkeP·˙Q=P·˙WkeQφezAWkezP·˙Q=P·˙WkezQ
122 67 121 syl5 eFin¬zeφeAWkeP·˙Q=P·˙WkeQφezAWkezP·˙Q=P·˙WkezQ
123 20 29 38 47 62 122 findcard2s AFinφAAWkAP·˙Q=P·˙WkAQ
124 123 imp AFinφAAWkAP·˙Q=P·˙WkAQ
125 11 124 mpanr2 AFinφWkAP·˙Q=P·˙WkAQ
126 7 125 mpancom φWkAP·˙Q=P·˙WkAQ