Metamath Proof Explorer

Theorem gsumzf1o

Description: Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 2-Jun-2019)

Ref Expression
Hypotheses gsumzcl.b 
|- B = ( Base ` G )
gsumzcl.0 
|- .0. = ( 0g ` G )
gsumzcl.z 
|- Z = ( Cntz ` G )
gsumzcl.g 
|- ( ph -> G e. Mnd )
gsumzcl.a 
|- ( ph -> A e. V )
gsumzcl.f 
|- ( ph -> F : A --> B )
gsumzcl.c 
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzcl.w 
|- ( ph -> F finSupp .0. )
gsumzf1o.h 
|- ( ph -> H : C -1-1-onto-> A )
Assertion gsumzf1o 
|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )

Proof

Step Hyp Ref Expression
1 gsumzcl.b 
 |-  B = ( Base ` G )
2 gsumzcl.0 
 |-  .0. = ( 0g ` G )
3 gsumzcl.z 
 |-  Z = ( Cntz ` G )
4 gsumzcl.g 
 |-  ( ph -> G e. Mnd )
5 gsumzcl.a 
 |-  ( ph -> A e. V )
6 gsumzcl.f 
 |-  ( ph -> F : A --> B )
7 gsumzcl.c 
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
8 gsumzcl.w 
 |-  ( ph -> F finSupp .0. )
9 gsumzf1o.h 
 |-  ( ph -> H : C -1-1-onto-> A )
10 2 gsumz 
 |-  ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
11 4 5 10 syl2anc 
 |-  ( ph -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
12 f1of1 
 |-  ( H : C -1-1-onto-> A -> H : C -1-1-> A )
13 9 12 syl 
 |-  ( ph -> H : C -1-1-> A )
14 f1dmex 
 |-  ( ( H : C -1-1-> A /\ A e. V ) -> C e. _V )
15 13 5 14 syl2anc 
 |-  ( ph -> C e. _V )
16 2 gsumz 
 |-  ( ( G e. Mnd /\ C e. _V ) -> ( G gsum ( x e. C |-> .0. ) ) = .0. )
17 4 15 16 syl2anc 
 |-  ( ph -> ( G gsum ( x e. C |-> .0. ) ) = .0. )
18 11 17 eqtr4d 
 |-  ( ph -> ( G gsum ( k e. A |-> .0. ) ) = ( G gsum ( x e. C |-> .0. ) ) )
19 18 adantr 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( k e. A |-> .0. ) ) = ( G gsum ( x e. C |-> .0. ) ) )
20 2 fvexi 
 |-  .0. e. _V
21 20 a1i 
 |-  ( ph -> .0. e. _V )
22 ssidd 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
23 6 5 21 22 gsumcllem 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> F = ( k e. A |-> .0. ) )
24 23 oveq2d 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) = ( G gsum ( k e. A |-> .0. ) ) )
25 f1of 
 |-  ( H : C -1-1-onto-> A -> H : C --> A )
26 9 25 syl 
 |-  ( ph -> H : C --> A )
27 26 adantr 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> H : C --> A )
28 27 ffvelcdmda 
 |-  ( ( ( ph /\ ( F supp .0. ) = (/) ) /\ x e. C ) -> ( H ` x ) e. A )
29 27 feqmptd 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> H = ( x e. C |-> ( H ` x ) ) )
30 eqidd 
 |-  ( k = ( H ` x ) -> .0. = .0. )
31 28 29 23 30 fmptco 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( F o. H ) = ( x e. C |-> .0. ) )
32 31 oveq2d 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( F o. H ) ) = ( G gsum ( x e. C |-> .0. ) ) )
33 19 24 32 3eqtr4d 
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) )
34 33 ex 
 |-  ( ph -> ( ( F supp .0. ) = (/) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) )
35 9 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> H : C -1-1-onto-> A )
36 f1ococnv2 
 |-  ( H : C -1-1-onto-> A -> ( H o. `' H ) = ( _I |` A ) )
37 35 36 syl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( H o. `' H ) = ( _I |` A ) )
38 37 coeq1d 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( H o. `' H ) o. f ) = ( ( _I |` A ) o. f ) )
39 f1of1 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) )
40 39 ad2antll 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) )
41 suppssdm 
 |-  ( F supp .0. ) C_ dom F
42 41 6 fssdm 
 |-  ( ph -> ( F supp .0. ) C_ A )
43 42 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ A )
44 f1ss 
 |-  ( ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) /\ ( F supp .0. ) C_ A ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A )
45 40 43 44 syl2anc 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A )
46 f1f 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A )
47 fcoi2 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A -> ( ( _I |` A ) o. f ) = f )
48 45 46 47 3syl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( _I |` A ) o. f ) = f )
49 38 48 eqtrd 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( H o. `' H ) o. f ) = f )
50 coass 
 |-  ( ( H o. `' H ) o. f ) = ( H o. ( `' H o. f ) )
51 49 50 eqtr3di 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f = ( H o. ( `' H o. f ) ) )
52 51 coeq2d 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. f ) = ( F o. ( H o. ( `' H o. f ) ) ) )
53 coass 
 |-  ( ( F o. H ) o. ( `' H o. f ) ) = ( F o. ( H o. ( `' H o. f ) ) )
54 52 53 eqtr4di 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. f ) = ( ( F o. H ) o. ( `' H o. f ) ) )
55 54 seqeq3d 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> seq 1 ( ( +g ` G ) , ( F o. f ) ) = seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) )
56 55 fveq1d 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( F supp .0. ) ) ) = ( seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) )
57 eqid 
 |-  ( +g ` G ) = ( +g ` G )
58 4 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> G e. Mnd )
59 5 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> A e. V )
60 6 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> F : A --> B )
61 7 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran F C_ ( Z ` ran F ) )
62 simprl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( # ` ( F supp .0. ) ) e. NN )
63 ssid 
 |-  ( F supp .0. ) C_ ( F supp .0. )
64 f1ofo 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) )
65 forn 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) )
66 64 65 syl 
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) )
67 66 ad2antll 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran f = ( F supp .0. ) )
68 63 67 sseqtrrid 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ ran f )
69 eqid 
 |-  ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
70 1 2 57 3 58 59 60 61 62 45 68 69 gsumval3 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum F ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( F supp .0. ) ) ) )
71 15 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> C e. _V )
72 fco 
 |-  ( ( F : A --> B /\ H : C --> A ) -> ( F o. H ) : C --> B )
73 6 26 72 syl2anc 
 |-  ( ph -> ( F o. H ) : C --> B )
74 73 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. H ) : C --> B )
75 rncoss 
 |-  ran ( F o. H ) C_ ran F
76 3 cntzidss 
 |-  ( ( ran F C_ ( Z ` ran F ) /\ ran ( F o. H ) C_ ran F ) -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) )
77 7 75 76 sylancl 
 |-  ( ph -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) )
78 77 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) )
79 f1ocnv 
 |-  ( H : C -1-1-onto-> A -> `' H : A -1-1-onto-> C )
80 f1of1 
 |-  ( `' H : A -1-1-onto-> C -> `' H : A -1-1-> C )
81 9 79 80 3syl 
 |-  ( ph -> `' H : A -1-1-> C )
82 81 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> `' H : A -1-1-> C )
83 f1co 
 |-  ( ( `' H : A -1-1-> C /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A ) -> ( `' H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> C )
84 82 45 83 syl2anc 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> C )
85 ssidd 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ ( F supp .0. ) )
86 6 5 fexd 
 |-  ( ph -> F e. _V )
87 suppimacnv 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
88 86 20 87 sylancl 
 |-  ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
89 88 eqcomd 
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) = ( F supp .0. ) )
90 89 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' F " ( _V \ { .0. } ) ) = ( F supp .0. ) )
91 85 90 67 3sstr4d 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ ran f )
92 imass2 
 |-  ( ( `' F " ( _V \ { .0. } ) ) C_ ran f -> ( `' H " ( `' F " ( _V \ { .0. } ) ) ) C_ ( `' H " ran f ) )
93 91 92 syl 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' H " ( `' F " ( _V \ { .0. } ) ) ) C_ ( `' H " ran f ) )
94 cnvco 
 |-  `' ( F o. H ) = ( `' H o. `' F )
95 94 imaeq1i 
 |-  ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( ( `' H o. `' F ) " ( _V \ { .0. } ) )
96 imaco 
 |-  ( ( `' H o. `' F ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) )
97 95 96 eqtri 
 |-  ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) )
98 rnco2 
 |-  ran ( `' H o. f ) = ( `' H " ran f )
99 93 97 98 3sstr4g 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) )
100 f1oexrnex 
 |-  ( ( H : C -1-1-onto-> A /\ A e. V ) -> H e. _V )
101 9 5 100 syl2anc 
 |-  ( ph -> H e. _V )
102 coexg 
 |-  ( ( F e. _V /\ H e. _V ) -> ( F o. H ) e. _V )
103 86 101 102 syl2anc 
 |-  ( ph -> ( F o. H ) e. _V )
104 suppimacnv 
 |-  ( ( ( F o. H ) e. _V /\ .0. e. _V ) -> ( ( F o. H ) supp .0. ) = ( `' ( F o. H ) " ( _V \ { .0. } ) ) )
105 103 20 104 sylancl 
 |-  ( ph -> ( ( F o. H ) supp .0. ) = ( `' ( F o. H ) " ( _V \ { .0. } ) ) )
106 105 sseq1d 
 |-  ( ph -> ( ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) <-> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) ) )
107 106 adantr 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) <-> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) ) )
108 99 107 mpbird 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) )
109 eqid 
 |-  ( ( ( F o. H ) o. ( `' H o. f ) ) supp .0. ) = ( ( ( F o. H ) o. ( `' H o. f ) ) supp .0. )
110 1 2 57 3 58 71 74 78 62 84 108 109 gsumval3 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum ( F o. H ) ) = ( seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) )
111 56 70 110 3eqtr4d 
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) )
112 111 expr 
 |-  ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) )
113 112 exlimdv 
 |-  ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) )
114 113 expimpd 
 |-  ( ph -> ( ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) )
115 fsuppimp 
 |-  ( F finSupp .0. -> ( Fun F /\ ( F supp .0. ) e. Fin ) )
116 115 simprd 
 |-  ( F finSupp .0. -> ( F supp .0. ) e. Fin )
117 fz1f1o 
 |-  ( ( F supp .0. ) e. Fin -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) )
118 8 116 117 3syl 
 |-  ( ph -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) )
119 34 114 118 mpjaod 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )