Metamath Proof Explorer

Theorem gsumzaddlem

Description: The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

Ref Expression
Hypotheses gsumzadd.b 
|- B = ( Base ` G )
gsumzadd.0 
|- .0. = ( 0g ` G )
gsumzadd.p 
|- .+ = ( +g ` G )
gsumzadd.z 
|- Z = ( Cntz ` G )
gsumzadd.g 
|- ( ph -> G e. Mnd )
gsumzadd.a 
|- ( ph -> A e. V )
gsumzadd.fn 
|- ( ph -> F finSupp .0. )
gsumzadd.hn 
|- ( ph -> H finSupp .0. )
gsumzaddlem.w 
|- W = ( ( F u. H ) supp .0. )
gsumzaddlem.f 
|- ( ph -> F : A --> B )
gsumzaddlem.h 
|- ( ph -> H : A --> B )
gsumzaddlem.1 
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzaddlem.2 
|- ( ph -> ran H C_ ( Z ` ran H ) )
gsumzaddlem.3 
|- ( ph -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
gsumzaddlem.4 
|- ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) )
Assertion gsumzaddlem 
|- ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )

Proof

Step Hyp Ref Expression
1 gsumzadd.b 
 |-  B = ( Base ` G )
2 gsumzadd.0 
 |-  .0. = ( 0g ` G )
3 gsumzadd.p 
 |-  .+ = ( +g ` G )
4 gsumzadd.z 
 |-  Z = ( Cntz ` G )
5 gsumzadd.g 
 |-  ( ph -> G e. Mnd )
6 gsumzadd.a 
 |-  ( ph -> A e. V )
7 gsumzadd.fn 
 |-  ( ph -> F finSupp .0. )
8 gsumzadd.hn 
 |-  ( ph -> H finSupp .0. )
9 gsumzaddlem.w 
 |-  W = ( ( F u. H ) supp .0. )
10 gsumzaddlem.f 
 |-  ( ph -> F : A --> B )
11 gsumzaddlem.h 
 |-  ( ph -> H : A --> B )
12 gsumzaddlem.1 
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
13 gsumzaddlem.2 
 |-  ( ph -> ran H C_ ( Z ` ran H ) )
14 gsumzaddlem.3 
 |-  ( ph -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
15 gsumzaddlem.4 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) )
16 1 2 mndidcl 
 |-  ( G e. Mnd -> .0. e. B )
17 5 16 syl 
 |-  ( ph -> .0. e. B )
18 1 3 2 mndlid 
 |-  ( ( G e. Mnd /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
19 5 17 18 syl2anc 
 |-  ( ph -> ( .0. .+ .0. ) = .0. )
20 19 adantr 
 |-  ( ( ph /\ W = (/) ) -> ( .0. .+ .0. ) = .0. )
21 2 fvexi 
 |-  .0. e. _V
22 21 a1i 
 |-  ( ph -> .0. e. _V )
23 fex 
 |-  ( ( H : A --> B /\ A e. V ) -> H e. _V )
24 11 6 23 syl2anc 
 |-  ( ph -> H e. _V )
25 24 suppun 
 |-  ( ph -> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) )
26 25 9 sseqtrrdi 
 |-  ( ph -> ( F supp .0. ) C_ W )
27 10 6 22 26 gsumcllem 
 |-  ( ( ph /\ W = (/) ) -> F = ( x e. A |-> .0. ) )
28 27 oveq2d 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum F ) = ( G gsum ( x e. A |-> .0. ) ) )
29 2 gsumz 
 |-  ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( x e. A |-> .0. ) ) = .0. )
30 5 6 29 syl2anc 
 |-  ( ph -> ( G gsum ( x e. A |-> .0. ) ) = .0. )
31 30 adantr 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum ( x e. A |-> .0. ) ) = .0. )
32 28 31 eqtrd 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum F ) = .0. )
33 fex 
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
34 10 6 33 syl2anc 
 |-  ( ph -> F e. _V )
35 34 suppun 
 |-  ( ph -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
36 uncom 
 |-  ( F u. H ) = ( H u. F )
37 36 oveq1i 
 |-  ( ( F u. H ) supp .0. ) = ( ( H u. F ) supp .0. )
38 35 37 sseqtrrdi 
 |-  ( ph -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
39 38 9 sseqtrrdi 
 |-  ( ph -> ( H supp .0. ) C_ W )
40 11 6 22 39 gsumcllem 
 |-  ( ( ph /\ W = (/) ) -> H = ( x e. A |-> .0. ) )
41 40 oveq2d 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum H ) = ( G gsum ( x e. A |-> .0. ) ) )
42 41 31 eqtrd 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum H ) = .0. )
43 32 42 oveq12d 
 |-  ( ( ph /\ W = (/) ) -> ( ( G gsum F ) .+ ( G gsum H ) ) = ( .0. .+ .0. ) )
44 6 adantr 
 |-  ( ( ph /\ W = (/) ) -> A e. V )
45 17 ad2antrr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. A ) -> .0. e. B )
46 44 45 45 27 40 offval2 
 |-  ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> ( .0. .+ .0. ) ) )
47 20 mpteq2dv 
 |-  ( ( ph /\ W = (/) ) -> ( x e. A |-> ( .0. .+ .0. ) ) = ( x e. A |-> .0. ) )
48 46 47 eqtrd 
 |-  ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> .0. ) )
49 48 oveq2d 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum ( F oF .+ H ) ) = ( G gsum ( x e. A |-> .0. ) ) )
50 49 31 eqtrd 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum ( F oF .+ H ) ) = .0. )
51 20 43 50 3eqtr4rd 
 |-  ( ( ph /\ W = (/) ) -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )
52 51 ex 
 |-  ( ph -> ( W = (/) -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) )
53 5 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> G e. Mnd )
54 1 3 mndcl 
 |-  ( ( G e. Mnd /\ z e. B /\ w e. B ) -> ( z .+ w ) e. B )
55 54 3expb 
 |-  ( ( G e. Mnd /\ ( z e. B /\ w e. B ) ) -> ( z .+ w ) e. B )
56 53 55 sylan 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( z e. B /\ w e. B ) ) -> ( z .+ w ) e. B )
57 56 caovclg 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
58 simprl 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. NN )
59 nnuz 
 |-  NN = ( ZZ>= ` 1 )
60 58 59 eleqtrdi 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. ( ZZ>= ` 1 ) )
61 10 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F : A --> B )
62 f1of1 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
63 62 ad2antll 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
64 suppssdm 
 |-  ( ( F u. H ) supp .0. ) C_ dom ( F u. H )
65 64 a1i 
 |-  ( ph -> ( ( F u. H ) supp .0. ) C_ dom ( F u. H ) )
66 9 a1i 
 |-  ( ph -> W = ( ( F u. H ) supp .0. ) )
67 dmun 
 |-  dom ( F u. H ) = ( dom F u. dom H )
68 10 fdmd 
 |-  ( ph -> dom F = A )
69 11 fdmd 
 |-  ( ph -> dom H = A )
70 68 69 uneq12d 
 |-  ( ph -> ( dom F u. dom H ) = ( A u. A ) )
71 unidm 
 |-  ( A u. A ) = A
72 70 71 eqtrdi 
 |-  ( ph -> ( dom F u. dom H ) = A )
73 67 72 syl5req 
 |-  ( ph -> A = dom ( F u. H ) )
74 65 66 73 3sstr4d 
 |-  ( ph -> W C_ A )
75 74 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> W C_ A )
76 f1ss 
 |-  ( ( f : ( 1 ... ( # ` W ) ) -1-1-> W /\ W C_ A ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
77 63 75 76 syl2anc 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
78 f1f 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-> A -> f : ( 1 ... ( # ` W ) ) --> A )
79 77 78 syl 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) --> A )
80 fco 
 |-  ( ( F : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
81 61 79 80 syl2anc 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
82 81 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) e. B )
83 11 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H : A --> B )
84 fco 
 |-  ( ( H : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
85 83 79 84 syl2anc 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
86 85 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) e. B )
87 61 ffnd 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F Fn A )
88 83 ffnd 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H Fn A )
89 6 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> A e. V )
90 ovexd 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( 1 ... ( # ` W ) ) e. _V )
91 inidm 
 |-  ( A i^i A ) = A
92 87 88 79 89 89 90 91 ofco 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F oF .+ H ) o. f ) = ( ( F o. f ) oF .+ ( H o. f ) ) )
93 92 fveq1d 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( ( F oF .+ H ) o. f ) ` k ) = ( ( ( F o. f ) oF .+ ( H o. f ) ) ` k ) )
94 93 adantr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F oF .+ H ) o. f ) ` k ) = ( ( ( F o. f ) oF .+ ( H o. f ) ) ` k ) )
95 fnfco 
 |-  ( ( F Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
96 87 79 95 syl2anc 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
97 fnfco 
 |-  ( ( H Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
98 88 79 97 syl2anc 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
99 inidm 
 |-  ( ( 1 ... ( # ` W ) ) i^i ( 1 ... ( # ` W ) ) ) = ( 1 ... ( # ` W ) )
100 eqidd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) = ( ( F o. f ) ` k ) )
101 eqidd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) = ( ( H o. f ) ` k ) )
102 96 98 90 90 99 100 101 ofval 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F o. f ) oF .+ ( H o. f ) ) ` k ) = ( ( ( F o. f ) ` k ) .+ ( ( H o. f ) ` k ) ) )
103 94 102 eqtrd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F oF .+ H ) o. f ) ` k ) = ( ( ( F o. f ) ` k ) .+ ( ( H o. f ) ` k ) ) )
104 5 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> G e. Mnd )
105 elfzouz 
 |-  ( n e. ( 1 ..^ ( # ` W ) ) -> n e. ( ZZ>= ` 1 ) )
106 105 adantl 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> n e. ( ZZ>= ` 1 ) )
107 elfzouz2 
 |-  ( n e. ( 1 ..^ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
108 107 adantl 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
109 fzss2 
 |-  ( ( # ` W ) e. ( ZZ>= ` n ) -> ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) )
110 108 109 syl 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) )
111 110 sselda 
 |-  ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) /\ k e. ( 1 ... n ) ) -> k e. ( 1 ... ( # ` W ) ) )
112 82 adantlr 
 |-  ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) e. B )
113 111 112 syldan 
 |-  ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) /\ k e. ( 1 ... n ) ) -> ( ( F o. f ) ` k ) e. B )
114 1 3 mndcl 
 |-  ( ( G e. Mnd /\ k e. B /\ x e. B ) -> ( k .+ x ) e. B )
115 114 3expb 
 |-  ( ( G e. Mnd /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
116 104 115 sylan 
 |-  ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
117 106 113 116 seqcl 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( F o. f ) ) ` n ) e. B )
118 86 adantlr 
 |-  ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) e. B )
119 111 118 syldan 
 |-  ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) /\ k e. ( 1 ... n ) ) -> ( ( H o. f ) ` k ) e. B )
120 106 119 116 seqcl 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. B )
121 fzofzp1 
 |-  ( n e. ( 1 ..^ ( # ` W ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
122 ffvelrn 
 |-  ( ( ( F o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. B )
123 81 121 122 syl2an 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. B )
124 ffvelrn 
 |-  ( ( ( H o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` ( n + 1 ) ) e. B )
125 85 121 124 syl2an 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( H o. f ) ` ( n + 1 ) ) e. B )
126 fvco3 
 |-  ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) = ( F ` ( f ` ( n + 1 ) ) ) )
127 79 121 126 syl2an 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) = ( F ` ( f ` ( n + 1 ) ) ) )
128 fveq2 
 |-  ( k = ( f ` ( n + 1 ) ) -> ( F ` k ) = ( F ` ( f ` ( n + 1 ) ) ) )
129 128 eleq1d 
 |-  ( k = ( f ` ( n + 1 ) ) -> ( ( F ` k ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) <-> ( F ` ( f ` ( n + 1 ) ) ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
130 15 expr 
 |-  ( ( ph /\ x C_ A ) -> ( k e. ( A \ x ) -> ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) ) )
131 130 ralrimiv 
 |-  ( ( ph /\ x C_ A ) -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) )
132 131 ex 
 |-  ( ph -> ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) ) )
133 132 alrimiv 
 |-  ( ph -> A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) ) )
134 133 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) ) )
135 imassrn 
 |-  ( f " ( 1 ... n ) ) C_ ran f
136 79 adantr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> f : ( 1 ... ( # ` W ) ) --> A )
137 136 frnd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ran f C_ A )
138 135 137 sstrid 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) C_ A )
139 vex 
 |-  f e. _V
140 139 imaex 
 |-  ( f " ( 1 ... n ) ) e. _V
141 sseq1 
 |-  ( x = ( f " ( 1 ... n ) ) -> ( x C_ A <-> ( f " ( 1 ... n ) ) C_ A ) )
142 difeq2 
 |-  ( x = ( f " ( 1 ... n ) ) -> ( A \ x ) = ( A \ ( f " ( 1 ... n ) ) ) )
143 reseq2 
 |-  ( x = ( f " ( 1 ... n ) ) -> ( H |` x ) = ( H |` ( f " ( 1 ... n ) ) ) )
144 143 oveq2d 
 |-  ( x = ( f " ( 1 ... n ) ) -> ( G gsum ( H |` x ) ) = ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) )
145 144 sneqd 
 |-  ( x = ( f " ( 1 ... n ) ) -> { ( G gsum ( H |` x ) ) } = { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } )
146 145 fveq2d 
 |-  ( x = ( f " ( 1 ... n ) ) -> ( Z ` { ( G gsum ( H |` x ) ) } ) = ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
147 146 eleq2d 
 |-  ( x = ( f " ( 1 ... n ) ) -> ( ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) <-> ( F ` k ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
148 142 147 raleqbidv 
 |-  ( x = ( f " ( 1 ... n ) ) -> ( A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) <-> A. k e. ( A \ ( f " ( 1 ... n ) ) ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
149 141 148 imbi12d 
 |-  ( x = ( f " ( 1 ... n ) ) -> ( ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) ) <-> ( ( f " ( 1 ... n ) ) C_ A -> A. k e. ( A \ ( f " ( 1 ... n ) ) ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) ) )
150 140 149 spcv 
 |-  ( A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) ) -> ( ( f " ( 1 ... n ) ) C_ A -> A. k e. ( A \ ( f " ( 1 ... n ) ) ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
151 134 138 150 sylc 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> A. k e. ( A \ ( f " ( 1 ... n ) ) ) ( F ` k ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
152 ffvelrn 
 |-  ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
153 79 121 152 syl2an 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
154 fzp1nel 
 |-  -. ( n + 1 ) e. ( 1 ... n )
155 77 adantr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
156 121 adantl 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
157 f1elima 
 |-  ( ( f : ( 1 ... ( # ` W ) ) -1-1-> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) /\ ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) ) -> ( ( f ` ( n + 1 ) ) e. ( f " ( 1 ... n ) ) <-> ( n + 1 ) e. ( 1 ... n ) ) )
158 155 156 110 157 syl3anc 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( f ` ( n + 1 ) ) e. ( f " ( 1 ... n ) ) <-> ( n + 1 ) e. ( 1 ... n ) ) )
159 154 158 mtbiri 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> -. ( f ` ( n + 1 ) ) e. ( f " ( 1 ... n ) ) )
160 153 159 eldifd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. ( A \ ( f " ( 1 ... n ) ) ) )
161 129 151 160 rspcdva 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( F ` ( f ` ( n + 1 ) ) ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
162 127 161 eqeltrd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
163 140 a1i 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) e. _V )
164 11 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> H : A --> B )
165 164 138 fssresd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( H |` ( f " ( 1 ... n ) ) ) : ( f " ( 1 ... n ) ) --> B )
166 13 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ran H C_ ( Z ` ran H ) )
167 resss 
 |-  ( H |` ( f " ( 1 ... n ) ) ) C_ H
168 167 rnssi 
 |-  ran ( H |` ( f " ( 1 ... n ) ) ) C_ ran H
169 4 cntzidss 
 |-  ( ( ran H C_ ( Z ` ran H ) /\ ran ( H |` ( f " ( 1 ... n ) ) ) C_ ran H ) -> ran ( H |` ( f " ( 1 ... n ) ) ) C_ ( Z ` ran ( H |` ( f " ( 1 ... n ) ) ) ) )
170 166 168 169 sylancl 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ran ( H |` ( f " ( 1 ... n ) ) ) C_ ( Z ` ran ( H |` ( f " ( 1 ... n ) ) ) ) )
171 106 59 eleqtrrdi 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> n e. NN )
172 f1ores 
 |-  ( ( f : ( 1 ... ( # ` W ) ) -1-1-> A /\ ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) )
173 155 110 172 syl2anc 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) )
174 f1of1 
 |-  ( ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-> ( f " ( 1 ... n ) ) )
175 173 174 syl 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-> ( f " ( 1 ... n ) ) )
176 suppssdm 
 |-  ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ dom ( H |` ( f " ( 1 ... n ) ) )
177 dmres 
 |-  dom ( H |` ( f " ( 1 ... n ) ) ) = ( ( f " ( 1 ... n ) ) i^i dom H )
178 177 a1i 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> dom ( H |` ( f " ( 1 ... n ) ) ) = ( ( f " ( 1 ... n ) ) i^i dom H ) )
179 176 178 sseqtrid 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ ( ( f " ( 1 ... n ) ) i^i dom H ) )
180 inss1 
 |-  ( ( f " ( 1 ... n ) ) i^i dom H ) C_ ( f " ( 1 ... n ) )
181 df-ima 
 |-  ( f " ( 1 ... n ) ) = ran ( f |` ( 1 ... n ) )
182 181 a1i 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) = ran ( f |` ( 1 ... n ) ) )
183 180 182 sseqtrid 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( f " ( 1 ... n ) ) i^i dom H ) C_ ran ( f |` ( 1 ... n ) ) )
184 179 183 sstrd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ ran ( f |` ( 1 ... n ) ) )
185 eqid 
 |-  ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) supp .0. ) = ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) supp .0. )
186 1 2 3 4 104 163 165 170 171 175 184 185 gsumval3 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) = ( seq 1 ( .+ , ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ) ` n ) )
187 181 eqimss2i 
 |-  ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) )
188 cores 
 |-  ( ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) ) -> ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( H o. ( f |` ( 1 ... n ) ) ) )
189 187 188 ax-mp 
 |-  ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( H o. ( f |` ( 1 ... n ) ) )
190 resco 
 |-  ( ( H o. f ) |` ( 1 ... n ) ) = ( H o. ( f |` ( 1 ... n ) ) )
191 189 190 eqtr4i 
 |-  ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( ( H o. f ) |` ( 1 ... n ) )
192 191 fveq1i 
 |-  ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( ( H o. f ) |` ( 1 ... n ) ) ` k )
193 fvres 
 |-  ( k e. ( 1 ... n ) -> ( ( ( H o. f ) |` ( 1 ... n ) ) ` k ) = ( ( H o. f ) ` k ) )
194 192 193 syl5eq 
 |-  ( k e. ( 1 ... n ) -> ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( H o. f ) ` k ) )
195 194 adantl 
 |-  ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) /\ k e. ( 1 ... n ) ) -> ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( H o. f ) ` k ) )
196 106 195 seqfveq 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ) ` n ) = ( seq 1 ( .+ , ( H o. f ) ) ` n ) )
197 186 196 eqtr2d 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( H o. f ) ) ` n ) = ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) )
198 fvex 
 |-  ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. _V
199 198 elsn 
 |-  ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } <-> ( seq 1 ( .+ , ( H o. f ) ) ` n ) = ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) )
200 197 199 sylibr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } )
201 3 4 cntzi 
 |-  ( ( ( ( F o. f ) ` ( n + 1 ) ) e. ( Z ` { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) /\ ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. { ( G gsum ( H |` ( f " ( 1 ... n ) ) ) ) } ) -> ( ( ( F o. f ) ` ( n + 1 ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` n ) ) = ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) .+ ( ( F o. f ) ` ( n + 1 ) ) ) )
202 162 200 201 syl2anc 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( ( F o. f ) ` ( n + 1 ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` n ) ) = ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) .+ ( ( F o. f ) ` ( n + 1 ) ) ) )
203 202 eqcomd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) .+ ( ( F o. f ) ` ( n + 1 ) ) ) = ( ( ( F o. f ) ` ( n + 1 ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` n ) ) )
204 1 3 104 117 120 123 125 203 mnd4g 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1 ..^ ( # ` W ) ) ) -> ( ( ( seq 1 ( .+ , ( F o. f ) ) ` n ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` n ) ) .+ ( ( ( F o. f ) ` ( n + 1 ) ) .+ ( ( H o. f ) ` ( n + 1 ) ) ) ) = ( ( ( seq 1 ( .+ , ( F o. f ) ) ` n ) .+ ( ( F o. f ) ` ( n + 1 ) ) ) .+ ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) .+ ( ( H o. f ) ` ( n + 1 ) ) ) ) )
205 57 57 60 82 86 103 204 seqcaopr3 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( seq 1 ( .+ , ( ( F oF .+ H ) o. f ) ) ` ( # ` W ) ) = ( ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` ( # ` W ) ) ) )
206 56 61 83 89 89 91 off 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
207 14 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
208 53 115 sylan 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
209 208 61 83 89 89 91 off 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
210 eldifi 
 |-  ( x e. ( A \ ran f ) -> x e. A )
211 eqidd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
212 eqidd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( H ` x ) = ( H ` x ) )
213 87 88 89 89 91 211 212 ofval 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( ( F oF .+ H ) ` x ) = ( ( F ` x ) .+ ( H ` x ) ) )
214 210 213 sylan2 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F oF .+ H ) ` x ) = ( ( F ` x ) .+ ( H ` x ) ) )
215 25 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) )
216 f1ofo 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -onto-> W )
217 forn 
 |-  ( f : ( 1 ... ( # ` W ) ) -onto-> W -> ran f = W )
218 216 217 syl 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = W )
219 218 9 eqtrdi 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = ( ( F u. H ) supp .0. ) )
220 219 sseq2d 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( ( F supp .0. ) C_ ran f <-> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
221 220 ad2antll 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F supp .0. ) C_ ran f <-> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
222 215 221 mpbird 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ran f )
223 21 a1i 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> .0. e. _V )
224 61 222 89 223 suppssr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( F ` x ) = .0. )
225 35 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
226 225 37 sseqtrrdi 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
227 219 sseq2d 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( ( H supp .0. ) C_ ran f <-> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
228 227 ad2antll 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( H supp .0. ) C_ ran f <-> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
229 226 228 mpbird 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ran f )
230 83 229 89 223 suppssr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( H ` x ) = .0. )
231 224 230 oveq12d 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F ` x ) .+ ( H ` x ) ) = ( .0. .+ .0. ) )
232 19 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( .0. .+ .0. ) = .0. )
233 214 231 232 3eqtrd 
 |-  ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F oF .+ H ) ` x ) = .0. )
234 209 233 suppss 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F oF .+ H ) supp .0. ) C_ ran f )
235 ovex 
 |-  ( F oF .+ H ) e. _V
236 235 139 coex 
 |-  ( ( F oF .+ H ) o. f ) e. _V
237 suppimacnv 
 |-  ( ( ( ( F oF .+ H ) o. f ) e. _V /\ .0. e. _V ) -> ( ( ( F oF .+ H ) o. f ) supp .0. ) = ( `' ( ( F oF .+ H ) o. f ) " ( _V \ { .0. } ) ) )
238 237 eqcomd 
 |-  ( ( ( ( F oF .+ H ) o. f ) e. _V /\ .0. e. _V ) -> ( `' ( ( F oF .+ H ) o. f ) " ( _V \ { .0. } ) ) = ( ( ( F oF .+ H ) o. f ) supp .0. ) )
239 236 21 238 mp2an 
 |-  ( `' ( ( F oF .+ H ) o. f ) " ( _V \ { .0. } ) ) = ( ( ( F oF .+ H ) o. f ) supp .0. )
240 1 2 3 4 53 89 206 207 58 77 234 239 gsumval3 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsum ( F oF .+ H ) ) = ( seq 1 ( .+ , ( ( F oF .+ H ) o. f ) ) ` ( # ` W ) ) )
241 12 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran F C_ ( Z ` ran F ) )
242 eqid 
 |-  ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
243 1 2 3 4 53 89 61 241 58 77 222 242 gsumval3 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsum F ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) )
244 13 adantr 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran H C_ ( Z ` ran H ) )
245 eqid 
 |-  ( ( H o. f ) supp .0. ) = ( ( H o. f ) supp .0. )
246 1 2 3 4 53 89 83 244 58 77 229 245 gsumval3 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsum H ) = ( seq 1 ( .+ , ( H o. f ) ) ` ( # ` W ) ) )
247 243 246 oveq12d 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( G gsum F ) .+ ( G gsum H ) ) = ( ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` ( # ` W ) ) ) )
248 205 240 247 3eqtr4d 
 |-  ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )
249 248 expr 
 |-  ( ( ph /\ ( # ` W ) e. NN ) -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) )
250 249 exlimdv 
 |-  ( ( ph /\ ( # ` W ) e. NN ) -> ( E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) )
251 250 expimpd 
 |-  ( ph -> ( ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) )
252 7 8 fsuppun 
 |-  ( ph -> ( ( F u. H ) supp .0. ) e. Fin )
253 9 252 eqeltrid 
 |-  ( ph -> W e. Fin )
254 fz1f1o 
 |-  ( W e. Fin -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
255 253 254 syl 
 |-  ( ph -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
256 52 251 255 mpjaod 
 |-  ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )