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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
seqhomo.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqhomo.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐻 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐻 ‘ 𝑥 ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) )
seqhomo.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) )
Assertion seqhomo ( 𝜑 → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 seqhomo.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 seqhomo.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
3 seqhomo.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4 seqhomo.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐻 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐻 ‘ 𝑥 ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) )
5 seqhomo.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) )
6 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
7 3 6 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
8 eleq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) )
9 2fveq3 ⊢ ( 𝑥 = 𝑀 → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) )
10 fveq2 ⊢ ( 𝑥 = 𝑀 → ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑀 ) )
11 9 10 eqeq12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ↔ ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑀 ) ) )
12 8 11 imbi12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ) ↔ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑀 ) ) ) )
13 12 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑀 ) ) ) ) )
14 eleq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
15 2fveq3 ⊢ ( 𝑥 = 𝑛 → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
16 fveq2 ⊢ ( 𝑥 = 𝑛 → ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) )
17 15 16 eqeq12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ↔ ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) ) )
18 14 17 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) ) ) )
19 18 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) ) ) ) )
20 eleq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
21 2fveq3 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
22 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ ( 𝑛 + 1 ) ) )
23 21 22 eqeq12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ↔ ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) )
24 20 23 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) )
25 24 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
26 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) )
27 2fveq3 ⊢ ( 𝑥 = 𝑁 → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
28 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑁 ) )
29 27 28 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ↔ ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑁 ) ) )
30 26 29 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ) ↔ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑁 ) ) ) )
31 30 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑁 ) ) ) ) )
32 2fveq3 ⊢ ( 𝑥 = 𝑀 → ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑀 ) ) )
33 fveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑀 ) )
34 32 33 eqeq12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐻 ‘ ( 𝐹 ‘ 𝑀 ) ) = ( 𝐺 ‘ 𝑀 ) ) )
35 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) )
36 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
37 3 36 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
38 34 35 37 rspcdva ⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝐹 ‘ 𝑀 ) ) = ( 𝐺 ‘ 𝑀 ) )
39 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
40 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
41 3 39 40 3syl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
42 41 fveq2d ⊢ ( 𝜑 → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑀 ) ) )
43 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) )
44 3 39 43 3syl ⊢ ( 𝜑 → ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) )
45 38 42 44 3eqtr4d ⊢ ( 𝜑 → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑀 ) )
46 45 a1d ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑀 ) ) )
47 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
48 47 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
49 48 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
50 49 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) ) ) )
51 oveq1 ⊢ ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) → ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
52 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
53 52 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
54 53 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
55 4 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝐻 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐻 ‘ 𝑥 ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) )
56 55 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝐻 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐻 ‘ 𝑥 ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) )
57 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
58 elfzuz3 ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) )
59 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) → ( 𝑀 ... 𝑛 ) ⊆ ( 𝑀 ... 𝑁 ) )
60 48 58 59 3syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑀 ... 𝑛 ) ⊆ ( 𝑀 ... 𝑁 ) )
61 60 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
62 2 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
63 61 62 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
64 1 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
65 57 63 64 seqcl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝑆 )
66 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
67 66 eleq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑆 ) )
68 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
69 68 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ∀ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
70 simprr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
71 67 69 70 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑆 )
72 fvoveq1 ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) → ( 𝐻 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + 𝑦 ) ) )
73 fveq2 ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
74 73 oveq1d ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) → ( ( 𝐻 ‘ 𝑥 ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) )
75 72 74 eqeq12d ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) → ( ( 𝐻 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐻 ‘ 𝑥 ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + 𝑦 ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) ) )
76 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ ( 𝑛 + 1 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + 𝑦 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
77 76 fveq2d ⊢ ( 𝑦 = ( 𝐹 ‘ ( 𝑛 + 1 ) ) → ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + 𝑦 ) ) = ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
78 fveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ ( 𝑛 + 1 ) ) → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
79 78 oveq2d ⊢ ( 𝑦 = ( 𝐹 ‘ ( 𝑛 + 1 ) ) → ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
80 77 79 eqeq12d ⊢ ( 𝑦 = ( 𝐹 ‘ ( 𝑛 + 1 ) ) → ( ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + 𝑦 ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
81 75 80 rspc2v ⊢ ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝑆 ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝐻 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐻 ‘ 𝑥 ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) → ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
82 65 71 81 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝐻 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐻 ‘ 𝑥 ) 𝑄 ( 𝐻 ‘ 𝑦 ) ) → ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
83 56 82 mpd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐻 ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
84 2fveq3 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
85 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝑛 + 1 ) ) )
86 84 85 eqeq12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
87 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ∀ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) )
88 86 87 70 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( 𝐺 ‘ ( 𝑛 + 1 ) ) )
89 88 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐻 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
90 54 83 89 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
91 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
92 91 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
93 90 92 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ↔ ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
94 51 93 imbitrrid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) )
95 50 94 animpimp2impd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑛 ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
96 13 19 25 31 46 95 uzind4i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑁 ) ) ) )
97 3 96 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑁 ) ) )
98 7 97 mpd ⊢ ( 𝜑 → ( 𝐻 ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( 𝑄 , 𝐺 ) ‘ 𝑁 ) )