seqof2

Description: Distribute function operation through a sequence. Maps-to notation version of seqof . (Contributed by Mario Carneiro, 7-Jul-2017)

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

Proof

Step	Hyp	Ref	Expression
1		seqof2.1	$⊢ φ \to A \in V$
2		seqof2.2	$⊢ φ \to N \in ℤ_{\geq M}$
3		seqof2.3	$⊢ φ \to (M \dots N) \subseteq B$
4		seqof2.4	$⊢ (φ \land (x \in B \land z \in A)) \to X \in W$
5		nfv	$⊢ Ⅎ x (φ \land n \in (M \dots N))$
6		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in B ⟼ (z \in A ⟼ X)) (n)$
7		nfcv	$⊢ \underline{Ⅎ} x A$
8		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in B ⟼ X) (n)$
9	7 8	nfmpt	$⊢ \underline{Ⅎ} x (z \in A ⟼ (x \in B ⟼ X) (n))$
10	6 9	nfeq	$⊢ Ⅎ x (x \in B ⟼ (z \in A ⟼ X)) (n) = (z \in A ⟼ (x \in B ⟼ X) (n))$
11	5 10	nfim	$⊢ Ⅎ x ((φ \land n \in (M \dots N)) \to (x \in B ⟼ (z \in A ⟼ X)) (n) = (z \in A ⟼ (x \in B ⟼ X) (n)))$
12		eleq1w	$⊢ x = n \to (x \in (M \dots N) \leftrightarrow n \in (M \dots N))$
13	12	anbi2d	$⊢ x = n \to ((φ \land x \in (M \dots N)) \leftrightarrow (φ \land n \in (M \dots N)))$
14		fveq2	$⊢ x = n \to (x \in B ⟼ (z \in A ⟼ X)) (x) = (x \in B ⟼ (z \in A ⟼ X)) (n)$
15		fveq2	$⊢ x = n \to (x \in B ⟼ X) (x) = (x \in B ⟼ X) (n)$
16	15	mpteq2dv	$⊢ x = n \to (z \in A ⟼ (x \in B ⟼ X) (x)) = (z \in A ⟼ (x \in B ⟼ X) (n))$
17	14 16	eqeq12d	$⊢ x = n \to ((x \in B ⟼ (z \in A ⟼ X)) (x) = (z \in A ⟼ (x \in B ⟼ X) (x)) \leftrightarrow (x \in B ⟼ (z \in A ⟼ X)) (n) = (z \in A ⟼ (x \in B ⟼ X) (n)))$
18	13 17	imbi12d	$⊢ x = n \to (((φ \land x \in (M \dots N)) \to (x \in B ⟼ (z \in A ⟼ X)) (x) = (z \in A ⟼ (x \in B ⟼ X) (x))) \leftrightarrow ((φ \land n \in (M \dots N)) \to (x \in B ⟼ (z \in A ⟼ X)) (n) = (z \in A ⟼ (x \in B ⟼ X) (n))))$
19	3	sselda	$⊢ (φ \land x \in (M \dots N)) \to x \in B$
20	1	adantr	$⊢ (φ \land x \in (M \dots N)) \to A \in V$
21	20	mptexd	$⊢ (φ \land x \in (M \dots N)) \to (z \in A ⟼ X) \in V$
22		eqid	$⊢ (x \in B ⟼ (z \in A ⟼ X)) = (x \in B ⟼ (z \in A ⟼ X))$
23	22	fvmpt2	$⊢ (x \in B \land (z \in A ⟼ X) \in V) \to (x \in B ⟼ (z \in A ⟼ X)) (x) = (z \in A ⟼ X)$
24	19 21 23	syl2anc	$⊢ (φ \land x \in (M \dots N)) \to (x \in B ⟼ (z \in A ⟼ X)) (x) = (z \in A ⟼ X)$
25	19	adantr	$⊢ ((φ \land x \in (M \dots N)) \land z \in A) \to x \in B$
26		simpll	$⊢ ((φ \land x \in (M \dots N)) \land z \in A) \to φ$
27		simpr	$⊢ ((φ \land x \in (M \dots N)) \land z \in A) \to z \in A$
28	26 25 27 4	syl12anc	$⊢ ((φ \land x \in (M \dots N)) \land z \in A) \to X \in W$
29		eqid	$⊢ (x \in B ⟼ X) = (x \in B ⟼ X)$
30	29	fvmpt2	$⊢ (x \in B \land X \in W) \to (x \in B ⟼ X) (x) = X$
31	25 28 30	syl2anc	$⊢ ((φ \land x \in (M \dots N)) \land z \in A) \to (x \in B ⟼ X) (x) = X$
32	31	mpteq2dva	$⊢ (φ \land x \in (M \dots N)) \to (z \in A ⟼ (x \in B ⟼ X) (x)) = (z \in A ⟼ X)$
33	24 32	eqtr4d	$⊢ (φ \land x \in (M \dots N)) \to (x \in B ⟼ (z \in A ⟼ X)) (x) = (z \in A ⟼ (x \in B ⟼ X) (x))$
34	11 18 33	chvarfv	$⊢ (φ \land n \in (M \dots N)) \to (x \in B ⟼ (z \in A ⟼ X)) (n) = (z \in A ⟼ (x \in B ⟼ X) (n))$
35		nfcv	$⊢ \underline{Ⅎ} y (x \in B ⟼ X) (n)$
36		nfcsb1v	$⊢ \underline{Ⅎ} z ⦋ y / z ⦌ (x \in B ⟼ X)$
37		nfcv	$⊢ \underline{Ⅎ} z n$
38	36 37	nffv	$⊢ \underline{Ⅎ} z ⦋ y / z ⦌ (x \in B ⟼ X) (n)$
39		csbeq1a	$⊢ z = y \to (x \in B ⟼ X) = ⦋ y / z ⦌ (x \in B ⟼ X)$
40	39	fveq1d	$⊢ z = y \to (x \in B ⟼ X) (n) = ⦋ y / z ⦌ (x \in B ⟼ X) (n)$
41	35 38 40	cbvmpt	$⊢ (z \in A ⟼ (x \in B ⟼ X) (n)) = (y \in A ⟼ ⦋ y / z ⦌ (x \in B ⟼ X) (n))$
42	34 41	syl6eq	$⊢ (φ \land n \in (M \dots N)) \to (x \in B ⟼ (z \in A ⟼ X)) (n) = (y \in A ⟼ ⦋ y / z ⦌ (x \in B ⟼ X) (n))$
43	1 2 42	seqof	$⊢ φ \to seq M (\circ_{f} \underset{˙}{+}, (x \in B ⟼ (z \in A ⟼ X))) (N) = (y \in A ⟼ seq M (\underset{˙}{+}, ⦋ y / z ⦌ (x \in B ⟼ X)) (N))$
44		nfcv	$⊢ \underline{Ⅎ} y seq M (\underset{˙}{+}, (x \in B ⟼ X)) (N)$
45		nfcv	$⊢ \underline{Ⅎ} z M$
46		nfcv	$⊢ \underline{Ⅎ} z \underset{˙}{+}$
47	45 46 36	nfseq	$⊢ \underline{Ⅎ} z seq M (\underset{˙}{+}, ⦋ y / z ⦌ (x \in B ⟼ X))$
48		nfcv	$⊢ \underline{Ⅎ} z N$
49	47 48	nffv	$⊢ \underline{Ⅎ} z seq M (\underset{˙}{+}, ⦋ y / z ⦌ (x \in B ⟼ X)) (N)$
50	39	seqeq3d	$⊢ z = y \to seq M (\underset{˙}{+}, (x \in B ⟼ X)) = seq M (\underset{˙}{+}, ⦋ y / z ⦌ (x \in B ⟼ X))$
51	50	fveq1d	$⊢ z = y \to seq M (\underset{˙}{+}, (x \in B ⟼ X)) (N) = seq M (\underset{˙}{+}, ⦋ y / z ⦌ (x \in B ⟼ X)) (N)$
52	44 49 51	cbvmpt	$⊢ (z \in A ⟼ seq M (\underset{˙}{+}, (x \in B ⟼ X)) (N)) = (y \in A ⟼ seq M (\underset{˙}{+}, ⦋ y / z ⦌ (x \in B ⟼ X)) (N))$
53	43 52	eqtr4di	$⊢ φ \to seq M (\circ_{f} \underset{˙}{+}, (x \in B ⟼ (z \in A ⟼ X))) (N) = (z \in A ⟼ seq M (\underset{˙}{+}, (x \in B ⟼ X)) (N))$

Metamath Proof Explorer

Theorem seqof2

Proof