Metamath Proof Explorer

Theorem seqhomo

Description: Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqhomo.1 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqhomo.2 
|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
seqhomo.3 
|- ( ph -> N e. ( ZZ>= ` M ) )
seqhomo.4 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( H ` ( x .+ y ) ) = ( ( H ` x ) Q ( H ` y ) ) )
seqhomo.5 
|- ( ( ph /\ x e. ( M ... N ) ) -> ( H ` ( F ` x ) ) = ( G ` x ) )
Assertion seqhomo 
|- ( ph -> ( H ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , G ) ` N ) )

Proof

Step Hyp Ref Expression
1 seqhomo.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqhomo.2 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
3 seqhomo.3 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
4 seqhomo.4 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( H ` ( x .+ y ) ) = ( ( H ` x ) Q ( H ` y ) ) )
5 seqhomo.5 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( H ` ( F ` x ) ) = ( G ` x ) )
6 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
7 3 6 syl 
 |-  ( ph -> N e. ( M ... N ) )
8 eleq1 
 |-  ( x = M -> ( x e. ( M ... N ) <-> M e. ( M ... N ) ) )
9 2fveq3 
 |-  ( x = M -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( H ` ( seq M ( .+ , F ) ` M ) ) )
10 fveq2 
 |-  ( x = M -> ( seq M ( Q , G ) ` x ) = ( seq M ( Q , G ) ` M ) )
11 9 10 eqeq12d 
 |-  ( x = M -> ( ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) <-> ( H ` ( seq M ( .+ , F ) ` M ) ) = ( seq M ( Q , G ) ` M ) ) )
12 8 11 imbi12d 
 |-  ( x = M -> ( ( x e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) ) <-> ( M e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` M ) ) = ( seq M ( Q , G ) ` M ) ) ) )
13 12 imbi2d 
 |-  ( x = M -> ( ( ph -> ( x e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) ) ) <-> ( ph -> ( M e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` M ) ) = ( seq M ( Q , G ) ` M ) ) ) ) )
14 eleq1 
 |-  ( x = n -> ( x e. ( M ... N ) <-> n e. ( M ... N ) ) )
15 2fveq3 
 |-  ( x = n -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( H ` ( seq M ( .+ , F ) ` n ) ) )
16 fveq2 
 |-  ( x = n -> ( seq M ( Q , G ) ` x ) = ( seq M ( Q , G ) ` n ) )
17 15 16 eqeq12d 
 |-  ( x = n -> ( ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) <-> ( H ` ( seq M ( .+ , F ) ` n ) ) = ( seq M ( Q , G ) ` n ) ) )
18 14 17 imbi12d 
 |-  ( x = n -> ( ( x e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) ) <-> ( n e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` n ) ) = ( seq M ( Q , G ) ` n ) ) ) )
19 18 imbi2d 
 |-  ( x = n -> ( ( ph -> ( x e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) ) ) <-> ( ph -> ( n e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` n ) ) = ( seq M ( Q , G ) ` n ) ) ) ) )
20 eleq1 
 |-  ( x = ( n + 1 ) -> ( x e. ( M ... N ) <-> ( n + 1 ) e. ( M ... N ) ) )
21 2fveq3 
 |-  ( x = ( n + 1 ) -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( H ` ( seq M ( .+ , F ) ` ( n + 1 ) ) ) )
22 fveq2 
 |-  ( x = ( n + 1 ) -> ( seq M ( Q , G ) ` x ) = ( seq M ( Q , G ) ` ( n + 1 ) ) )
23 21 22 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) <-> ( H ` ( seq M ( .+ , F ) ` ( n + 1 ) ) ) = ( seq M ( Q , G ) ` ( n + 1 ) ) ) )
24 20 23 imbi12d 
 |-  ( x = ( n + 1 ) -> ( ( x e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) ) <-> ( ( n + 1 ) e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` ( n + 1 ) ) ) = ( seq M ( Q , G ) ` ( n + 1 ) ) ) ) )
25 24 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( x e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` ( n + 1 ) ) ) = ( seq M ( Q , G ) ` ( n + 1 ) ) ) ) ) )
26 eleq1 
 |-  ( x = N -> ( x e. ( M ... N ) <-> N e. ( M ... N ) ) )
27 2fveq3 
 |-  ( x = N -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( H ` ( seq M ( .+ , F ) ` N ) ) )
28 fveq2 
 |-  ( x = N -> ( seq M ( Q , G ) ` x ) = ( seq M ( Q , G ) ` N ) )
29 27 28 eqeq12d 
 |-  ( x = N -> ( ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) <-> ( H ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , G ) ` N ) ) )
30 26 29 imbi12d 
 |-  ( x = N -> ( ( x e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) ) <-> ( N e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , G ) ` N ) ) ) )
31 30 imbi2d 
 |-  ( x = N -> ( ( ph -> ( x e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` x ) ) = ( seq M ( Q , G ) ` x ) ) ) <-> ( ph -> ( N e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , G ) ` N ) ) ) ) )
32 2fveq3 
 |-  ( x = M -> ( H ` ( F ` x ) ) = ( H ` ( F ` M ) ) )
33 fveq2 
 |-  ( x = M -> ( G ` x ) = ( G ` M ) )
34 32 33 eqeq12d 
 |-  ( x = M -> ( ( H ` ( F ` x ) ) = ( G ` x ) <-> ( H ` ( F ` M ) ) = ( G ` M ) ) )
35 5 ralrimiva 
 |-  ( ph -> A. x e. ( M ... N ) ( H ` ( F ` x ) ) = ( G ` x ) )
36 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
37 3 36 syl 
 |-  ( ph -> M e. ( M ... N ) )
38 34 35 37 rspcdva 
 |-  ( ph -> ( H ` ( F ` M ) ) = ( G ` M ) )
39 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
40 seq1 
 |-  ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
41 3 39 40 3syl 
 |-  ( ph -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
42 41 fveq2d 
 |-  ( ph -> ( H ` ( seq M ( .+ , F ) ` M ) ) = ( H ` ( F ` M ) ) )
43 seq1 
 |-  ( M e. ZZ -> ( seq M ( Q , G ) ` M ) = ( G ` M ) )
44 3 39 43 3syl 
 |-  ( ph -> ( seq M ( Q , G ) ` M ) = ( G ` M ) )
45 38 42 44 3eqtr4d 
 |-  ( ph -> ( H ` ( seq M ( .+ , F ) ` M ) ) = ( seq M ( Q , G ) ` M ) )
46 45 a1d 
 |-  ( ph -> ( M e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` M ) ) = ( seq M ( Q , G ) ` M ) ) )
47 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) -> n e. ( M ... N ) )
48 47 adantl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( M ... N ) )
49 48 expr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n + 1 ) e. ( M ... N ) -> n e. ( M ... N ) ) )
50 49 imim1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` n ) ) = ( seq M ( Q , G ) ` n ) ) -> ( ( n + 1 ) e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` n ) ) = ( seq M ( Q , G ) ` n ) ) ) )
51 oveq1 
 |-  ( ( H ` ( seq M ( .+ , F ) ` n ) ) = ( seq M ( Q , G ) ` n ) -> ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( G ` ( n + 1 ) ) ) = ( ( seq M ( Q , G ) ` n ) Q ( G ` ( n + 1 ) ) ) )
52 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
53 52 ad2antrl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
54 53 fveq2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( H ` ( seq M ( .+ , F ) ` ( n + 1 ) ) ) = ( H ` ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) )
55 4 ralrimivva 
 |-  ( ph -> A. x e. S A. y e. S ( H ` ( x .+ y ) ) = ( ( H ` x ) Q ( H ` y ) ) )
56 55 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> A. x e. S A. y e. S ( H ` ( x .+ y ) ) = ( ( H ` x ) Q ( H ` y ) ) )
57 simprl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( ZZ>= ` M ) )
58 elfzuz3 
 |-  ( n e. ( M ... N ) -> N e. ( ZZ>= ` n ) )
59 fzss2 
 |-  ( N e. ( ZZ>= ` n ) -> ( M ... n ) C_ ( M ... N ) )
60 48 58 59 3syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( M ... n ) C_ ( M ... N ) )
61 60 sselda 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) /\ x e. ( M ... n ) ) -> x e. ( M ... N ) )
62 2 adantlr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
63 61 62 syldan 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) /\ x e. ( M ... n ) ) -> ( F ` x ) e. S )
64 1 adantlr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
65 57 63 64 seqcl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( seq M ( .+ , F ) ` n ) e. S )
66 fveq2 
 |-  ( x = ( n + 1 ) -> ( F ` x ) = ( F ` ( n + 1 ) ) )
67 66 eleq1d 
 |-  ( x = ( n + 1 ) -> ( ( F ` x ) e. S <-> ( F ` ( n + 1 ) ) e. S ) )
68 2 ralrimiva 
 |-  ( ph -> A. x e. ( M ... N ) ( F ` x ) e. S )
69 68 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> A. x e. ( M ... N ) ( F ` x ) e. S )
70 simprr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( n + 1 ) e. ( M ... N ) )
71 67 69 70 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` ( n + 1 ) ) e. S )
72 fvoveq1 
 |-  ( x = ( seq M ( .+ , F ) ` n ) -> ( H ` ( x .+ y ) ) = ( H ` ( ( seq M ( .+ , F ) ` n ) .+ y ) ) )
73 fveq2 
 |-  ( x = ( seq M ( .+ , F ) ` n ) -> ( H ` x ) = ( H ` ( seq M ( .+ , F ) ` n ) ) )
74 73 oveq1d 
 |-  ( x = ( seq M ( .+ , F ) ` n ) -> ( ( H ` x ) Q ( H ` y ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` y ) ) )
75 72 74 eqeq12d 
 |-  ( x = ( seq M ( .+ , F ) ` n ) -> ( ( H ` ( x .+ y ) ) = ( ( H ` x ) Q ( H ` y ) ) <-> ( H ` ( ( seq M ( .+ , F ) ` n ) .+ y ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` y ) ) ) )
76 oveq2 
 |-  ( y = ( F ` ( n + 1 ) ) -> ( ( seq M ( .+ , F ) ` n ) .+ y ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
77 76 fveq2d 
 |-  ( y = ( F ` ( n + 1 ) ) -> ( H ` ( ( seq M ( .+ , F ) ` n ) .+ y ) ) = ( H ` ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) )
78 fveq2 
 |-  ( y = ( F ` ( n + 1 ) ) -> ( H ` y ) = ( H ` ( F ` ( n + 1 ) ) ) )
79 78 oveq2d 
 |-  ( y = ( F ` ( n + 1 ) ) -> ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` y ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` ( F ` ( n + 1 ) ) ) ) )
80 77 79 eqeq12d 
 |-  ( y = ( F ` ( n + 1 ) ) -> ( ( H ` ( ( seq M ( .+ , F ) ` n ) .+ y ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` y ) ) <-> ( H ` ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` ( F ` ( n + 1 ) ) ) ) ) )
81 75 80 rspc2v 
 |-  ( ( ( seq M ( .+ , F ) ` n ) e. S /\ ( F ` ( n + 1 ) ) e. S ) -> ( A. x e. S A. y e. S ( H ` ( x .+ y ) ) = ( ( H ` x ) Q ( H ` y ) ) -> ( H ` ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` ( F ` ( n + 1 ) ) ) ) ) )
82 65 71 81 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( A. x e. S A. y e. S ( H ` ( x .+ y ) ) = ( ( H ` x ) Q ( H ` y ) ) -> ( H ` ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` ( F ` ( n + 1 ) ) ) ) ) )
83 56 82 mpd 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( H ` ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` ( F ` ( n + 1 ) ) ) ) )
84 2fveq3 
 |-  ( x = ( n + 1 ) -> ( H ` ( F ` x ) ) = ( H ` ( F ` ( n + 1 ) ) ) )
85 fveq2 
 |-  ( x = ( n + 1 ) -> ( G ` x ) = ( G ` ( n + 1 ) ) )
86 84 85 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( H ` ( F ` x ) ) = ( G ` x ) <-> ( H ` ( F ` ( n + 1 ) ) ) = ( G ` ( n + 1 ) ) ) )
87 35 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> A. x e. ( M ... N ) ( H ` ( F ` x ) ) = ( G ` x ) )
88 86 87 70 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( H ` ( F ` ( n + 1 ) ) ) = ( G ` ( n + 1 ) ) )
89 88 oveq2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( H ` ( F ` ( n + 1 ) ) ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( G ` ( n + 1 ) ) ) )
90 54 83 89 3eqtrd 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( H ` ( seq M ( .+ , F ) ` ( n + 1 ) ) ) = ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( G ` ( n + 1 ) ) ) )
91 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( Q , G ) ` ( n + 1 ) ) = ( ( seq M ( Q , G ) ` n ) Q ( G ` ( n + 1 ) ) ) )
92 91 ad2antrl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( seq M ( Q , G ) ` ( n + 1 ) ) = ( ( seq M ( Q , G ) ` n ) Q ( G ` ( n + 1 ) ) ) )
93 90 92 eqeq12d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( H ` ( seq M ( .+ , F ) ` ( n + 1 ) ) ) = ( seq M ( Q , G ) ` ( n + 1 ) ) <-> ( ( H ` ( seq M ( .+ , F ) ` n ) ) Q ( G ` ( n + 1 ) ) ) = ( ( seq M ( Q , G ) ` n ) Q ( G ` ( n + 1 ) ) ) ) )
94 51 93 imbitrrid 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( H ` ( seq M ( .+ , F ) ` n ) ) = ( seq M ( Q , G ) ` n ) -> ( H ` ( seq M ( .+ , F ) ` ( n + 1 ) ) ) = ( seq M ( Q , G ) ` ( n + 1 ) ) ) )
95 50 94 animpimp2impd 
 |-  ( n e. ( ZZ>= ` M ) -> ( ( ph -> ( n e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` n ) ) = ( seq M ( Q , G ) ` n ) ) ) -> ( ph -> ( ( n + 1 ) e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` ( n + 1 ) ) ) = ( seq M ( Q , G ) ` ( n + 1 ) ) ) ) ) )
96 13 19 25 31 46 95 uzind4i 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( N e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , G ) ` N ) ) ) )
97 3 96 mpcom 
 |-  ( ph -> ( N e. ( M ... N ) -> ( H ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , G ) ` N ) ) )
98 7 97 mpd 
 |-  ( ph -> ( H ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , G ) ` N ) )