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