Metamath Proof Explorer

Theorem gsumvsca2

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

Ref Expression
Hypotheses gsumvsca.b 
|- B = ( Base ` W )
gsumvsca.g 
|- G = ( Scalar ` W )
gsumvsca.z 
|- .0. = ( 0g ` W )
gsumvsca.t 
|- .x. = ( .s ` W )
gsumvsca.p 
|- .+ = ( +g ` W )
gsumvsca.k 
|- ( ph -> K C_ ( Base ` G ) )
gsumvsca.a 
|- ( ph -> A e. Fin )
gsumvsca.w 
|- ( ph -> W e. SLMod )
gsumvsca2.n 
|- ( ph -> Q e. B )
gsumvsca2.c 
|- ( ( ph /\ k e. A ) -> P e. K )
Assertion gsumvsca2 
|- ( ph -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. A |-> P ) ) .x. Q ) )

Proof

Step Hyp Ref Expression
1 gsumvsca.b 
 |-  B = ( Base ` W )
2 gsumvsca.g 
 |-  G = ( Scalar ` W )
3 gsumvsca.z 
 |-  .0. = ( 0g ` W )
4 gsumvsca.t 
 |-  .x. = ( .s ` W )
5 gsumvsca.p 
 |-  .+ = ( +g ` W )
6 gsumvsca.k 
 |-  ( ph -> K C_ ( Base ` G ) )
7 gsumvsca.a 
 |-  ( ph -> A e. Fin )
8 gsumvsca.w 
 |-  ( ph -> W e. SLMod )
9 gsumvsca2.n 
 |-  ( ph -> Q e. B )
10 gsumvsca2.c 
 |-  ( ( ph /\ k e. A ) -> P e. K )
11 ssid 
 |-  A C_ A
12 sseq1 
 |-  ( a = (/) -> ( a C_ A <-> (/) C_ A ) )
13 12 anbi2d 
 |-  ( a = (/) -> ( ( ph /\ a C_ A ) <-> ( ph /\ (/) C_ A ) ) )
14 mpteq1 
 |-  ( a = (/) -> ( k e. a |-> ( P .x. Q ) ) = ( k e. (/) |-> ( P .x. Q ) ) )
15 14 oveq2d 
 |-  ( a = (/) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) )
16 mpteq1 
 |-  ( a = (/) -> ( k e. a |-> P ) = ( k e. (/) |-> P ) )
17 16 oveq2d 
 |-  ( a = (/) -> ( G gsum ( k e. a |-> P ) ) = ( G gsum ( k e. (/) |-> P ) ) )
18 17 oveq1d 
 |-  ( a = (/) -> ( ( G gsum ( k e. a |-> P ) ) .x. Q ) = ( ( G gsum ( k e. (/) |-> P ) ) .x. Q ) )
19 15 18 eqeq12d 
 |-  ( a = (/) -> ( ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. a |-> P ) ) .x. Q ) <-> ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. (/) |-> P ) ) .x. Q ) ) )
20 13 19 imbi12d 
 |-  ( a = (/) -> ( ( ( ph /\ a C_ A ) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. a |-> P ) ) .x. Q ) ) <-> ( ( ph /\ (/) C_ A ) -> ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. (/) |-> P ) ) .x. Q ) ) ) )
21 sseq1 
 |-  ( a = e -> ( a C_ A <-> e C_ A ) )
22 21 anbi2d 
 |-  ( a = e -> ( ( ph /\ a C_ A ) <-> ( ph /\ e C_ A ) ) )
23 mpteq1 
 |-  ( a = e -> ( k e. a |-> ( P .x. Q ) ) = ( k e. e |-> ( P .x. Q ) ) )
24 23 oveq2d 
 |-  ( a = e -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( W gsum ( k e. e |-> ( P .x. Q ) ) ) )
25 mpteq1 
 |-  ( a = e -> ( k e. a |-> P ) = ( k e. e |-> P ) )
26 25 oveq2d 
 |-  ( a = e -> ( G gsum ( k e. a |-> P ) ) = ( G gsum ( k e. e |-> P ) ) )
27 26 oveq1d 
 |-  ( a = e -> ( ( G gsum ( k e. a |-> P ) ) .x. Q ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) )
28 24 27 eqeq12d 
 |-  ( a = e -> ( ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. a |-> P ) ) .x. Q ) <-> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) )
29 22 28 imbi12d 
 |-  ( a = e -> ( ( ( ph /\ a C_ A ) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. a |-> P ) ) .x. Q ) ) <-> ( ( ph /\ e C_ A ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) ) )
30 sseq1 
 |-  ( a = ( e u. { z } ) -> ( a C_ A <-> ( e u. { z } ) C_ A ) )
31 30 anbi2d 
 |-  ( a = ( e u. { z } ) -> ( ( ph /\ a C_ A ) <-> ( ph /\ ( e u. { z } ) C_ A ) ) )
32 mpteq1 
 |-  ( a = ( e u. { z } ) -> ( k e. a |-> ( P .x. Q ) ) = ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) )
33 32 oveq2d 
 |-  ( a = ( e u. { z } ) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) )
34 mpteq1 
 |-  ( a = ( e u. { z } ) -> ( k e. a |-> P ) = ( k e. ( e u. { z } ) |-> P ) )
35 34 oveq2d 
 |-  ( a = ( e u. { z } ) -> ( G gsum ( k e. a |-> P ) ) = ( G gsum ( k e. ( e u. { z } ) |-> P ) ) )
36 35 oveq1d 
 |-  ( a = ( e u. { z } ) -> ( ( G gsum ( k e. a |-> P ) ) .x. Q ) = ( ( G gsum ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) )
37 33 36 eqeq12d 
 |-  ( a = ( e u. { z } ) -> ( ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. a |-> P ) ) .x. Q ) <-> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) )
38 31 37 imbi12d 
 |-  ( a = ( e u. { z } ) -> ( ( ( ph /\ a C_ A ) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. a |-> P ) ) .x. Q ) ) <-> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) ) )
39 sseq1 
 |-  ( a = A -> ( a C_ A <-> A C_ A ) )
40 39 anbi2d 
 |-  ( a = A -> ( ( ph /\ a C_ A ) <-> ( ph /\ A C_ A ) ) )
41 mpteq1 
 |-  ( a = A -> ( k e. a |-> ( P .x. Q ) ) = ( k e. A |-> ( P .x. Q ) ) )
42 41 oveq2d 
 |-  ( a = A -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( W gsum ( k e. A |-> ( P .x. Q ) ) ) )
43 mpteq1 
 |-  ( a = A -> ( k e. a |-> P ) = ( k e. A |-> P ) )
44 43 oveq2d 
 |-  ( a = A -> ( G gsum ( k e. a |-> P ) ) = ( G gsum ( k e. A |-> P ) ) )
45 44 oveq1d 
 |-  ( a = A -> ( ( G gsum ( k e. a |-> P ) ) .x. Q ) = ( ( G gsum ( k e. A |-> P ) ) .x. Q ) )
46 42 45 eqeq12d 
 |-  ( a = A -> ( ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. a |-> P ) ) .x. Q ) <-> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. A |-> P ) ) .x. Q ) ) )
47 40 46 imbi12d 
 |-  ( a = A -> ( ( ( ph /\ a C_ A ) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. a |-> P ) ) .x. Q ) ) <-> ( ( ph /\ A C_ A ) -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. A |-> P ) ) .x. Q ) ) ) )
48 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
49 1 2 4 48 3 slmd0vs 
 |-  ( ( W e. SLMod /\ Q e. B ) -> ( ( 0g ` G ) .x. Q ) = .0. )
50 8 9 49 syl2anc 
 |-  ( ph -> ( ( 0g ` G ) .x. Q ) = .0. )
51 50 eqcomd 
 |-  ( ph -> .0. = ( ( 0g ` G ) .x. Q ) )
52 mpt0 
 |-  ( k e. (/) |-> ( P .x. Q ) ) = (/)
53 52 oveq2i 
 |-  ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( W gsum (/) )
54 3 gsum0 
 |-  ( W gsum (/) ) = .0.
55 53 54 eqtri 
 |-  ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = .0.
56 mpt0 
 |-  ( k e. (/) |-> P ) = (/)
57 56 oveq2i 
 |-  ( G gsum ( k e. (/) |-> P ) ) = ( G gsum (/) )
58 48 gsum0 
 |-  ( G gsum (/) ) = ( 0g ` G )
59 57 58 eqtri 
 |-  ( G gsum ( k e. (/) |-> P ) ) = ( 0g ` G )
60 59 oveq1i 
 |-  ( ( G gsum ( k e. (/) |-> P ) ) .x. Q ) = ( ( 0g ` G ) .x. Q )
61 51 55 60 3eqtr4g 
 |-  ( ph -> ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. (/) |-> P ) ) .x. Q ) )
62 61 adantr 
 |-  ( ( ph /\ (/) C_ A ) -> ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. (/) |-> P ) ) .x. Q ) )
63 ssun1 
 |-  e C_ ( e u. { z } )
64 sstr2 
 |-  ( e C_ ( e u. { z } ) -> ( ( e u. { z } ) C_ A -> e C_ A ) )
65 63 64 ax-mp 
 |-  ( ( e u. { z } ) C_ A -> e C_ A )
66 65 anim2i 
 |-  ( ( ph /\ ( e u. { z } ) C_ A ) -> ( ph /\ e C_ A ) )
67 66 imim1i 
 |-  ( ( ( ph /\ e C_ A ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) )
68 8 ad2antrl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> W e. SLMod )
69 eqid 
 |-  ( Base ` G ) = ( Base ` G )
70 2 slmdsrg 
 |-  ( W e. SLMod -> G e. SRing )
71 srgcmn 
 |-  ( G e. SRing -> G e. CMnd )
72 68 70 71 3syl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> G e. CMnd )
73 vex 
 |-  e e. _V
74 73 a1i 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> e e. _V )
75 simplrl 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> ph )
76 simprr 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( e u. { z } ) C_ A )
77 76 unssad 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> e C_ A )
78 77 sselda 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> k e. A )
79 6 adantr 
 |-  ( ( ph /\ k e. A ) -> K C_ ( Base ` G ) )
80 79 10 sseldd 
 |-  ( ( ph /\ k e. A ) -> P e. ( Base ` G ) )
81 75 78 80 syl2anc 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> P e. ( Base ` G ) )
82 81 fmpttd 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( k e. e |-> P ) : e --> ( Base ` G ) )
83 eqid 
 |-  ( k e. e |-> P ) = ( k e. e |-> P )
84 simpll 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> e e. Fin )
85 75 78 10 syl2anc 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> P e. K )
86 fvexd 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( 0g ` G ) e. _V )
87 83 84 85 86 fsuppmptdm 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( k e. e |-> P ) finSupp ( 0g ` G ) )
88 69 48 72 74 82 87 gsumcl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( G gsum ( k e. e |-> P ) ) e. ( Base ` G ) )
89 76 unssbd 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> { z } C_ A )
90 vex 
 |-  z e. _V
91 90 snss 
 |-  ( z e. A <-> { z } C_ A )
92 89 91 sylibr 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> z e. A )
93 80 ralrimiva 
 |-  ( ph -> A. k e. A P e. ( Base ` G ) )
94 93 ad2antrl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> A. k e. A P e. ( Base ` G ) )
95 rspcsbela 
 |-  ( ( z e. A /\ A. k e. A P e. ( Base ` G ) ) -> [_ z / k ]_ P e. ( Base ` G ) )
96 92 94 95 syl2anc 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> [_ z / k ]_ P e. ( Base ` G ) )
97 9 ad2antrl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> Q e. B )
98 eqid 
 |-  ( +g ` G ) = ( +g ` G )
99 1 5 2 4 69 98 slmdvsdir 
 |-  ( ( W e. SLMod /\ ( ( G gsum ( k e. e |-> P ) ) e. ( Base ` G ) /\ [_ z / k ]_ P e. ( Base ` G ) /\ Q e. B ) ) -> ( ( ( G gsum ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) = ( ( ( G gsum ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
100 68 88 96 97 99 syl13anc 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( ( ( G gsum ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) = ( ( ( G gsum ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
101 100 adantr 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( ( ( G gsum ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) = ( ( ( G gsum ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
102 nfcsb1v 
 |-  F/_ k [_ z / k ]_ P
103 90 a1i 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> z e. _V )
104 simplr 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> -. z e. e )
105 csbeq1a 
 |-  ( k = z -> P = [_ z / k ]_ P )
106 102 69 98 72 84 81 103 104 96 105 gsumunsnf 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( G gsum ( k e. ( e u. { z } ) |-> P ) ) = ( ( G gsum ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) )
107 106 oveq1d 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( ( G gsum ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) = ( ( ( G gsum ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) )
108 107 adantr 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( ( G gsum ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) = ( ( ( G gsum ( k e. e |-> P ) ) ( +g ` G ) [_ z / k ]_ P ) .x. Q ) )
109 nfcv 
 |-  F/_ k .x.
110 nfcv 
 |-  F/_ k Q
111 102 109 110 nfov 
 |-  F/_ k ( [_ z / k ]_ P .x. Q )
112 slmdcmn 
 |-  ( W e. SLMod -> W e. CMnd )
113 68 112 syl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> W e. CMnd )
114 75 8 syl 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> W e. SLMod )
115 75 9 syl 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> Q e. B )
116 1 2 4 69 slmdvscl 
 |-  ( ( W e. SLMod /\ P e. ( Base ` G ) /\ Q e. B ) -> ( P .x. Q ) e. B )
117 114 81 115 116 syl3anc 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> ( P .x. Q ) e. B )
118 1 2 4 69 slmdvscl 
 |-  ( ( W e. SLMod /\ [_ z / k ]_ P e. ( Base ` G ) /\ Q e. B ) -> ( [_ z / k ]_ P .x. Q ) e. B )
119 68 96 97 118 syl3anc 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( [_ z / k ]_ P .x. Q ) e. B )
120 105 oveq1d 
 |-  ( k = z -> ( P .x. Q ) = ( [_ z / k ]_ P .x. Q ) )
121 111 1 5 113 84 117 103 104 119 120 gsumunsnf 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( W gsum ( k e. e |-> ( P .x. Q ) ) ) .+ ( [_ z / k ]_ P .x. Q ) ) )
122 121 adantr 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( W gsum ( k e. e |-> ( P .x. Q ) ) ) .+ ( [_ z / k ]_ P .x. Q ) ) )
123 simpr 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) )
124 123 oveq1d 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( ( W gsum ( k e. e |-> ( P .x. Q ) ) ) .+ ( [_ z / k ]_ P .x. Q ) ) = ( ( ( G gsum ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
125 122 124 eqtrd 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( ( G gsum ( k e. e |-> P ) ) .x. Q ) .+ ( [_ z / k ]_ P .x. Q ) ) )
126 101 108 125 3eqtr4rd 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) )
127 126 exp31 
 |-  ( ( e e. Fin /\ -. z e. e ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) ) )
128 127 a2d 
 |-  ( ( e e. Fin /\ -. z e. e ) -> ( ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) ) )
129 67 128 syl5 
 |-  ( ( e e. Fin /\ -. z e. e ) -> ( ( ( ph /\ e C_ A ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. e |-> P ) ) .x. Q ) ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. ( e u. { z } ) |-> P ) ) .x. Q ) ) ) )
130 20 29 38 47 62 129 findcard2s 
 |-  ( A e. Fin -> ( ( ph /\ A C_ A ) -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. A |-> P ) ) .x. Q ) ) )
131 130 imp 
 |-  ( ( A e. Fin /\ ( ph /\ A C_ A ) ) -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. A |-> P ) ) .x. Q ) )
132 11 131 mpanr2 
 |-  ( ( A e. Fin /\ ph ) -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. A |-> P ) ) .x. Q ) )
133 7 132 mpancom 
 |-  ( ph -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( ( G gsum ( k e. A |-> P ) ) .x. Q ) )