seqof

Description: Distribute function operation through a sequence. Note that G ( z ) is an implicit function on z . (Contributed by Mario Carneiro, 3-Mar-2015)

	Ref	Expression
Hypotheses	seqof.1	$⊢ φ \to A \in V$
	seqof.2	$⊢ φ \to N \in ℤ_{\geq M}$
	seqof.3	$⊢ (φ \land x \in (M \dots N)) \to F (x) = (z \in A ⟼ G (x))$
Assertion	seqof	$⊢ φ \to seq M (\circ_{f} \underset{˙}{+}, F) (N) = (z \in A ⟼ seq M (\underset{˙}{+}, G) (N))$

Proof

Step	Hyp	Ref	Expression
1		seqof.1	$⊢ φ \to A \in V$
2		seqof.2	$⊢ φ \to N \in ℤ_{\geq M}$
3		seqof.3	$⊢ (φ \land x \in (M \dots N)) \to F (x) = (z \in A ⟼ G (x))$
4		fvex	$⊢ G (x) \in V$
5	4	rgenw	$⊢ \forall z \in A G (x) \in V$
6		eqid	$⊢ (z \in A ⟼ G (x)) = (z \in A ⟼ G (x))$
7	6	fnmpt	$⊢ \forall z \in A G (x) \in V \to (z \in A ⟼ G (x)) Fn A$
8	5 7	mp1i	$⊢ (φ \land x \in (M \dots N)) \to (z \in A ⟼ G (x)) Fn A$
9	3	fneq1d	$⊢ (φ \land x \in (M \dots N)) \to (F (x) Fn A \leftrightarrow (z \in A ⟼ G (x)) Fn A)$
10	8 9	mpbird	$⊢ (φ \land x \in (M \dots N)) \to F (x) Fn A$
11		fvex	$⊢ F (x) \in V$
12		fneq1	$⊢ z = F (x) \to (z Fn A \leftrightarrow F (x) Fn A)$
13	11 12	elab	$⊢ F (x) \in \{z \| z Fn A\} \leftrightarrow F (x) Fn A$
14	10 13	sylibr	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in \{z \| z Fn A\}$
15		simprl	$⊢ (φ \land (x Fn A \land y Fn A)) \to x Fn A$
16		simprr	$⊢ (φ \land (x Fn A \land y Fn A)) \to y Fn A$
17	1	adantr	$⊢ (φ \land (x Fn A \land y Fn A)) \to A \in V$
18		inidm	$⊢ A \cap A = A$
19	15 16 17 17 18	offn	$⊢ (φ \land (x Fn A \land y Fn A)) \to (x {\underset{˙}{+}}_{f} y) Fn A$
20	19	ex	$⊢ φ \to ((x Fn A \land y Fn A) \to (x {\underset{˙}{+}}_{f} y) Fn A)$
21		vex	$⊢ x \in V$
22		fneq1	$⊢ z = x \to (z Fn A \leftrightarrow x Fn A)$
23	21 22	elab	$⊢ x \in \{z \| z Fn A\} \leftrightarrow x Fn A$
24		vex	$⊢ y \in V$
25		fneq1	$⊢ z = y \to (z Fn A \leftrightarrow y Fn A)$
26	24 25	elab	$⊢ y \in \{z \| z Fn A\} \leftrightarrow y Fn A$
27	23 26	anbi12i	$⊢ (x \in \{z \| z Fn A\} \land y \in \{z \| z Fn A\}) \leftrightarrow (x Fn A \land y Fn A)$
28		ovex	$⊢ x {\underset{˙}{+}}_{f} y \in V$
29		fneq1	$⊢ z = x {\underset{˙}{+}}_{f} y \to (z Fn A \leftrightarrow (x {\underset{˙}{+}}_{f} y) Fn A)$
30	28 29	elab	$⊢ x {\underset{˙}{+}}_{f} y \in \{z \| z Fn A\} \leftrightarrow (x {\underset{˙}{+}}_{f} y) Fn A$
31	20 27 30	3imtr4g	$⊢ φ \to ((x \in \{z \| z Fn A\} \land y \in \{z \| z Fn A\}) \to x {\underset{˙}{+}}_{f} y \in \{z \| z Fn A\})$
32	31	imp	$⊢ (φ \land (x \in \{z \| z Fn A\} \land y \in \{z \| z Fn A\})) \to x {\underset{˙}{+}}_{f} y \in \{z \| z Fn A\}$
33	2 14 32	seqcl	$⊢ φ \to seq M (\circ_{f} \underset{˙}{+}, F) (N) \in \{z \| z Fn A\}$
34		fvex	$⊢ seq M (\circ_{f} \underset{˙}{+}, F) (N) \in V$
35		fneq1	$⊢ z = seq M (\circ_{f} \underset{˙}{+}, F) (N) \to (z Fn A \leftrightarrow seq M (\circ_{f} \underset{˙}{+}, F) (N) Fn A)$
36	34 35	elab	$⊢ seq M (\circ_{f} \underset{˙}{+}, F) (N) \in \{z \| z Fn A\} \leftrightarrow seq M (\circ_{f} \underset{˙}{+}, F) (N) Fn A$
37	33 36	sylib	$⊢ φ \to seq M (\circ_{f} \underset{˙}{+}, F) (N) Fn A$
38		dffn5	$⊢ seq M (\circ_{f} \underset{˙}{+}, F) (N) Fn A \leftrightarrow seq M (\circ_{f} \underset{˙}{+}, F) (N) = (z \in A ⟼ seq M (\circ_{f} \underset{˙}{+}, F) (N) (z))$
39	37 38	sylib	$⊢ φ \to seq M (\circ_{f} \underset{˙}{+}, F) (N) = (z \in A ⟼ seq M (\circ_{f} \underset{˙}{+}, F) (N) (z))$
40		fveq1	$⊢ w = seq M (\circ_{f} \underset{˙}{+}, F) (N) \to w (z) = seq M (\circ_{f} \underset{˙}{+}, F) (N) (z)$
41		eqid	$⊢ (w \in V ⟼ w (z)) = (w \in V ⟼ w (z))$
42		fvex	$⊢ seq M (\circ_{f} \underset{˙}{+}, F) (N) (z) \in V$
43	40 41 42	fvmpt	$⊢ seq M (\circ_{f} \underset{˙}{+}, F) (N) \in V \to (w \in V ⟼ w (z)) (seq M (\circ_{f} \underset{˙}{+}, F) (N)) = seq M (\circ_{f} \underset{˙}{+}, F) (N) (z)$
44	34 43	mp1i	$⊢ (φ \land z \in A) \to (w \in V ⟼ w (z)) (seq M (\circ_{f} \underset{˙}{+}, F) (N)) = seq M (\circ_{f} \underset{˙}{+}, F) (N) (z)$
45	32	adantlr	$⊢ ((φ \land z \in A) \land (x \in \{z \| z Fn A\} \land y \in \{z \| z Fn A\})) \to x {\underset{˙}{+}}_{f} y \in \{z \| z Fn A\}$
46	14	adantlr	$⊢ ((φ \land z \in A) \land x \in (M \dots N)) \to F (x) \in \{z \| z Fn A\}$
47	2	adantr	$⊢ (φ \land z \in A) \to N \in ℤ_{\geq M}$
48		eqidd	$⊢ ((φ \land (x Fn A \land y Fn A)) \land z \in A) \to x (z) = x (z)$
49		eqidd	$⊢ ((φ \land (x Fn A \land y Fn A)) \land z \in A) \to y (z) = y (z)$
50	15 16 17 17 18 48 49	ofval	$⊢ ((φ \land (x Fn A \land y Fn A)) \land z \in A) \to (x {\underset{˙}{+}}_{f} y) (z) = x (z) \underset{˙}{+} y (z)$
51	50	an32s	$⊢ ((φ \land z \in A) \land (x Fn A \land y Fn A)) \to (x {\underset{˙}{+}}_{f} y) (z) = x (z) \underset{˙}{+} y (z)$
52		fveq1	$⊢ w = x {\underset{˙}{+}}_{f} y \to w (z) = (x {\underset{˙}{+}}_{f} y) (z)$
53		fvex	$⊢ (x {\underset{˙}{+}}_{f} y) (z) \in V$
54	52 41 53	fvmpt	$⊢ x {\underset{˙}{+}}_{f} y \in V \to (w \in V ⟼ w (z)) (x {\underset{˙}{+}}_{f} y) = (x {\underset{˙}{+}}_{f} y) (z)$
55	28 54	ax-mp	$⊢ (w \in V ⟼ w (z)) (x {\underset{˙}{+}}_{f} y) = (x {\underset{˙}{+}}_{f} y) (z)$
56		fveq1	$⊢ w = x \to w (z) = x (z)$
57		fvex	$⊢ x (z) \in V$
58	56 41 57	fvmpt	$⊢ x \in V \to (w \in V ⟼ w (z)) (x) = x (z)$
59	58	elv	$⊢ (w \in V ⟼ w (z)) (x) = x (z)$
60		fveq1	$⊢ w = y \to w (z) = y (z)$
61		fvex	$⊢ y (z) \in V$
62	60 41 61	fvmpt	$⊢ y \in V \to (w \in V ⟼ w (z)) (y) = y (z)$
63	62	elv	$⊢ (w \in V ⟼ w (z)) (y) = y (z)$
64	59 63	oveq12i	$⊢ (w \in V ⟼ w (z)) (x) \underset{˙}{+} (w \in V ⟼ w (z)) (y) = x (z) \underset{˙}{+} y (z)$
65	51 55 64	3eqtr4g	$⊢ ((φ \land z \in A) \land (x Fn A \land y Fn A)) \to (w \in V ⟼ w (z)) (x {\underset{˙}{+}}_{f} y) = (w \in V ⟼ w (z)) (x) \underset{˙}{+} (w \in V ⟼ w (z)) (y)$
66	27 65	sylan2b	$⊢ ((φ \land z \in A) \land (x \in \{z \| z Fn A\} \land y \in \{z \| z Fn A\})) \to (w \in V ⟼ w (z)) (x {\underset{˙}{+}}_{f} y) = (w \in V ⟼ w (z)) (x) \underset{˙}{+} (w \in V ⟼ w (z)) (y)$
67		fveq1	$⊢ w = F (x) \to w (z) = F (x) (z)$
68		fvex	$⊢ F (x) (z) \in V$
69	67 41 68	fvmpt	$⊢ F (x) \in V \to (w \in V ⟼ w (z)) (F (x)) = F (x) (z)$
70	11 69	ax-mp	$⊢ (w \in V ⟼ w (z)) (F (x)) = F (x) (z)$
71	3	adantlr	$⊢ ((φ \land z \in A) \land x \in (M \dots N)) \to F (x) = (z \in A ⟼ G (x))$
72	71	fveq1d	$⊢ ((φ \land z \in A) \land x \in (M \dots N)) \to F (x) (z) = (z \in A ⟼ G (x)) (z)$
73		simplr	$⊢ ((φ \land z \in A) \land x \in (M \dots N)) \to z \in A$
74	6	fvmpt2	$⊢ (z \in A \land G (x) \in V) \to (z \in A ⟼ G (x)) (z) = G (x)$
75	73 4 74	sylancl	$⊢ ((φ \land z \in A) \land x \in (M \dots N)) \to (z \in A ⟼ G (x)) (z) = G (x)$
76	72 75	eqtrd	$⊢ ((φ \land z \in A) \land x \in (M \dots N)) \to F (x) (z) = G (x)$
77	70 76	syl5eq	$⊢ ((φ \land z \in A) \land x \in (M \dots N)) \to (w \in V ⟼ w (z)) (F (x)) = G (x)$
78	45 46 47 66 77	seqhomo	$⊢ (φ \land z \in A) \to (w \in V ⟼ w (z)) (seq M (\circ_{f} \underset{˙}{+}, F) (N)) = seq M (\underset{˙}{+}, G) (N)$
79	44 78	eqtr3d	$⊢ (φ \land z \in A) \to seq M (\circ_{f} \underset{˙}{+}, F) (N) (z) = seq M (\underset{˙}{+}, G) (N)$
80	79	mpteq2dva	$⊢ φ \to (z \in A ⟼ seq M (\circ_{f} \underset{˙}{+}, F) (N) (z)) = (z \in A ⟼ seq M (\underset{˙}{+}, G) (N))$
81	39 80	eqtrd	$⊢ φ \to seq M (\circ_{f} \underset{˙}{+}, F) (N) = (z \in A ⟼ seq M (\underset{˙}{+}, G) (N))$

Metamath Proof Explorer

Theorem seqof

Proof