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 227 elfzelzd
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( `' G ` k ) e. ZZ )
229 btwnnz
 |-  ( ( m e. ZZ /\ m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ )
230 229 3expib
 |-  ( m e. ZZ -> ( ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ ) )
231 230 con2d
 |-  ( m e. ZZ -> ( ( `' G ` k ) e. ZZ -> -. ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) ) )
232 224 228 231 sylc
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> -. ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) )
233 5 ad2antrr
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
234 156 adantrr
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> m e. ( 1 ... ( # ` A ) ) )
235 isorel
 |-  ( ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) /\ ( m e. ( 1 ... ( # ` A ) ) /\ ( `' G ` k ) e. ( 1 ... ( # ` A ) ) ) ) -> ( m < ( `' G ` k ) <-> ( G ` m ) < ( G ` ( `' G ` k ) ) ) )
236 233 234 227 235 syl12anc
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( G ` m ) < ( G ` ( `' G ` k ) ) ) )
237 38 ad2antrr
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> G : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
238 237 226 114 syl2anc
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( G ` ( `' G ` k ) ) = k )
239 238 breq2d
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( G ` m ) < ( G ` ( `' G ` k ) ) <-> ( G ` m ) < k ) )
240 174 adantrr
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( G ` m ) e. ZZ )
241 7 ad2antrr
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> A C_ ( ZZ>= ` M ) )
242 241 226 sseldd
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> k e. ( ZZ>= ` M ) )
243 eluzelz
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
244 242 243 syl
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> k e. ZZ )
245 zltp1le
 |-  ( ( ( G ` m ) e. ZZ /\ k e. ZZ ) -> ( ( G ` m ) < k <-> ( ( G ` m ) + 1 ) <_ k ) )
246 240 244 245 syl2anc
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( G ` m ) < k <-> ( ( G ` m ) + 1 ) <_ k ) )
247 236 239 246 3bitrd
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( ( G ` m ) + 1 ) <_ k ) )
248 169 adantrr
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( m + 1 ) e. ( 1 ... ( # ` A ) ) )
249 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 ) ) ) )
250 233 227 248 249 syl12anc
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( `' G ` k ) < ( m + 1 ) <-> ( G ` ( `' G ` k ) ) < ( G ` ( m + 1 ) ) ) )
251 238 breq1d
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( G ` ( `' G ` k ) ) < ( G ` ( m + 1 ) ) <-> k < ( G ` ( m + 1 ) ) ) )
252 178 adantrr
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( G ` ( m + 1 ) ) e. ZZ )
253 zltlem1
 |-  ( ( k e. ZZ /\ ( G ` ( m + 1 ) ) e. ZZ ) -> ( k < ( G ` ( m + 1 ) ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
254 244 252 253 syl2anc
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( k < ( G ` ( m + 1 ) ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
255 250 251 254 3bitrd
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> ( ( `' G ` k ) < ( m + 1 ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
256 247 255 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 ) ) ) )
257 232 256 mtbid
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) /\ k e. A ) ) -> -. ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
258 257 expr
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( k e. A -> -. ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) ) )
259 258 con2d
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) -> -. k e. A ) )
260 elfzle1
 |-  ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` m ) + 1 ) <_ k )
261 elfzle2
 |-  ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k <_ ( ( G ` ( m + 1 ) ) - 1 ) )
262 260 261 jca
 |-  ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
263 259 262 impel
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> -. k e. A )
264 223 263 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 ) )
265 213 264 9 syl2anc
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ( F ` k ) = Z )
266 160 164 186 212 265 seqid2
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq M ( .+ , F ) ` ( ( G ` ( m + 1 ) ) - 1 ) ) )
267 266 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 ) ) ) ) )
268 fveq2
 |-  ( n = ( m + 1 ) -> ( H ` n ) = ( H ` ( m + 1 ) ) )
269 2fveq3
 |-  ( n = ( m + 1 ) -> ( F ` ( G ` n ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
270 268 269 eqeq12d
 |-  ( n = ( m + 1 ) -> ( ( H ` n ) = ( F ` ( G ` n ) ) <-> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) )
271 270 imbi2d
 |-  ( n = ( m + 1 ) -> ( ( ph -> ( H ` n ) = ( F ` ( G ` n ) ) ) <-> ( ph -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) ) )
272 271 136 vtoclga
 |-  ( ( m + 1 ) e. ( 1 ... ( # ` A ) ) -> ( ph -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) )
273 272 impcom
 |-  ( ( ph /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
274 273 adantlr
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
275 274 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 ) ) ) ) )
276 93 ad2antrr
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> M e. ZZ )
277 178 zcnd
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( m + 1 ) ) e. CC )
278 ax-1cn
 |-  1 e. CC
279 npcan
 |-  ( ( ( G ` ( m + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
280 277 278 279 sylancl
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
281 uztrn
 |-  ( ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) /\ ( G ` m ) e. ( ZZ>= ` M ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) )
282 186 164 281 syl2anc
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) )
283 eluzp1p1
 |-  ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
284 282 283 syl
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
285 280 284 eqeltrrd
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` ( M + 1 ) ) )
286 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 ) ) ) ) )
287 276 285 286 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 ) ) ) ) )
288 267 275 287 3eqtr4rd
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( H ` ( m + 1 ) ) ) )
289 seqp1
 |-  ( m e. ( ZZ>= ` 1 ) -> ( seq 1 ( .+ , H ) ` ( m + 1 ) ) = ( ( seq 1 ( .+ , H ) ` m ) .+ ( H ` ( m + 1 ) ) ) )
290 148 289 syl
 |-  ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( seq 1 ( .+ , H ) ` ( m + 1 ) ) = ( ( seq 1 ( .+ , H ) ` m ) .+ ( H ` ( m + 1 ) ) ) )
291 288 290 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 ) ) ) ) )
292 159 291 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 ) ) ) )
293 292 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 ) ) ) ) )
294 293 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 ) ) ) ) )
295 158 294 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 ) ) ) ) )
296 295 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 ) ) ) ) ) )
297 296 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 ) ) ) ) ) )
298 18 24 30 36 145 297 nnind
 |-  ( N e. NN -> ( ph -> ( N e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) ) )
299 12 298 mpcom
 |-  ( ph -> ( N e. ( 1 ... ( # ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) )
300 6 299 mpd
 |-  ( ph -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) )