seqf1o

Description: Rearrange a sum via an arbitrary bijection on ( M ... N ) . (Contributed by Mario Carneiro, 27-Feb-2014) (Revised by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	seqf1o.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqf1o.2	$⊢ (φ \land (x \in C \land y \in C)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
	seqf1o.3	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	seqf1o.4	$⊢ φ \to N \in ℤ_{\geq M}$
	seqf1o.5	$⊢ φ \to C \subseteq S$
	seqf1o.6	$⊢ φ \to F : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N)$
	seqf1o.7	$⊢ (φ \land x \in (M \dots N)) \to G (x) \in C$
	seqf1o.8	$⊢ (φ \land k \in (M \dots N)) \to H (k) = G (F (k))$
Assertion	seqf1o	$⊢ φ \to seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, G) (N)$

Proof

Step	Hyp	Ref	Expression
1		seqf1o.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
2		seqf1o.2	$⊢ (φ \land (x \in C \land y \in C)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
3		seqf1o.3	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
4		seqf1o.4	$⊢ φ \to N \in ℤ_{\geq M}$
5		seqf1o.5	$⊢ φ \to C \subseteq S$
6		seqf1o.6	$⊢ φ \to F : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N)$
7		seqf1o.7	$⊢ (φ \land x \in (M \dots N)) \to G (x) \in C$
8		seqf1o.8	$⊢ (φ \land k \in (M \dots N)) \to H (k) = G (F (k))$
9	7	fmpttd	$⊢ φ \to (x \in (M \dots N) ⟼ G (x)) : (M \dots N) ⟶ C$
10		oveq2	$⊢ x = M \to (M \dots x) = (M \dots M)$
11		f1oeq23	$⊢ ((M \dots x) = (M \dots M) \land (M \dots x) = (M \dots M)) \to (f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \leftrightarrow f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M))$
12	10 10 11	syl2anc	$⊢ x = M \to (f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \leftrightarrow f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M))$
13	10	feq2d	$⊢ x = M \to (g : (M \dots x) ⟶ C \leftrightarrow g : (M \dots M) ⟶ C)$
14	12 13	anbi12d	$⊢ x = M \to ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \leftrightarrow (f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C))$
15		fveq2	$⊢ x = M \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, (g \circ f)) (M)$
16		fveq2	$⊢ x = M \to seq M (\underset{˙}{+}, g) (x) = seq M (\underset{˙}{+}, g) (M)$
17	15 16	eqeq12d	$⊢ x = M \to (seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x) \leftrightarrow seq M (\underset{˙}{+}, (g \circ f)) (M) = seq M (\underset{˙}{+}, g) (M))$
18	14 17	imbi12d	$⊢ x = M \to (((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x)) \leftrightarrow ((f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (M) = seq M (\underset{˙}{+}, g) (M)))$
19	18	2albidv	$⊢ x = M \to (\forall g \forall f ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x)) \leftrightarrow \forall g \forall f ((f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (M) = seq M (\underset{˙}{+}, g) (M)))$
20	19	imbi2d	$⊢ x = M \to ((φ \to \forall g \forall f ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x))) \leftrightarrow (φ \to \forall g \forall f ((f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (M) = seq M (\underset{˙}{+}, g) (M))))$
21		oveq2	$⊢ x = k \to (M \dots x) = (M \dots k)$
22		f1oeq23	$⊢ ((M \dots x) = (M \dots k) \land (M \dots x) = (M \dots k)) \to (f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \leftrightarrow f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k))$
23	21 21 22	syl2anc	$⊢ x = k \to (f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \leftrightarrow f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k))$
24	21	feq2d	$⊢ x = k \to (g : (M \dots x) ⟶ C \leftrightarrow g : (M \dots k) ⟶ C)$
25	23 24	anbi12d	$⊢ x = k \to ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \leftrightarrow (f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C))$
26		fveq2	$⊢ x = k \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, (g \circ f)) (k)$
27		fveq2	$⊢ x = k \to seq M (\underset{˙}{+}, g) (x) = seq M (\underset{˙}{+}, g) (k)$
28	26 27	eqeq12d	$⊢ x = k \to (seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x) \leftrightarrow seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))$
29	25 28	imbi12d	$⊢ x = k \to (((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x)) \leftrightarrow ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k)))$
30	29	2albidv	$⊢ x = k \to (\forall g \forall f ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x)) \leftrightarrow \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k)))$
31	30	imbi2d	$⊢ x = k \to ((φ \to \forall g \forall f ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x))) \leftrightarrow (φ \to \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))))$
32		oveq2	$⊢ x = k + 1 \to (M \dots x) = (M \dots k + 1)$
33		f1oeq23	$⊢ ((M \dots x) = (M \dots k + 1) \land (M \dots x) = (M \dots k + 1)) \to (f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \leftrightarrow f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1))$
34	32 32 33	syl2anc	$⊢ x = k + 1 \to (f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \leftrightarrow f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1))$
35	32	feq2d	$⊢ x = k + 1 \to (g : (M \dots x) ⟶ C \leftrightarrow g : (M \dots k + 1) ⟶ C)$
36	34 35	anbi12d	$⊢ x = k + 1 \to ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \leftrightarrow (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C))$
37		fveq2	$⊢ x = k + 1 \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, (g \circ f)) (k + 1)$
38		fveq2	$⊢ x = k + 1 \to seq M (\underset{˙}{+}, g) (x) = seq M (\underset{˙}{+}, g) (k + 1)$
39	37 38	eqeq12d	$⊢ x = k + 1 \to (seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x) \leftrightarrow seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1))$
40	36 39	imbi12d	$⊢ x = k + 1 \to (((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x)) \leftrightarrow ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1)))$
41	40	2albidv	$⊢ x = k + 1 \to (\forall g \forall f ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x)) \leftrightarrow \forall g \forall f ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1)))$
42	41	imbi2d	$⊢ x = k + 1 \to ((φ \to \forall g \forall f ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x))) \leftrightarrow (φ \to \forall g \forall f ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1))))$
43		oveq2	$⊢ x = N \to (M \dots x) = (M \dots N)$
44		f1oeq23	$⊢ ((M \dots x) = (M \dots N) \land (M \dots x) = (M \dots N)) \to (f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \leftrightarrow f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N))$
45	43 43 44	syl2anc	$⊢ x = N \to (f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \leftrightarrow f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N))$
46	43	feq2d	$⊢ x = N \to (g : (M \dots x) ⟶ C \leftrightarrow g : (M \dots N) ⟶ C)$
47	45 46	anbi12d	$⊢ x = N \to ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \leftrightarrow (f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C))$
48		fveq2	$⊢ x = N \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, (g \circ f)) (N)$
49		fveq2	$⊢ x = N \to seq M (\underset{˙}{+}, g) (x) = seq M (\underset{˙}{+}, g) (N)$
50	48 49	eqeq12d	$⊢ x = N \to (seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x) \leftrightarrow seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N))$
51	47 50	imbi12d	$⊢ x = N \to (((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x)) \leftrightarrow ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N)))$
52	51	2albidv	$⊢ x = N \to (\forall g \forall f ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x)) \leftrightarrow \forall g \forall f ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N)))$
53	52	imbi2d	$⊢ x = N \to ((φ \to \forall g \forall f ((f : (M \dots x) \underset{1-1 onto}{⟶} (M \dots x) \land g : (M \dots x) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (x) = seq M (\underset{˙}{+}, g) (x))) \leftrightarrow (φ \to \forall g \forall f ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N))))$
54		f1of	$⊢ f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \to f : (M \dots M) ⟶ (M \dots M)$
55	54	adantr	$⊢ (f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C) \to f : (M \dots M) ⟶ (M \dots M)$
56		elfz3	$⊢ M \in ℤ \to M \in (M \dots M)$
57		fvco3	$⊢ (f : (M \dots M) ⟶ (M \dots M) \land M \in (M \dots M)) \to (g \circ f) (M) = g (f (M))$
58	55 56 57	syl2anr	$⊢ (M \in ℤ \land (f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C)) \to (g \circ f) (M) = g (f (M))$
59		ffvelcdm	$⊢ (f : (M \dots M) ⟶ (M \dots M) \land M \in (M \dots M)) \to f (M) \in (M \dots M)$
60	54 56 59	syl2anr	$⊢ (M \in ℤ \land f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M)) \to f (M) \in (M \dots M)$
61		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
62	61	eleq2d	$⊢ M \in ℤ \to (f (M) \in (M \dots M) \leftrightarrow f (M) \in \{M\})$
63		elsni	$⊢ f (M) \in \{M\} \to f (M) = M$
64	62 63	biimtrdi	$⊢ M \in ℤ \to (f (M) \in (M \dots M) \to f (M) = M)$
65	64	imp	$⊢ (M \in ℤ \land f (M) \in (M \dots M)) \to f (M) = M$
66	60 65	syldan	$⊢ (M \in ℤ \land f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M)) \to f (M) = M$
67	66	adantrr	$⊢ (M \in ℤ \land (f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C)) \to f (M) = M$
68	67	fveq2d	$⊢ (M \in ℤ \land (f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C)) \to g (f (M)) = g (M)$
69	58 68	eqtrd	$⊢ (M \in ℤ \land (f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C)) \to (g \circ f) (M) = g (M)$
70		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, (g \circ f)) (M) = (g \circ f) (M)$
71	70	adantr	$⊢ (M \in ℤ \land (f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C)) \to seq M (\underset{˙}{+}, (g \circ f)) (M) = (g \circ f) (M)$
72		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, g) (M) = g (M)$
73	72	adantr	$⊢ (M \in ℤ \land (f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C)) \to seq M (\underset{˙}{+}, g) (M) = g (M)$
74	69 71 73	3eqtr4d	$⊢ (M \in ℤ \land (f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C)) \to seq M (\underset{˙}{+}, (g \circ f)) (M) = seq M (\underset{˙}{+}, g) (M)$
75	74	ex	$⊢ M \in ℤ \to ((f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (M) = seq M (\underset{˙}{+}, g) (M))$
76	75	alrimivv	$⊢ M \in ℤ \to \forall g \forall f ((f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (M) = seq M (\underset{˙}{+}, g) (M))$
77	76	a1d	$⊢ M \in ℤ \to (φ \to \forall g \forall f ((f : (M \dots M) \underset{1-1 onto}{⟶} (M \dots M) \land g : (M \dots M) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (M) = seq M (\underset{˙}{+}, g) (M)))$
78		f1oeq1	$⊢ f = t \to (f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \leftrightarrow t : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k))$
79		feq1	$⊢ g = s \to (g : (M \dots k) ⟶ C \leftrightarrow s : (M \dots k) ⟶ C)$
80	78 79	bi2anan9r	$⊢ (g = s \land f = t) \to ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \leftrightarrow (t : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land s : (M \dots k) ⟶ C))$
81		coeq1	$⊢ g = s \to g \circ f = s \circ f$
82		coeq2	$⊢ f = t \to s \circ f = s \circ t$
83	81 82	sylan9eq	$⊢ (g = s \land f = t) \to g \circ f = s \circ t$
84	83	seqeq3d	$⊢ (g = s \land f = t) \to seq M (\underset{˙}{+}, (g \circ f)) = seq M (\underset{˙}{+}, (s \circ t))$
85	84	fveq1d	$⊢ (g = s \land f = t) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, (s \circ t)) (k)$
86		simpl	$⊢ (g = s \land f = t) \to g = s$
87	86	seqeq3d	$⊢ (g = s \land f = t) \to seq M (\underset{˙}{+}, g) = seq M (\underset{˙}{+}, s)$
88	87	fveq1d	$⊢ (g = s \land f = t) \to seq M (\underset{˙}{+}, g) (k) = seq M (\underset{˙}{+}, s) (k)$
89	85 88	eqeq12d	$⊢ (g = s \land f = t) \to (seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k) \leftrightarrow seq M (\underset{˙}{+}, (s \circ t)) (k) = seq M (\underset{˙}{+}, s) (k))$
90	80 89	imbi12d	$⊢ (g = s \land f = t) \to (((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k)) \leftrightarrow ((t : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land s : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (s \circ t)) (k) = seq M (\underset{˙}{+}, s) (k)))$
91	90	cbval2vw	$⊢ \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k)) \leftrightarrow \forall s \forall t ((t : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land s : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (s \circ t)) (k) = seq M (\underset{˙}{+}, s) (k))$
92		simplll	$⊢ (((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \to φ$
93	92 1	sylan	$⊢ ((((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
94	92 2	sylan	$⊢ ((((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \land (x \in C \land y \in C)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
95	92 3	sylan	$⊢ ((((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
96		simpllr	$⊢ (((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \to k \in ℤ_{\geq M}$
97	92 5	syl	$⊢ (((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \to C \subseteq S$
98		simprl	$⊢ (((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \to f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1)$
99		simprr	$⊢ (((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \to g : (M \dots k + 1) ⟶ C$
100		eqid	$⊢ (w \in (M \dots k) ⟼ f (if (w < f^{-1} (k + 1), w, w + 1))) = (w \in (M \dots k) ⟼ f (if (w < f^{-1} (k + 1), w, w + 1)))$
101		eqid	$⊢ f^{-1} (k + 1) = f^{-1} (k + 1)$
102		simplr	$⊢ (((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \to \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))$
103	102 91	sylib	$⊢ (((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \to \forall s \forall t ((t : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land s : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (s \circ t)) (k) = seq M (\underset{˙}{+}, s) (k))$
104	93 94 95 96 97 98 99 100 101 103	seqf1olem2	$⊢ (((φ \land k \in ℤ_{\geq M}) \land \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \land (f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C)) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1)$
105	104	exp31	$⊢ (φ \land k \in ℤ_{\geq M}) \to (\forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k)) \to ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1)))$
106	91 105	biimtrrid	$⊢ (φ \land k \in ℤ_{\geq M}) \to (\forall s \forall t ((t : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land s : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (s \circ t)) (k) = seq M (\underset{˙}{+}, s) (k)) \to ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1)))$
107	106	alrimdv	$⊢ (φ \land k \in ℤ_{\geq M}) \to (\forall s \forall t ((t : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land s : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (s \circ t)) (k) = seq M (\underset{˙}{+}, s) (k)) \to \forall f ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1)))$
108	107	alrimdv	$⊢ (φ \land k \in ℤ_{\geq M}) \to (\forall s \forall t ((t : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land s : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (s \circ t)) (k) = seq M (\underset{˙}{+}, s) (k)) \to \forall g \forall f ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1)))$
109	91 108	biimtrid	$⊢ (φ \land k \in ℤ_{\geq M}) \to (\forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k)) \to \forall g \forall f ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1)))$
110	109	expcom	$⊢ k \in ℤ_{\geq M} \to (φ \to (\forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k)) \to \forall g \forall f ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1))))$
111	110	a2d	$⊢ k \in ℤ_{\geq M} \to ((φ \to \forall g \forall f ((f : (M \dots k) \underset{1-1 onto}{⟶} (M \dots k) \land g : (M \dots k) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k) = seq M (\underset{˙}{+}, g) (k))) \to (φ \to \forall g \forall f ((f : (M \dots k + 1) \underset{1-1 onto}{⟶} (M \dots k + 1) \land g : (M \dots k + 1) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (k + 1) = seq M (\underset{˙}{+}, g) (k + 1))))$
112	20 31 42 53 77 111	uzind4	$⊢ N \in ℤ_{\geq M} \to (φ \to \forall g \forall f ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N)))$
113	4 112	mpcom	$⊢ φ \to \forall g \forall f ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N))$
114		fvex	$⊢ G (x) \in V$
115		eqid	$⊢ (x \in (M \dots N) ⟼ G (x)) = (x \in (M \dots N) ⟼ G (x))$
116	114 115	fnmpti	$⊢ (x \in (M \dots N) ⟼ G (x)) Fn (M \dots N)$
117		fzfi	$⊢ (M \dots N) \in Fin$
118		fnfi	$⊢ ((x \in (M \dots N) ⟼ G (x)) Fn (M \dots N) \land (M \dots N) \in Fin) \to (x \in (M \dots N) ⟼ G (x)) \in Fin$
119	116 117 118	mp2an	$⊢ (x \in (M \dots N) ⟼ G (x)) \in Fin$
120		f1of	$⊢ F : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \to F : (M \dots N) ⟶ (M \dots N)$
121	6 120	syl	$⊢ φ \to F : (M \dots N) ⟶ (M \dots N)$
122		ovexd	$⊢ φ \to (M \dots N) \in V$
123		fex2	$⊢ (F : (M \dots N) ⟶ (M \dots N) \land (M \dots N) \in V \land (M \dots N) \in V) \to F \in V$
124	121 122 122 123	syl3anc	$⊢ φ \to F \in V$
125		f1oeq1	$⊢ f = F \to (f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \leftrightarrow F : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N))$
126		feq1	$⊢ g = (x \in (M \dots N) ⟼ G (x)) \to (g : (M \dots N) ⟶ C \leftrightarrow (x \in (M \dots N) ⟼ G (x)) : (M \dots N) ⟶ C)$
127	125 126	bi2anan9r	$⊢ (g = (x \in (M \dots N) ⟼ G (x)) \land f = F) \to ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \leftrightarrow (F : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land (x \in (M \dots N) ⟼ G (x)) : (M \dots N) ⟶ C))$
128		coeq1	$⊢ g = (x \in (M \dots N) ⟼ G (x)) \to g \circ f = (x \in (M \dots N) ⟼ G (x)) \circ f$
129		coeq2	$⊢ f = F \to (x \in (M \dots N) ⟼ G (x)) \circ f = (x \in (M \dots N) ⟼ G (x)) \circ F$
130	128 129	sylan9eq	$⊢ (g = (x \in (M \dots N) ⟼ G (x)) \land f = F) \to g \circ f = (x \in (M \dots N) ⟼ G (x)) \circ F$
131	130	seqeq3d	$⊢ (g = (x \in (M \dots N) ⟼ G (x)) \land f = F) \to seq M (\underset{˙}{+}, (g \circ f)) = seq M (\underset{˙}{+}, ((x \in (M \dots N) ⟼ G (x)) \circ F))$
132	131	fveq1d	$⊢ (g = (x \in (M \dots N) ⟼ G (x)) \land f = F) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, ((x \in (M \dots N) ⟼ G (x)) \circ F)) (N)$
133		simpl	$⊢ (g = (x \in (M \dots N) ⟼ G (x)) \land f = F) \to g = (x \in (M \dots N) ⟼ G (x))$
134	133	seqeq3d	$⊢ (g = (x \in (M \dots N) ⟼ G (x)) \land f = F) \to seq M (\underset{˙}{+}, g) = seq M (\underset{˙}{+}, (x \in (M \dots N) ⟼ G (x)))$
135	134	fveq1d	$⊢ (g = (x \in (M \dots N) ⟼ G (x)) \land f = F) \to seq M (\underset{˙}{+}, g) (N) = seq M (\underset{˙}{+}, (x \in (M \dots N) ⟼ G (x))) (N)$
136	132 135	eqeq12d	$⊢ (g = (x \in (M \dots N) ⟼ G (x)) \land f = F) \to (seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N) \leftrightarrow seq M (\underset{˙}{+}, ((x \in (M \dots N) ⟼ G (x)) \circ F)) (N) = seq M (\underset{˙}{+}, (x \in (M \dots N) ⟼ G (x))) (N))$
137	127 136	imbi12d	$⊢ (g = (x \in (M \dots N) ⟼ G (x)) \land f = F) \to (((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N)) \leftrightarrow ((F : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land (x \in (M \dots N) ⟼ G (x)) : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, ((x \in (M \dots N) ⟼ G (x)) \circ F)) (N) = seq M (\underset{˙}{+}, (x \in (M \dots N) ⟼ G (x))) (N)))$
138	137	spc2gv	$⊢ ((x \in (M \dots N) ⟼ G (x)) \in Fin \land F \in V) \to (\forall g \forall f ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N)) \to ((F : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land (x \in (M \dots N) ⟼ G (x)) : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, ((x \in (M \dots N) ⟼ G (x)) \circ F)) (N) = seq M (\underset{˙}{+}, (x \in (M \dots N) ⟼ G (x))) (N)))$
139	119 124 138	sylancr	$⊢ φ \to (\forall g \forall f ((f : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land g : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, (g \circ f)) (N) = seq M (\underset{˙}{+}, g) (N)) \to ((F : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land (x \in (M \dots N) ⟼ G (x)) : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, ((x \in (M \dots N) ⟼ G (x)) \circ F)) (N) = seq M (\underset{˙}{+}, (x \in (M \dots N) ⟼ G (x))) (N)))$
140	113 139	mpd	$⊢ φ \to ((F : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N) \land (x \in (M \dots N) ⟼ G (x)) : (M \dots N) ⟶ C) \to seq M (\underset{˙}{+}, ((x \in (M \dots N) ⟼ G (x)) \circ F)) (N) = seq M (\underset{˙}{+}, (x \in (M \dots N) ⟼ G (x))) (N))$
141	6 9 140	mp2and	$⊢ φ \to seq M (\underset{˙}{+}, ((x \in (M \dots N) ⟼ G (x)) \circ F)) (N) = seq M (\underset{˙}{+}, (x \in (M \dots N) ⟼ G (x))) (N)$
142	121	ffvelcdmda	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in (M \dots N)$
143		fveq2	$⊢ x = F (k) \to G (x) = G (F (k))$
144		fvex	$⊢ G (F (k)) \in V$
145	143 115 144	fvmpt	$⊢ F (k) \in (M \dots N) \to (x \in (M \dots N) ⟼ G (x)) (F (k)) = G (F (k))$
146	142 145	syl	$⊢ (φ \land k \in (M \dots N)) \to (x \in (M \dots N) ⟼ G (x)) (F (k)) = G (F (k))$
147		fvco3	$⊢ (F : (M \dots N) ⟶ (M \dots N) \land k \in (M \dots N)) \to ((x \in (M \dots N) ⟼ G (x)) \circ F) (k) = (x \in (M \dots N) ⟼ G (x)) (F (k))$
148	121 147	sylan	$⊢ (φ \land k \in (M \dots N)) \to ((x \in (M \dots N) ⟼ G (x)) \circ F) (k) = (x \in (M \dots N) ⟼ G (x)) (F (k))$
149	146 148 8	3eqtr4d	$⊢ (φ \land k \in (M \dots N)) \to ((x \in (M \dots N) ⟼ G (x)) \circ F) (k) = H (k)$
150	4 149	seqfveq	$⊢ φ \to seq M (\underset{˙}{+}, ((x \in (M \dots N) ⟼ G (x)) \circ F)) (N) = seq M (\underset{˙}{+}, H) (N)$
151		fveq2	$⊢ x = k \to G (x) = G (k)$
152		fvex	$⊢ G (k) \in V$
153	151 115 152	fvmpt	$⊢ k \in (M \dots N) \to (x \in (M \dots N) ⟼ G (x)) (k) = G (k)$
154	153	adantl	$⊢ (φ \land k \in (M \dots N)) \to (x \in (M \dots N) ⟼ G (x)) (k) = G (k)$
155	4 154	seqfveq	$⊢ φ \to seq M (\underset{˙}{+}, (x \in (M \dots N) ⟼ G (x))) (N) = seq M (\underset{˙}{+}, G) (N)$
156	141 150 155	3eqtr3d	$⊢ φ \to seq M (\underset{˙}{+}, H) (N) = seq M (\underset{˙}{+}, G) (N)$

Metamath Proof Explorer

Theorem seqf1o

Proof