# 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
seqhomo.2 ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to {F}\left({x}\right)\in {S}$
seqhomo.3 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
seqhomo.4
seqhomo.5 ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to {H}\left({F}\left({x}\right)\right)={G}\left({x}\right)$
Assertion seqhomo

### Proof

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