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 = ( 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 )
gsumvsca1.n 
|- ( ph -> P e. K )
gsumvsca1.c 
|- ( ( ph /\ k e. A ) -> Q e. B )
Assertion gsumvsca1 
|- ( ph -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. A |-> 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 gsumvsca1.n 
 |-  ( ph -> P e. K )
10 gsumvsca1.c 
 |-  ( ( ph /\ k e. A ) -> Q e. B )
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 |-> Q ) = ( k e. (/) |-> Q ) )
17 16 oveq2d 
 |-  ( a = (/) -> ( W gsum ( k e. a |-> Q ) ) = ( W gsum ( k e. (/) |-> Q ) ) )
18 17 oveq2d 
 |-  ( a = (/) -> ( P .x. ( W gsum ( k e. a |-> Q ) ) ) = ( P .x. ( W gsum ( k e. (/) |-> Q ) ) ) )
19 15 18 eqeq12d 
 |-  ( a = (/) -> ( ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. a |-> Q ) ) ) <-> ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. (/) |-> Q ) ) ) ) )
20 13 19 imbi12d 
 |-  ( a = (/) -> ( ( ( ph /\ a C_ A ) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. a |-> Q ) ) ) ) <-> ( ( ph /\ (/) C_ A ) -> ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. (/) |-> 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 |-> Q ) = ( k e. e |-> Q ) )
26 25 oveq2d 
 |-  ( a = e -> ( W gsum ( k e. a |-> Q ) ) = ( W gsum ( k e. e |-> Q ) ) )
27 26 oveq2d 
 |-  ( a = e -> ( P .x. ( W gsum ( k e. a |-> Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) )
28 24 27 eqeq12d 
 |-  ( a = e -> ( ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. a |-> Q ) ) ) <-> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) )
29 22 28 imbi12d 
 |-  ( a = e -> ( ( ( ph /\ a C_ A ) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. a |-> Q ) ) ) ) <-> ( ( ph /\ e C_ A ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> 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 |-> Q ) = ( k e. ( e u. { z } ) |-> Q ) )
35 34 oveq2d 
 |-  ( a = ( e u. { z } ) -> ( W gsum ( k e. a |-> Q ) ) = ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) )
36 35 oveq2d 
 |-  ( a = ( e u. { z } ) -> ( P .x. ( W gsum ( k e. a |-> Q ) ) ) = ( P .x. ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) ) )
37 33 36 eqeq12d 
 |-  ( a = ( e u. { z } ) -> ( ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. a |-> Q ) ) ) <-> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) ) ) )
38 31 37 imbi12d 
 |-  ( a = ( e u. { z } ) -> ( ( ( ph /\ a C_ A ) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. a |-> Q ) ) ) ) <-> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. ( e u. { z } ) |-> 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 |-> Q ) = ( k e. A |-> Q ) )
44 43 oveq2d 
 |-  ( a = A -> ( W gsum ( k e. a |-> Q ) ) = ( W gsum ( k e. A |-> Q ) ) )
45 44 oveq2d 
 |-  ( a = A -> ( P .x. ( W gsum ( k e. a |-> Q ) ) ) = ( P .x. ( W gsum ( k e. A |-> Q ) ) ) )
46 42 45 eqeq12d 
 |-  ( a = A -> ( ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. a |-> Q ) ) ) <-> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. A |-> Q ) ) ) ) )
47 40 46 imbi12d 
 |-  ( a = A -> ( ( ( ph /\ a C_ A ) -> ( W gsum ( k e. a |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. a |-> Q ) ) ) ) <-> ( ( ph /\ A C_ A ) -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. A |-> Q ) ) ) ) ) )
48 6 9 sseldd 
 |-  ( ph -> P e. ( Base ` G ) )
49 eqid 
 |-  ( Base ` G ) = ( Base ` G )
50 2 4 49 3 slmdvs0 
 |-  ( ( W e. SLMod /\ P e. ( Base ` G ) ) -> ( P .x. .0. ) = .0. )
51 8 48 50 syl2anc 
 |-  ( ph -> ( P .x. .0. ) = .0. )
52 51 eqcomd 
 |-  ( ph -> .0. = ( P .x. .0. ) )
53 mpt0 
 |-  ( k e. (/) |-> ( P .x. Q ) ) = (/)
54 53 oveq2i 
 |-  ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( W gsum (/) )
55 3 gsum0 
 |-  ( W gsum (/) ) = .0.
56 54 55 eqtri 
 |-  ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = .0.
57 mpt0 
 |-  ( k e. (/) |-> Q ) = (/)
58 57 oveq2i 
 |-  ( W gsum ( k e. (/) |-> Q ) ) = ( W gsum (/) )
59 58 55 eqtri 
 |-  ( W gsum ( k e. (/) |-> Q ) ) = .0.
60 59 oveq2i 
 |-  ( P .x. ( W gsum ( k e. (/) |-> Q ) ) ) = ( P .x. .0. )
61 52 56 60 3eqtr4g 
 |-  ( ph -> ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. (/) |-> Q ) ) ) )
62 61 adantr 
 |-  ( ( ph /\ (/) C_ A ) -> ( W gsum ( k e. (/) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. (/) |-> 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 ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) )
68 8 ad2antrl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> W e. SLMod )
69 48 ad2antrl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> P e. ( Base ` G ) )
70 slmdcmn 
 |-  ( W e. SLMod -> W e. CMnd )
71 68 70 syl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> W e. CMnd )
72 vex 
 |-  e e. _V
73 72 a1i 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> e e. _V )
74 simplrl 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> ph )
75 simprr 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( e u. { z } ) C_ A )
76 75 unssad 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> e C_ A )
77 76 sselda 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> k e. A )
78 74 77 10 syl2anc 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> Q e. B )
79 78 fmpttd 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( k e. e |-> Q ) : e --> B )
80 eqid 
 |-  ( k e. e |-> Q ) = ( k e. e |-> Q )
81 simpll 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> e e. Fin )
82 3 fvexi 
 |-  .0. e. _V
83 82 a1i 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> .0. e. _V )
84 80 81 78 83 fsuppmptdm 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( k e. e |-> Q ) finSupp .0. )
85 1 3 71 73 79 84 gsumcl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( W gsum ( k e. e |-> Q ) ) e. B )
86 75 unssbd 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> { z } C_ A )
87 vex 
 |-  z e. _V
88 87 snss 
 |-  ( z e. A <-> { z } C_ A )
89 86 88 sylibr 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> z e. A )
90 10 ralrimiva 
 |-  ( ph -> A. k e. A Q e. B )
91 90 ad2antrl 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> A. k e. A Q e. B )
92 rspcsbela 
 |-  ( ( z e. A /\ A. k e. A Q e. B ) -> [_ z / k ]_ Q e. B )
93 89 91 92 syl2anc 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> [_ z / k ]_ Q e. B )
94 1 5 2 4 49 slmdvsdi 
 |-  ( ( W e. SLMod /\ ( P e. ( Base ` G ) /\ ( W gsum ( k e. e |-> Q ) ) e. B /\ [_ z / k ]_ Q e. B ) ) -> ( P .x. ( ( W gsum ( k e. e |-> Q ) ) .+ [_ z / k ]_ Q ) ) = ( ( P .x. ( W gsum ( k e. e |-> Q ) ) ) .+ ( P .x. [_ z / k ]_ Q ) ) )
95 68 69 85 93 94 syl13anc 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( P .x. ( ( W gsum ( k e. e |-> Q ) ) .+ [_ z / k ]_ Q ) ) = ( ( P .x. ( W gsum ( k e. e |-> Q ) ) ) .+ ( P .x. [_ z / k ]_ Q ) ) )
96 95 adantr 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( P .x. ( ( W gsum ( k e. e |-> Q ) ) .+ [_ z / k ]_ Q ) ) = ( ( P .x. ( W gsum ( k e. e |-> Q ) ) ) .+ ( P .x. [_ z / k ]_ Q ) ) )
97 nfcsb1v 
 |-  F/_ k [_ z / k ]_ Q
98 87 a1i 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> z e. _V )
99 simplr 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> -. z e. e )
100 csbeq1a 
 |-  ( k = z -> Q = [_ z / k ]_ Q )
101 97 1 5 71 81 78 98 99 93 100 gsumunsnf 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) = ( ( W gsum ( k e. e |-> Q ) ) .+ [_ z / k ]_ Q ) )
102 101 oveq2d 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( P .x. ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) ) = ( P .x. ( ( W gsum ( k e. e |-> Q ) ) .+ [_ z / k ]_ Q ) ) )
103 102 adantr 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( P .x. ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) ) = ( P .x. ( ( W gsum ( k e. e |-> Q ) ) .+ [_ z / k ]_ Q ) ) )
104 nfcv 
 |-  F/_ k P
105 nfcv 
 |-  F/_ k .x.
106 104 105 97 nfov 
 |-  F/_ k ( P .x. [_ z / k ]_ Q )
107 74 8 syl 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> W e. SLMod )
108 74 48 syl 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> P e. ( Base ` G ) )
109 1 2 4 49 slmdvscl 
 |-  ( ( W e. SLMod /\ P e. ( Base ` G ) /\ Q e. B ) -> ( P .x. Q ) e. B )
110 107 108 78 109 syl3anc 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ k e. e ) -> ( P .x. Q ) e. B )
111 1 2 4 49 slmdvscl 
 |-  ( ( W e. SLMod /\ P e. ( Base ` G ) /\ [_ z / k ]_ Q e. B ) -> ( P .x. [_ z / k ]_ Q ) e. B )
112 68 69 93 111 syl3anc 
 |-  ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) -> ( P .x. [_ z / k ]_ Q ) e. B )
113 100 oveq2d 
 |-  ( k = z -> ( P .x. Q ) = ( P .x. [_ z / k ]_ Q ) )
114 106 1 5 71 81 110 98 99 112 113 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 ) ) ) .+ ( P .x. [_ z / k ]_ Q ) ) )
115 114 adantr 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( W gsum ( k e. e |-> ( P .x. Q ) ) ) .+ ( P .x. [_ z / k ]_ Q ) ) )
116 simpr 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) )
117 116 oveq1d 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( ( W gsum ( k e. e |-> ( P .x. Q ) ) ) .+ ( P .x. [_ z / k ]_ Q ) ) = ( ( P .x. ( W gsum ( k e. e |-> Q ) ) ) .+ ( P .x. [_ z / k ]_ Q ) ) )
118 115 117 eqtrd 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( ( P .x. ( W gsum ( k e. e |-> Q ) ) ) .+ ( P .x. [_ z / k ]_ Q ) ) )
119 96 103 118 3eqtr4rd 
 |-  ( ( ( ( e e. Fin /\ -. z e. e ) /\ ( ph /\ ( e u. { z } ) C_ A ) ) /\ ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) ) )
120 119 exp31 
 |-  ( ( e e. Fin /\ -. z e. e ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) ) ) ) )
121 120 a2d 
 |-  ( ( e e. Fin /\ -. z e. e ) -> ( ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) ) ) ) )
122 67 121 syl5 
 |-  ( ( e e. Fin /\ -. z e. e ) -> ( ( ( ph /\ e C_ A ) -> ( W gsum ( k e. e |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. e |-> Q ) ) ) ) -> ( ( ph /\ ( e u. { z } ) C_ A ) -> ( W gsum ( k e. ( e u. { z } ) |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. ( e u. { z } ) |-> Q ) ) ) ) ) )
123 20 29 38 47 62 122 findcard2s 
 |-  ( A e. Fin -> ( ( ph /\ A C_ A ) -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. A |-> Q ) ) ) ) )
124 123 imp 
 |-  ( ( A e. Fin /\ ( ph /\ A C_ A ) ) -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. A |-> Q ) ) ) )
125 11 124 mpanr2 
 |-  ( ( A e. Fin /\ ph ) -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. A |-> Q ) ) ) )
126 7 125 mpancom 
 |-  ( ph -> ( W gsum ( k e. A |-> ( P .x. Q ) ) ) = ( P .x. ( W gsum ( k e. A |-> Q ) ) ) )