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	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqhomo.2	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in S$
	seqhomo.3	$⊢ φ \to N \in ℤ_{\geq M}$
	seqhomo.4	$⊢ (φ \land (x \in S \land y \in S)) \to H (x \underset{˙}{+} y) = H (x) Q H (y)$
	seqhomo.5	$⊢ (φ \land x \in (M \dots N)) \to H (F (x)) = G (x)$
Assertion	seqhomo	$⊢ φ \to H (seq M (\underset{˙}{+}, F) (N)) = seq M (Q, G) (N)$

Proof

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

Metamath Proof Explorer

Theorem seqhomo

Proof