Metamath Proof Explorer

Theorem seqcoll

Description: The function F contains a sparse set of nonzero values to be summed. The function G is an order isomorphism from the set of nonzero values of F to a 1-based finite sequence, and H collects these nonzero values together. Under these conditions, the sum over the values in H yields the same result as the sum over the original set F . (Contributed by Mario Carneiro, 2-Apr-2014)

Ref Expression
Hypotheses seqcoll.1 
|- ( ( ph /\ k e. S ) -> ( Z .+ k ) = k )
seqcoll.1b 
|- ( ( ph /\ k e. S ) -> ( k .+ Z ) = k )
seqcoll.c 
|- ( ( ph /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )
seqcoll.a 
|- ( ph -> Z e. S )
seqcoll.2 
|- ( ph -> G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
seqcoll.3 
|- ( ph -> N e. ( 1 ... ( # ` A ) ) )
seqcoll.4 
|- ( ph -> A C_ ( ZZ>= ` M ) )
seqcoll.5 
|- ( ( ph /\ k e. ( M ... ( G ` ( # ` A ) ) ) ) -> ( F ` k ) e. S )
seqcoll.6 
|- ( ( ph /\ k e. ( ( M ... ( G ` ( # ` A ) ) ) \ A ) ) -> ( F ` k ) = Z )
seqcoll.7 
|- ( ( ph /\ n e. ( 1 ... ( # ` A ) ) ) -> ( H ` n ) = ( F ` ( G ` n ) ) )
Assertion seqcoll 
|- ( ph -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) )

Proof

Step Hyp Ref Expression
1 seqcoll.1 
 |-  ( ( ph /\ k e. S ) -> ( Z .+ k ) = k )
2 seqcoll.1b 
 |-  ( ( ph /\ k e. S ) -> ( k .+ Z ) = k )
3 seqcoll.c 
 |-  ( ( ph /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )
4 seqcoll.a 
 |-  ( ph -> Z e. S )
5 seqcoll.2 
 |-  ( ph -> G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
6 seqcoll.3 
 |-  ( ph -> N e. ( 1 ... ( # ` A ) ) )
7 seqcoll.4 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
8 seqcoll.5 
 |-  ( ( ph /\ k e. ( M ... ( G ` ( # ` A ) ) ) ) -> ( F ` k ) e. S )
9 seqcoll.6 
 |-  ( ( ph /\ k e. ( ( M ... ( G ` ( # ` A ) ) ) \ A ) ) -> ( F ` k ) = Z )
10 seqcoll.7 
 |-  ( ( ph /\ n e. ( 1 ... ( # ` A ) ) ) -> ( H ` n ) = ( F ` ( G ` n ) ) )
11 elfznn 
 |-  ( N e. ( 1 ... ( # ` A ) ) -> N e. NN )
12 6 11 syl 
 |-  ( ph -> N e. NN )
13 eleq1 
 |-  ( y = 1 -> ( y e. ( 1 ... ( # ` A ) ) <-> 1 e. ( 1 ... ( # ` A ) ) ) )
14 2fveq3 
 |-  ( y = 1 -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` 1 ) ) )
15 fveq2 
 |-  ( y = 1 -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` 1 ) )
16 14 15 eqeq12d 
 |-  ( y = 1 -> ( ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) <-> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) ) )
17 13 16 imbi12d 
 |-  ( y = 1 -> ( ( y e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) <-> ( 1 e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) ) ) )
18 17 imbi2d 
 |-  ( y = 1 -> ( ( ph -> ( y e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) ) <-> ( ph -> ( 1 e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) ) ) ) )
19 eleq1 
 |-  ( y = m -> ( y e. ( 1 ... ( # ` A ) ) <-> m e. ( 1 ... ( # ` A ) ) ) )
20 2fveq3 
 |-  ( y = m -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` m ) ) )
21 fveq2 
 |-  ( y = m -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` m ) )
22 20 21 eqeq12d 
 |-  ( y = m -> ( ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) <-> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) )
23 19 22 imbi12d 
 |-  ( y = m -> ( ( y e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) <-> ( m e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) ) )
24 23 imbi2d 
 |-  ( y = m -> ( ( ph -> ( y e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) ) <-> ( ph -> ( m e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) ) ) )
25 eleq1 
 |-  ( y = ( m + 1 ) -> ( y e. ( 1 ... ( # ` A ) ) <-> ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) )
26 2fveq3 
 |-  ( y = ( m + 1 ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) )
27 fveq2 
 |-  ( y = ( m + 1 ) -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) )
28 26 27 eqeq12d 
 |-  ( y = ( m + 1 ) -> ( ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) <-> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) )
29 25 28 imbi12d 
 |-  ( y = ( m + 1 ) -> ( ( y e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) <-> ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) )
30 29 imbi2d 
 |-  ( y = ( m + 1 ) -> ( ( ph -> ( y e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) ) <-> ( ph -> ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) ) )
31 eleq1 
 |-  ( y = N -> ( y e. ( 1 ... ( # ` A ) ) <-> N e. ( 1 ... ( # ` A ) ) ) )
32 2fveq3 
 |-  ( y = N -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` N ) ) )
33 fveq2 
 |-  ( y = N -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` N ) )
34 32 33 eqeq12d 
 |-  ( y = N -> ( ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) <-> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) )
35 31 34 imbi12d 
 |-  ( y = N -> ( ( y e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) <-> ( N e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) ) )
36 35 imbi2d 
 |-  ( y = N -> ( ( ph -> ( y e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) ) <-> ( ph -> ( N e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) ) ) )
37 isof1o 
 |-  ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> G : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
38 5 37 syl 
 |-  ( ph -> G : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
39 f1of 
 |-  ( G : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> G : ( 1 ... ( # ` A ) ) --> A )
40 38 39 syl 
 |-  ( ph -> G : ( 1 ... ( # ` A ) ) --> A )
41 elfzuz2 
 |-  ( N e. ( 1 ... ( # ` A ) ) -> ( # ` A ) e. ( ZZ>= ` 1 ) )
42 6 41 syl 
 |-  ( ph -> ( # ` A ) e. ( ZZ>= ` 1 ) )
43 eluzfz1 
 |-  ( ( # ` A ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( # ` A ) ) )
44 42 43 syl 
 |-  ( ph -> 1 e. ( 1 ... ( # ` A ) ) )
45 40 44 ffvelrnd 
 |-  ( ph -> ( G ` 1 ) e. A )
46 7 45 sseldd 
 |-  ( ph -> ( G ` 1 ) e. ( ZZ>= ` M ) )
47 eluzle 
 |-  ( ( # ` A ) e. ( ZZ>= ` 1 ) -> 1 <_ ( # ` A ) )
48 42 47 syl 
 |-  ( ph -> 1 <_ ( # ` A ) )
49 fzssz 
 |-  ( 1 ... ( # ` A ) ) C_ ZZ
50 zssre 
 |-  ZZ C_ RR
51 49 50 sstri 
 |-  ( 1 ... ( # ` A ) ) C_ RR
52 51 a1i 
 |-  ( ph -> ( 1 ... ( # ` A ) ) C_ RR )
53 ressxr 
 |-  RR C_ RR*
54 52 53 sstrdi 
 |-  ( ph -> ( 1 ... ( # ` A ) ) C_ RR* )
55 eluzelre 
 |-  ( k e. ( ZZ>= ` M ) -> k e. RR )
56 55 ssriv 
 |-  ( ZZ>= ` M ) C_ RR
57 7 56 sstrdi 
 |-  ( ph -> A C_ RR )
58 57 53 sstrdi 
 |-  ( ph -> A C_ RR* )
59 eluzfz2 
 |-  ( ( # ` A ) e. ( ZZ>= ` 1 ) -> ( # ` A ) e. ( 1 ... ( # ` A ) ) )
60 42 59 syl 
 |-  ( ph -> ( # ` A ) e. ( 1 ... ( # ` A ) ) )
61 leisorel 
 |-  ( ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) /\ ( ( 1 ... ( # ` A ) ) C_ RR* /\ A C_ RR* ) /\ ( 1 e. ( 1 ... ( # ` A ) ) /\ ( # ` A ) e. ( 1 ... ( # ` A ) ) ) ) -> ( 1 <_ ( # ` A ) <-> ( G ` 1 ) <_ ( G ` ( # ` A ) ) ) )
62 5 54 58 44 60 61 syl122anc 
 |-  ( ph -> ( 1 <_ ( # ` A ) <-> ( G ` 1 ) <_ ( G ` ( # ` A ) ) ) )
63 48 62 mpbid 
 |-  ( ph -> ( G ` 1 ) <_ ( G ` ( # ` A ) ) )
64 40 60 ffvelrnd 
 |-  ( ph -> ( G ` ( # ` A ) ) e. A )
65 7 64 sseldd 
 |-  ( ph -> ( G ` ( # ` A ) ) e. ( ZZ>= ` M ) )
66 eluzelz 
 |-  ( ( G ` ( # ` A ) ) e. ( ZZ>= ` M ) -> ( G ` ( # ` A ) ) e. ZZ )
67 65 66 syl 
 |-  ( ph -> ( G ` ( # ` A ) ) e. ZZ )
68 elfz5 
 |-  ( ( ( G ` 1 ) e. ( ZZ>= ` M ) /\ ( G ` ( # ` A ) ) e. ZZ ) -> ( ( G ` 1 ) e. ( M ... ( G ` ( # ` A ) ) ) <-> ( G ` 1 ) <_ ( G ` ( # ` A ) ) ) )
69 46 67 68 syl2anc 
 |-  ( ph -> ( ( G ` 1 ) e. ( M ... ( G ` ( # ` A ) ) ) <-> ( G ` 1 ) <_ ( G ` ( # ` A ) ) ) )
70 63 69 mpbird 
 |-  ( ph -> ( G ` 1 ) e. ( M ... ( G ` ( # ` A ) ) ) )
71 fveq2 
 |-  ( k = ( G ` 1 ) -> ( F ` k ) = ( F ` ( G ` 1 ) ) )
72 71 eleq1d 
 |-  ( k = ( G ` 1 ) -> ( ( F ` k ) e. S <-> ( F ` ( G ` 1 ) ) e. S ) )
73 72 imbi2d 
 |-  ( k = ( G ` 1 ) -> ( ( ph -> ( F ` k ) e. S ) <-> ( ph -> ( F ` ( G ` 1 ) ) e. S ) ) )
74 8 expcom 
 |-  ( k e. ( M ... ( G ` ( # ` A ) ) ) -> ( ph -> ( F ` k ) e. S ) )
75 73 74 vtoclga 
 |-  ( ( G ` 1 ) e. ( M ... ( G ` ( # ` A ) ) ) -> ( ph -> ( F ` ( G ` 1 ) ) e. S ) )
76 70 75 mpcom 
 |-  ( ph -> ( F ` ( G ` 1 ) ) e. S )
77 eluzelz 
 |-  ( ( G ` 1 ) e. ( ZZ>= ` M ) -> ( G ` 1 ) e. ZZ )
78 46 77 syl 
 |-  ( ph -> ( G ` 1 ) e. ZZ )
79 peano2zm 
 |-  ( ( G ` 1 ) e. ZZ -> ( ( G ` 1 ) - 1 ) e. ZZ )
80 78 79 syl 
 |-  ( ph -> ( ( G ` 1 ) - 1 ) e. ZZ )
81 80 zred 
 |-  ( ph -> ( ( G ` 1 ) - 1 ) e. RR )
82 78 zred 
 |-  ( ph -> ( G ` 1 ) e. RR )
83 67 zred 
 |-  ( ph -> ( G ` ( # ` A ) ) e. RR )
84 82 lem1d 
 |-  ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` 1 ) )
85 81 82 83 84 63 letrd 
 |-  ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` ( # ` A ) ) )
86 eluz 
 |-  ( ( ( ( G ` 1 ) - 1 ) e. ZZ /\ ( G ` ( # ` A ) ) e. ZZ ) -> ( ( G ` ( # ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) <-> ( ( G ` 1 ) - 1 ) <_ ( G ` ( # ` A ) ) ) )
87 80 67 86 syl2anc 
 |-  ( ph -> ( ( G ` ( # ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) <-> ( ( G ` 1 ) - 1 ) <_ ( G ` ( # ` A ) ) ) )
88 85 87 mpbird 
 |-  ( ph -> ( G ` ( # ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) )
89 fzss2 
 |-  ( ( G ` ( # ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) -> ( M ... ( ( G ` 1 ) - 1 ) ) C_ ( M ... ( G ` ( # ` A ) ) ) )
90 88 89 syl 
 |-  ( ph -> ( M ... ( ( G ` 1 ) - 1 ) ) C_ ( M ... ( G ` ( # ` A ) ) ) )
91 90 sselda 
 |-  ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> k e. ( M ... ( G ` ( # ` A ) ) ) )
92 eluzel2 
 |-  ( ( G ` 1 ) e. ( ZZ>= ` M ) -> M e. ZZ )
93 46 92 syl 
 |-  ( ph -> M e. ZZ )
94 elfzm11 
 |-  ( ( M e. ZZ /\ ( G ` 1 ) e. ZZ ) -> ( k e. ( M ... ( ( G ` 1 ) - 1 ) ) <-> ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) ) )
95 93 78 94 syl2anc 
 |-  ( ph -> ( k e. ( M ... ( ( G ` 1 ) - 1 ) ) <-> ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) ) )
96 simp3 
 |-  ( ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) -> k < ( G ` 1 ) )
97 82 adantr 
 |-  ( ( ph /\ k e. A ) -> ( G ` 1 ) e. RR )
98 57 sselda 
 |-  ( ( ph /\ k e. A ) -> k e. RR )
99 f1ocnv 
 |-  ( G : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> `' G : A -1-1-onto-> ( 1 ... ( # ` A ) ) )
100 38 99 syl 
 |-  ( ph -> `' G : A -1-1-onto-> ( 1 ... ( # ` A ) ) )
101 f1of 
 |-  ( `' G : A -1-1-onto-> ( 1 ... ( # ` A ) ) -> `' G : A --> ( 1 ... ( # ` A ) ) )
102 100 101 syl 
 |-  ( ph -> `' G : A --> ( 1 ... ( # ` A ) ) )
103 102 ffvelrnda 
 |-  ( ( ph /\ k e. A ) -> ( `' G ` k ) e. ( 1 ... ( # ` A ) ) )
104 elfznn 
 |-  ( ( `' G ` k ) e. ( 1 ... ( # ` A ) ) -> ( `' G ` k ) e. NN )
105 103 104 syl 
 |-  ( ( ph /\ k e. A ) -> ( `' G ` k ) e. NN )
106 105 nnge1d 
 |-  ( ( ph /\ k e. A ) -> 1 <_ ( `' G ` k ) )
107 5 adantr 
 |-  ( ( ph /\ k e. A ) -> G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
108 54 adantr 
 |-  ( ( ph /\ k e. A ) -> ( 1 ... ( # ` A ) ) C_ RR* )
109 58 adantr 
 |-  ( ( ph /\ k e. A ) -> A C_ RR* )
110 44 adantr 
 |-  ( ( ph /\ k e. A ) -> 1 e. ( 1 ... ( # ` A ) ) )
111 leisorel 
 |-  ( ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) /\ ( ( 1 ... ( # ` A ) ) C_ RR* /\ A C_ RR* ) /\ ( 1 e. ( 1 ... ( # ` A ) ) /\ ( `' G ` k ) e. ( 1 ... ( # ` A ) ) ) ) -> ( 1 <_ ( `' G ` k ) <-> ( G ` 1 ) <_ ( G ` ( `' G ` k ) ) ) )
112 107 108 109 110 103 111 syl122anc 
 |-  ( ( ph /\ k e. A ) -> ( 1 <_ ( `' G ` k ) <-> ( G ` 1 ) <_ ( G ` ( `' G ` k ) ) ) )
113 106 112 mpbid 
 |-  ( ( ph /\ k e. A ) -> ( G ` 1 ) <_ ( G ` ( `' G ` k ) ) )
114 f1ocnvfv2 
 |-  ( ( G : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ k e. A ) -> ( G ` ( `' G ` k ) ) = k )
115 38 114 sylan 
 |-  ( ( ph /\ k e. A ) -> ( G ` ( `' G ` k ) ) = k )
116 113 115 breqtrd 
 |-  ( ( ph /\ k e. A ) -> ( G ` 1 ) <_ k )
117 97 98 116 lensymd 
 |-  ( ( ph /\ k e. A ) -> -. k < ( G ` 1 ) )
118 117 ex 
 |-  ( ph -> ( k e. A -> -. k < ( G ` 1 ) ) )
119 118 con2d 
 |-  ( ph -> ( k < ( G ` 1 ) -> -. k e. A ) )
120 96 119 syl5 
 |-  ( ph -> ( ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) -> -. k e. A ) )
121 95 120 sylbid 
 |-  ( ph -> ( k e. ( M ... ( ( G ` 1 ) - 1 ) ) -> -. k e. A ) )
122 121 imp 
 |-  ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> -. k e. A )
123 91 122 eldifd 
 |-  ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> k e. ( ( M ... ( G ` ( # ` A ) ) ) \ A ) )
124 123 9 syldan 
 |-  ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> ( F ` k ) = Z )
125 1 4 46 76 124 seqid 
 |-  ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) = seq ( G ` 1 ) ( .+ , F ) )
126 125 fveq1d 
 |-  ( ph -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) ` ( G ` 1 ) ) = ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) )
127 uzid 
 |-  ( ( G ` 1 ) e. ZZ -> ( G ` 1 ) e. ( ZZ>= ` ( G ` 1 ) ) )
128 78 127 syl 
 |-  ( ph -> ( G ` 1 ) e. ( ZZ>= ` ( G ` 1 ) ) )
129 128 fvresd 
 |-  ( ph -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) ` ( G ` 1 ) ) = ( seq M ( .+ , F ) ` ( G ` 1 ) ) )
130 seq1 
 |-  ( ( G ` 1 ) e. ZZ -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( F ` ( G ` 1 ) ) )
131 78 130 syl 
 |-  ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( F ` ( G ` 1 ) ) )
132 fveq2 
 |-  ( n = 1 -> ( H ` n ) = ( H ` 1 ) )
133 2fveq3 
 |-  ( n = 1 -> ( F ` ( G ` n ) ) = ( F ` ( G ` 1 ) ) )
134 132 133 eqeq12d 
 |-  ( n = 1 -> ( ( H ` n ) = ( F ` ( G ` n ) ) <-> ( H ` 1 ) = ( F ` ( G ` 1 ) ) ) )
135 134 imbi2d 
 |-  ( n = 1 -> ( ( ph -> ( H ` n ) = ( F ` ( G ` n ) ) ) <-> ( ph -> ( H ` 1 ) = ( F ` ( G ` 1 ) ) ) ) )
136 10 expcom 
 |-  ( n e. ( 1 ... ( # ` A ) ) -> ( ph -> ( H ` n ) = ( F ` ( G ` n ) ) ) )
137 135 136 vtoclga 
 |-  ( 1 e. ( 1 ... ( # ` A ) ) -> ( ph -> ( H ` 1 ) = ( F ` ( G ` 1 ) ) ) )
138 44 137 mpcom 
 |-  ( ph -> ( H ` 1 ) = ( F ` ( G ` 1 ) ) )
139 131 138 eqtr4d 
 |-  ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
140 126 129 139 3eqtr3d 
 |-  ( ph -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
141 1z 
 |-  1 e. ZZ
142 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( .+ , H ) ` 1 ) = ( H ` 1 ) )
143 141 142 ax-mp 
 |-  ( seq 1 ( .+ , H ) ` 1 ) = ( H ` 1 )
144 140 143 eqtr4di 
 |-  ( ph -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) )
145 144 a1d 
 |-  ( ph -> ( 1 e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) ) )
146 simplr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> m e. NN )
147 nnuz 
 |-  NN = ( ZZ>= ` 1 )
148 146 147 eleqtrdi 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> m e. ( ZZ>= ` 1 ) )
149 nnz 
 |-  ( m e. NN -> m e. ZZ )
150 149 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> m e. ZZ )
151 elfzuz3 
 |-  ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( # ` A ) e. ( ZZ>= ` ( m + 1 ) ) )
152 151 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( # ` A ) e. ( ZZ>= ` ( m + 1 ) ) )
153 peano2uzr 
 |-  ( ( m e. ZZ /\ ( # ` A ) e. ( ZZ>= ` ( m + 1 ) ) ) -> ( # ` A ) e. ( ZZ>= ` m ) )
154 150 152 153 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( # ` A ) e. ( ZZ>= ` m ) )
155 elfzuzb 
 |-  ( m e. ( 1 ... ( # ` A ) ) <-> ( m e. ( ZZ>= ` 1 ) /\ ( # ` A ) e. ( ZZ>= ` m ) ) )
156 148 154 155 sylanbrc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> m e. ( 1 ... ( # ` A ) ) )
157 156 ex 
 |-  ( ( ph /\ m e. NN ) -> ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> m e. ( 1 ... ( # ` A ) ) ) )
158 157 imim1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( m e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) -> ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) ) )
159 oveq1 
 |-  ( ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( H ` ( m + 1 ) ) ) = ( ( seq 1 ( .+ , H ) ` m ) .+ ( H ` ( m + 1 ) ) ) )
160 2 ad4ant14 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. S ) -> ( k .+ Z ) = k )
161 7 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> A C_ ( ZZ>= ` M ) )
162 40 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> G : ( 1 ... ( # ` A ) ) --> A )
163 162 156 ffvelrnd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` m ) e. A )
164 161 163 sseldd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` m ) e. ( ZZ>= ` M ) )
165 nnre 
 |-  ( m e. NN -> m e. RR )
166 165 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> m e. RR )
167 166 ltp1d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> m < ( m + 1 ) )
168 5 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
169 simpr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( m + 1 ) e. ( 1 ... ( # ` A ) ) )
170 isorel 
 |-  ( ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) /\ ( m e. ( 1 ... ( # ` A ) ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) ) -> ( m < ( m + 1 ) <-> ( G ` m ) < ( G ` ( m + 1 ) ) ) )
171 168 156 169 170 syl12anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( m < ( m + 1 ) <-> ( G ` m ) < ( G ` ( m + 1 ) ) ) )
172 167 171 mpbid 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` m ) < ( G ` ( m + 1 ) ) )
173 eluzelz 
 |-  ( ( G ` m ) e. ( ZZ>= ` M ) -> ( G ` m ) e. ZZ )
174 164 173 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` m ) e. ZZ )
175 162 169 ffvelrnd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( m + 1 ) ) e. A )
176 161 175 sseldd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` M ) )
177 eluzelz 
 |-  ( ( G ` ( m + 1 ) ) e. ( ZZ>= ` M ) -> ( G ` ( m + 1 ) ) e. ZZ )
178 176 177 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ZZ )
179 zltlem1 
 |-  ( ( ( G ` m ) e. ZZ /\ ( G ` ( m + 1 ) ) e. ZZ ) -> ( ( G ` m ) < ( G ` ( m + 1 ) ) <-> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
180 174 178 179 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` m ) < ( G ` ( m + 1 ) ) <-> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
181 172 180 mpbid 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) )
182 peano2zm 
 |-  ( ( G ` ( m + 1 ) ) e. ZZ -> ( ( G ` ( m + 1 ) ) - 1 ) e. ZZ )
183 178 182 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ZZ )
184 eluz 
 |-  ( ( ( G ` m ) e. ZZ /\ ( ( G ` ( m + 1 ) ) - 1 ) e. ZZ ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) <-> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
185 174 183 184 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) <-> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
186 181 185 mpbird 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) )
187 183 zred 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. RR )
188 178 zred 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( m + 1 ) ) e. RR )
189 83 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( # ` A ) ) e. RR )
190 188 lem1d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` ( m + 1 ) ) )
191 elfzle2 
 |-  ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( m + 1 ) <_ ( # ` A ) )
192 191 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( m + 1 ) <_ ( # ` A ) )
193 54 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( 1 ... ( # ` A ) ) C_ RR* )
194 58 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> A C_ RR* )
195 60 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( # ` A ) e. ( 1 ... ( # ` A ) ) )
196 leisorel 
 |-  ( ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) /\ ( ( 1 ... ( # ` A ) ) C_ RR* /\ A C_ RR* ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ ( # ` A ) e. ( 1 ... ( # ` A ) ) ) ) -> ( ( m + 1 ) <_ ( # ` A ) <-> ( G ` ( m + 1 ) ) <_ ( G ` ( # ` A ) ) ) )
197 168 193 194 169 195 196 syl122anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( m + 1 ) <_ ( # ` A ) <-> ( G ` ( m + 1 ) ) <_ ( G ` ( # ` A ) ) ) )
198 192 197 mpbid 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( m + 1 ) ) <_ ( G ` ( # ` A ) ) )
199 187 188 189 190 198 letrd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` ( # ` A ) ) )
200 67 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( # ` A ) ) e. ZZ )
201 eluz 
 |-  ( ( ( ( G ` ( m + 1 ) ) - 1 ) e. ZZ /\ ( G ` ( # ` A ) ) e. ZZ ) -> ( ( G ` ( # ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) <-> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` ( # ` A ) ) ) )
202 183 200 201 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` ( # ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) <-> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` ( # ` A ) ) ) )
203 199 202 mpbird 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( # ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) )
204 uztrn 
 |-  ( ( ( G ` ( # ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) /\ ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) ) -> ( G ` ( # ` A ) ) e. ( ZZ>= ` ( G ` m ) ) )
205 203 186 204 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( # ` A ) ) e. ( ZZ>= ` ( G ` m ) ) )
206 fzss2 
 |-  ( ( G ` ( # ` A ) ) e. ( ZZ>= ` ( G ` m ) ) -> ( M ... ( G ` m ) ) C_ ( M ... ( G ` ( # ` A ) ) ) )
207 205 206 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( M ... ( G ` m ) ) C_ ( M ... ( G ` ( # ` A ) ) ) )
208 207 sselda 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( M ... ( G ` m ) ) ) -> k e. ( M ... ( G ` ( # ` A ) ) ) )
209 8 ad4ant14 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( M ... ( G ` ( # ` A ) ) ) ) -> ( F ` k ) e. S )
210 208 209 syldan 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( M ... ( G ` m ) ) ) -> ( F ` k ) e. S )
211 3 ad4ant14 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )
212 164 210 211 seqcl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) e. S )
213 simplll 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ph )
214 elfzuz 
 |-  ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( ( G ` m ) + 1 ) ) )
215 peano2uz 
 |-  ( ( G ` m ) e. ( ZZ>= ` M ) -> ( ( G ` m ) + 1 ) e. ( ZZ>= ` M ) )
216 164 215 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` m ) + 1 ) e. ( ZZ>= ` M ) )
217 uztrn 
 |-  ( ( k e. ( ZZ>= ` ( ( G ` m ) + 1 ) ) /\ ( ( G ` m ) + 1 ) e. ( ZZ>= ` M ) ) -> k e. ( ZZ>= ` M ) )
218 214 216 217 syl2anr 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> k e. ( ZZ>= ` M ) )
219 elfzuz3 
 |-  ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` k ) )
220 uztrn 
 |-  ( ( ( G ` ( # ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) /\ ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` k ) ) -> ( G ` ( # ` A ) ) e. ( ZZ>= ` k ) )
221 203 219 220 syl2an 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ( G ` ( # ` A ) ) e. ( ZZ>= ` k ) )
222 elfzuzb 
 |-  ( k e. ( M ... ( G ` ( # ` A ) ) ) <-> ( k e. ( ZZ>= ` M ) /\ ( G ` ( # ` A ) ) e. ( ZZ>= ` k ) ) )
223 218 221 222 sylanbrc 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> k e. ( M ... ( G ` ( # ` A ) ) ) )
224 149 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> m e. ZZ )
225 102 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> `' G : A --> ( 1 ... ( # ` A ) ) )
226 simprr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> k e. A )
227 225 226 ffvelrnd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( `' G ` k ) e. ( 1 ... ( # ` A ) ) )
228 elfzelz 
 |-  ( ( `' G ` k ) e. ( 1 ... ( # ` A ) ) -> ( `' G ` k ) e. ZZ )
229 227 228 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( `' G ` k ) e. ZZ )
230 btwnnz 
 |-  ( ( m e. ZZ /\ m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ )
231 230 3expib 
 |-  ( m e. ZZ -> ( ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ ) )
232 231 con2d 
 |-  ( m e. ZZ -> ( ( `' G ` k ) e. ZZ -> -. ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) ) )
233 224 229 232 sylc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> -. ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) )
234 5 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
235 156 adantrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> m e. ( 1 ... ( # ` A ) ) )
236 isorel 
 |-  ( ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) /\ ( m e. ( 1 ... ( # ` A ) ) /\ ( `' G ` k ) e. ( 1 ... ( # ` A ) ) ) ) -> ( m < ( `' G ` k ) <-> ( G ` m ) < ( G ` ( `' G ` k ) ) ) )
237 234 235 227 236 syl12anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( G ` m ) < ( G ` ( `' G ` k ) ) ) )
238 38 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> G : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
239 238 226 114 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( G ` ( `' G ` k ) ) = k )
240 239 breq2d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( G ` m ) < ( G ` ( `' G ` k ) ) <-> ( G ` m ) < k ) )
241 174 adantrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( G ` m ) e. ZZ )
242 7 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> A C_ ( ZZ>= ` M ) )
243 242 226 sseldd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> k e. ( ZZ>= ` M ) )
244 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
245 243 244 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> k e. ZZ )
246 zltp1le 
 |-  ( ( ( G ` m ) e. ZZ /\ k e. ZZ ) -> ( ( G ` m ) < k <-> ( ( G ` m ) + 1 ) <_ k ) )
247 241 245 246 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( G ` m ) < k <-> ( ( G ` m ) + 1 ) <_ k ) )
248 237 240 247 3bitrd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( ( G ` m ) + 1 ) <_ k ) )
249 169 adantrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( m + 1 ) e. ( 1 ... ( # ` A ) ) )
250 isorel 
 |-  ( ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) /\ ( ( `' G ` k ) e. ( 1 ... ( # ` A ) ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) ) -> ( ( `' G ` k ) < ( m + 1 ) <-> ( G ` ( `' G ` k ) ) < ( G ` ( m + 1 ) ) ) )
251 234 227 249 250 syl12anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( `' G ` k ) < ( m + 1 ) <-> ( G ` ( `' G ` k ) ) < ( G ` ( m + 1 ) ) ) )
252 239 breq1d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( G ` ( `' G ` k ) ) < ( G ` ( m + 1 ) ) <-> k < ( G ` ( m + 1 ) ) ) )
253 178 adantrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( G ` ( m + 1 ) ) e. ZZ )
254 zltlem1 
 |-  ( ( k e. ZZ /\ ( G ` ( m + 1 ) ) e. ZZ ) -> ( k < ( G ` ( m + 1 ) ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
255 245 253 254 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( k < ( G ` ( m + 1 ) ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
256 251 252 255 3bitrd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( `' G ` k ) < ( m + 1 ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
257 248 256 anbi12d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) <-> ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) ) )
258 233 257 mtbid 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> -. ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
259 258 expr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( k e. A -> -. ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) ) )
260 259 con2d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) -> -. k e. A ) )
261 elfzle1 
 |-  ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` m ) + 1 ) <_ k )
262 elfzle2 
 |-  ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k <_ ( ( G ` ( m + 1 ) ) - 1 ) )
263 261 262 jca 
 |-  ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
264 260 263 impel 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> -. k e. A )
265 223 264 eldifd 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> k e. ( ( M ... ( G ` ( # ` A ) ) ) \ A ) )
266 213 265 9 syl2anc 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ( F ` k ) = Z )
267 160 164 186 212 266 seqid2 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq M ( .+ , F ) ` ( ( G ` ( m + 1 ) ) - 1 ) ) )
268 267 oveq1d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( F ` ( G ` ( m + 1 ) ) ) ) = ( ( seq M ( .+ , F ) ` ( ( G ` ( m + 1 ) ) - 1 ) ) .+ ( F ` ( G ` ( m + 1 ) ) ) ) )
269 fveq2 
 |-  ( n = ( m + 1 ) -> ( H ` n ) = ( H ` ( m + 1 ) ) )
270 2fveq3 
 |-  ( n = ( m + 1 ) -> ( F ` ( G ` n ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
271 269 270 eqeq12d 
 |-  ( n = ( m + 1 ) -> ( ( H ` n ) = ( F ` ( G ` n ) ) <-> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) )
272 271 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ph -> ( H ` n ) = ( F ` ( G ` n ) ) ) <-> ( ph -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) ) )
273 272 136 vtoclga 
 |-  ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( ph -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) )
274 273 impcom 
 |-  ( ( ph /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
275 274 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
276 275 oveq2d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( H ` ( m + 1 ) ) ) = ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( F ` ( G ` ( m + 1 ) ) ) ) )
277 93 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> M e. ZZ )
278 178 zcnd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( m + 1 ) ) e. CC )
279 ax-1cn 
 |-  1 e. CC
280 npcan 
 |-  ( ( ( G ` ( m + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
281 278 279 280 sylancl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
282 uztrn 
 |-  ( ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) /\ ( G ` m ) e. ( ZZ>= ` M ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) )
283 186 164 282 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) )
284 eluzp1p1 
 |-  ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
285 283 284 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
286 281 285 eqeltrrd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` ( M + 1 ) ) )
287 seqm1 
 |-  ( ( M e. ZZ /\ ( G ` ( m + 1 ) ) e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( ( seq M ( .+ , F ) ` ( ( G ` ( m + 1 ) ) - 1 ) ) .+ ( F ` ( G ` ( m + 1 ) ) ) ) )
288 277 286 287 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( ( seq M ( .+ , F ) ` ( ( G ` ( m + 1 ) ) - 1 ) ) .+ ( F ` ( G ` ( m + 1 ) ) ) ) )
289 268 276 288 3eqtr4rd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( H ` ( m + 1 ) ) ) )
290 seqp1 
 |-  ( m e. ( ZZ>= ` 1 ) -> ( seq 1 ( .+ , H ) ` ( m + 1 ) ) = ( ( seq 1 ( .+ , H ) ` m ) .+ ( H ` ( m + 1 ) ) ) )
291 148 290 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( seq 1 ( .+ , H ) ` ( m + 1 ) ) = ( ( seq 1 ( .+ , H ) ` m ) .+ ( H ` ( m + 1 ) ) ) )
292 289 291 eqeq12d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) <-> ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( H ` ( m + 1 ) ) ) = ( ( seq 1 ( .+ , H ) ` m ) .+ ( H ` ( m + 1 ) ) ) ) )
293 159 292 syl5ibr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) )
294 293 ex 
 |-  ( ( ph /\ m e. NN ) -> ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) )
295 294 a2d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) -> ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) )
296 158 295 syld 
 |-  ( ( ph /\ m e. NN ) -> ( ( m e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) -> ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) )
297 296 expcom 
 |-  ( m e. NN -> ( ph -> ( ( m e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) -> ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) ) )
298 297 a2d 
 |-  ( m e. NN -> ( ( ph -> ( m e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) ) -> ( ph -> ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) ) )
299 18 24 30 36 145 298 nnind 
 |-  ( N e. NN -> ( ph -> ( N e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) ) )
300 12 299 mpcom 
 |-  ( ph -> ( N e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) )
301 6 300 mpd 
 |-  ( ph -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) )