Theorem seqhomog 10719

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

Hypotheses

Ref	Expression
seqhomo.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
seqhomo.2	⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)
seqhomo.3	⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
seqhomo.4	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)))
seqhomo.5	⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥))
seqhomog.f	⊢ (𝜑 → 𝐹 ∈ 𝑉)
seqhomog.g	⊢ (𝜑 → 𝐺 ∈ 𝑊)
seqhomog.p	⊢ (𝜑 → + ∈ 𝑋)
seqhomog.q	⊢ (𝜑 → 𝑄 ∈ 𝑌)

Assertion

Ref	Expression
seqhomog	⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))

Distinct variable groups:   𝑥,𝑦,𝐹   𝑥,𝐻,𝑦   𝑥,𝑀,𝑦   𝑥,𝑁,𝑦   𝜑,𝑥,𝑦   𝑥,𝐺   𝑥, + ,𝑦   𝑥,𝑄,𝑦   𝑥,𝑆,𝑦

Allowed substitution hints:   𝐺(𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)   𝑋(𝑥,𝑦)   𝑌(𝑥,𝑦)

Proof of Theorem seqhomog

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		seqhomo.3	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
2		eluzfz2 10196	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
3	1, 2	syl 14	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
4		eleq1 2272	. . . . . 6 ⊢ (𝑥 = 𝑀 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁)))
5		2fveq3 5608	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)))
6		fveq2 5603	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (seq𝑀(𝑄, 𝐺)‘𝑥) = (seq𝑀(𝑄, 𝐺)‘𝑀))
7	5, 6	eqeq12d 2224	. . . . . 6 ⊢ (𝑥 = 𝑀 → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥) ↔ (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀)))
8	4, 7	imbi12d 234	. . . . 5 ⊢ (𝑥 = 𝑀 → ((𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥)) ↔ (𝑀 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀))))
9	8	imbi2d 230	. . . 4 ⊢ (𝑥 = 𝑀 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥))) ↔ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀)))))
10		eleq1 2272	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁)))
11		2fveq3 5608	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)))
12		fveq2 5603	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq𝑀(𝑄, 𝐺)‘𝑥) = (seq𝑀(𝑄, 𝐺)‘𝑛))
13	11, 12	eqeq12d 2224	. . . . . 6 ⊢ (𝑥 = 𝑛 → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥) ↔ (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛)))
14	10, 13	imbi12d 234	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥)) ↔ (𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛))))
15	14	imbi2d 230	. . . 4 ⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥))) ↔ (𝜑 → (𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛)))))
16		eleq1 2272	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝑀...𝑁) ↔ (𝑛 + 1) ∈ (𝑀...𝑁)))
17		2fveq3 5608	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))))
18		fveq2 5603	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (seq𝑀(𝑄, 𝐺)‘𝑥) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)))
19	17, 18	eqeq12d 2224	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥) ↔ (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1))))
20	16, 19	imbi12d 234	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥)) ↔ ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)))))
21	20	imbi2d 230	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1))))))
22		eleq1 2272	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁)))
23		2fveq3 5608	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)))
24		fveq2 5603	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (seq𝑀(𝑄, 𝐺)‘𝑥) = (seq𝑀(𝑄, 𝐺)‘𝑁))
25	23, 24	eqeq12d 2224	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥) ↔ (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)))
26	22, 25	imbi12d 234	. . . . 5 ⊢ (𝑥 = 𝑁 → ((𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥)) ↔ (𝑁 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))))
27	26	imbi2d 230	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑥)) = (seq𝑀(𝑄, 𝐺)‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)))))
28		2fveq3 5608	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → (𝐻‘(𝐹‘𝑥)) = (𝐻‘(𝐹‘𝑀)))
29		fveq2 5603	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → (𝐺‘𝑥) = (𝐺‘𝑀))
30	28, 29	eqeq12d 2224	. . . . . . 7 ⊢ (𝑥 = 𝑀 → ((𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) ↔ (𝐻‘(𝐹‘𝑀)) = (𝐺‘𝑀)))
31		seqhomo.5	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥))
32	31	ralrimiva 2583	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥))
33		eluzfz1 10195	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))
34	1, 33	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁))
35	30, 32, 34	rspcdva 2892	. . . . . 6 ⊢ (𝜑 → (𝐻‘(𝐹‘𝑀)) = (𝐺‘𝑀))
36		eluzel2 9695	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
37	1, 36	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
38		seqhomog.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
39		seqhomog.p	. . . . . . . 8 ⊢ (𝜑 → + ∈ 𝑋)
40		seq1g 10652	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ∧ + ∈ 𝑋) → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
41	37, 38, 39, 40	syl3anc 1252	. . . . . . 7 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
42	41	fveq2d 5607	. . . . . 6 ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (𝐻‘(𝐹‘𝑀)))
43		seqhomog.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ 𝑊)
44		seqhomog.q	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ 𝑌)
45		seq1g 10652	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝐺 ∈ 𝑊 ∧ 𝑄 ∈ 𝑌) → (seq𝑀(𝑄, 𝐺)‘𝑀) = (𝐺‘𝑀))
46	37, 43, 44, 45	syl3anc 1252	. . . . . 6 ⊢ (𝜑 → (seq𝑀(𝑄, 𝐺)‘𝑀) = (𝐺‘𝑀))
47	35, 42, 46	3eqtr4d 2252	. . . . 5 ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀))
48	47	a1d 22	. . . 4 ⊢ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑀)) = (seq𝑀(𝑄, 𝐺)‘𝑀)))
49		peano2fzr 10201	. . . . . . . 8 ⊢ ((𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁))
50	49	adantl 277	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (𝑀...𝑁))
51	50	expr 375	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑛 ∈ (𝑀...𝑁)))
52	51	imim1d 75	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛))))
53		oveq1 5981	. . . . . 6 ⊢ ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐺‘(𝑛 + 1))) = ((seq𝑀(𝑄, 𝐺)‘𝑛)𝑄(𝐺‘(𝑛 + 1))))
54		simprl 529	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (ℤ≥‘𝑀))
55	38	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝐹 ∈ 𝑉)
56	39	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → + ∈ 𝑋)
57		seqp1g 10655	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ℤ≥‘𝑀) ∧ 𝐹 ∈ 𝑉 ∧ + ∈ 𝑋) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
58	54, 55, 56, 57	syl3anc 1252	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq𝑀( + , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
59	58	fveq2d 5607	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
60		seqhomo.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)))
61	60	ralrimivva 2592	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)))
62	61	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)))
63		elfzuz3 10186	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑛))
64		fzss2 10228	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ≥‘𝑛) → (𝑀...𝑛) ⊆ (𝑀...𝑁))
65	50, 63, 64	3syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑀...𝑛) ⊆ (𝑀...𝑁))
66	65	sselda 3204	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ 𝑥 ∈ (𝑀...𝑛)) → 𝑥 ∈ (𝑀...𝑁))
67		seqhomo.2	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)
68	67	adantlr 477	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)
69	66, 68	syldan 282	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ 𝑥 ∈ (𝑀...𝑛)) → (𝐹‘𝑥) ∈ 𝑆)
70		seqhomo.1	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
71	70	adantlr 477	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
72	54, 69, 71, 55, 56	seqclg 10661	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ 𝑆)
73		fveq2 5603	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1)))
74	73	eleq1d 2278	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑆))
75	67	ralrimiva 2583	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ 𝑆)
76	75	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ 𝑆)
77		simprr 531	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑛 + 1) ∈ (𝑀...𝑁))
78	74, 76, 77	rspcdva 2892	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘(𝑛 + 1)) ∈ 𝑆)
79		fvoveq1 5997	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) → (𝐻‘(𝑥 + 𝑦)) = (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + 𝑦)))
80		fveq2 5603	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) → (𝐻‘𝑥) = (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)))
81	80	oveq1d 5989	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) → ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘𝑦)))
82	79, 81	eqeq12d 2224	. . . . . . . . . . 11 ⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) → ((𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) ↔ (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + 𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘𝑦))))
83		oveq2 5982	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((seq𝑀( + , 𝐹)‘𝑛) + 𝑦) = ((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
84	83	fveq2d 5607	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + 𝑦)) = (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
85		fveq2 5603	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → (𝐻‘𝑦) = (𝐻‘(𝐹‘(𝑛 + 1))))
86	85	oveq2d 5990	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))))
87	84, 86	eqeq12d 2224	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘(𝑛 + 1)) → ((𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + 𝑦)) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘𝑦)) ↔ (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1))))))
88	82, 87	rspc2v 2900	. . . . . . . . . 10 ⊢ (((seq𝑀( + , 𝐹)‘𝑛) ∈ 𝑆 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) → (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1))))))
89	72, 78, 88	syl2anc 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)) → (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1))))))
90	62, 89	mpd 13	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐻‘((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))))
91		2fveq3 5608	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (𝐻‘(𝐹‘𝑥)) = (𝐻‘(𝐹‘(𝑛 + 1))))
92		fveq2 5603	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (𝐺‘𝑥) = (𝐺‘(𝑛 + 1)))
93	91, 92	eqeq12d 2224	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥) ↔ (𝐻‘(𝐹‘(𝑛 + 1))) = (𝐺‘(𝑛 + 1))))
94	32	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑥 ∈ (𝑀...𝑁)(𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥))
95	93, 94, 77	rspcdva 2892	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐻‘(𝐹‘(𝑛 + 1))) = (𝐺‘(𝑛 + 1)))
96	95	oveq2d 5990	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐻‘(𝐹‘(𝑛 + 1)))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐺‘(𝑛 + 1))))
97	59, 90, 96	3eqtrd 2246	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐺‘(𝑛 + 1))))
98	43	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝐺 ∈ 𝑊)
99	44	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑄 ∈ 𝑌)
100		seqp1g 10655	. . . . . . . 8 ⊢ ((𝑛 ∈ (ℤ≥‘𝑀) ∧ 𝐺 ∈ 𝑊 ∧ 𝑄 ∈ 𝑌) → (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)) = ((seq𝑀(𝑄, 𝐺)‘𝑛)𝑄(𝐺‘(𝑛 + 1))))
101	54, 98, 99, 100	syl3anc 1252	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)) = ((seq𝑀(𝑄, 𝐺)‘𝑛)𝑄(𝐺‘(𝑛 + 1))))
102	97, 101	eqeq12d 2224	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1)) ↔ ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛))𝑄(𝐺‘(𝑛 + 1))) = ((seq𝑀(𝑄, 𝐺)‘𝑛)𝑄(𝐺‘(𝑛 + 1)))))
103	53, 102	imbitrrid 156	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1))))
104	52, 103	animpimp2impd 559	. . . 4 ⊢ (𝑛 ∈ (ℤ≥‘𝑀) → ((𝜑 → (𝑛 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑛)) = (seq𝑀(𝑄, 𝐺)‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘(𝑛 + 1))) = (seq𝑀(𝑄, 𝐺)‘(𝑛 + 1))))))
105	9, 15, 21, 27, 48, 104	uzind4i 9755	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))))
106	1, 105	mpcom 36	. 2 ⊢ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)))
107	3, 106	mpd 13	1 ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1375   ∈ wcel 2180  ∀wral 2488   ⊆ wss 3177  ‘cfv 5294  (class class class)co 5974  1c1 7968   + caddc 7970  ℤcz 9414  ℤ_≥cuz 9690  ...cfz 10172  seqcseq 10636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-coll 4178  ax-sep 4181  ax-nul 4189  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-setind 4606  ax-iinf 4657  ax-cnex 8058  ax-resscn 8059  ax-1cn 8060  ax-1re 8061  ax-icn 8062  ax-addcl 8063  ax-addrcl 8064  ax-mulcl 8065  ax-addcom 8067  ax-addass 8069  ax-distr 8071  ax-i2m1 8072  ax-0lt1 8073  ax-0id 8075  ax-rnegex 8076  ax-cnre 8078  ax-pre-ltirr 8079  ax-pre-ltwlin 8080  ax-pre-lttrn 8081  ax-pre-ltadd 8083

This theorem depends on definitions:  df-bi 117  df-3or 984  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-nel 2476  df-ral 2493  df-rex 2494  df-reu 2495  df-rab 2497  df-v 2781  df-sbc 3009  df-csb 3105  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-nul 3472  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-int 3903  df-iun 3946  df-br 4063  df-opab 4125  df-mpt 4126  df-tr 4162  df-id 4361  df-iord 4434  df-on 4436  df-ilim 4437  df-suc 4439  df-iom 4660  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-f1 5299  df-fo 5300  df-f1o 5301  df-fv 5302  df-riota 5927  df-ov 5977  df-oprab 5978  df-mpo 5979  df-1st 6256  df-2nd 6257  df-recs 6421  df-frec 6507  df-pnf 8151  df-mnf 8152  df-xr 8153  df-ltxr 8154  df-le 8155  df-sub 8287  df-neg 8288  df-inn 9079  df-n0 9338  df-z 9415  df-uz 9691  df-fz 10173  df-fzo 10307  df-seqfrec 10637

This theorem is referenced by:  gsumwmhm  13497  gsumfzmhm  13846