sticksstones8

Description: Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 1-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones8.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones8.2	$⊢ φ \to K \in ℕ_{0}$
	sticksstones8.3	$⊢ F = (a \in A ⟼ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)))$
	sticksstones8.4	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
	sticksstones8.5	$⊢ B = \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
Assertion	sticksstones8	$⊢ φ \to F : A ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		sticksstones8.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones8.2	$⊢ φ \to K \in ℕ_{0}$
3		sticksstones8.3	$⊢ F = (a \in A ⟼ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)))$
4		sticksstones8.4	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
5		sticksstones8.5	$⊢ B = \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
6		eqidd	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to (e \in (1 \dots K) ⟼ e + \sum_{l = 1}^{e} a (l)) = (e \in (1 \dots K) ⟼ e + \sum_{l = 1}^{e} a (l))$
7		simpr	$⊢ ((φ \land a \in A \land j \in (1 \dots K)) \land e = j) \to e = j$
8	7	oveq2d	$⊢ ((φ \land a \in A \land j \in (1 \dots K)) \land e = j) \to (1 \dots e) = (1 \dots j)$
9	8	sumeq1d	$⊢ ((φ \land a \in A \land j \in (1 \dots K)) \land e = j) \to \sum_{l = 1}^{e} a (l) = \sum_{l = 1}^{j} a (l)$
10	7 9	oveq12d	$⊢ ((φ \land a \in A \land j \in (1 \dots K)) \land e = j) \to e + \sum_{l = 1}^{e} a (l) = j + \sum_{l = 1}^{j} a (l)$
11		simp3	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to j \in (1 \dots K)$
12		ovexd	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to j + \sum_{l = 1}^{j} a (l) \in V$
13	6 10 11 12	fvmptd	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to (e \in (1 \dots K) ⟼ e + \sum_{l = 1}^{e} a (l)) (j) = j + \sum_{l = 1}^{j} a (l)$
14	1	3ad2ant1	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to N \in ℕ_{0}$
15	2	3ad2ant1	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to K \in ℕ_{0}$
16		simpr	$⊢ (φ \land a \in A) \to a \in A$
17	4	a1i	$⊢ (φ \land a \in A) \to A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
18	17	eqcomd	$⊢ (φ \land a \in A) \to \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} = A$
19	16 18	eleqtrrd	$⊢ (φ \land a \in A) \to a \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
20		feq1	$⊢ g = a \to (g : (1 \dots K + 1) ⟶ ℕ_{0} \leftrightarrow a : (1 \dots K + 1) ⟶ ℕ_{0})$
21		simpl	$⊢ (g = a \land i \in (1 \dots K + 1)) \to g = a$
22	21	fveq1d	$⊢ (g = a \land i \in (1 \dots K + 1)) \to g (i) = a (i)$
23	22	sumeq2dv	$⊢ g = a \to \sum_{i = 1}^{K + 1} g (i) = \sum_{i = 1}^{K + 1} a (i)$
24	23	eqeq1d	$⊢ g = a \to (\sum_{i = 1}^{K + 1} g (i) = N \leftrightarrow \sum_{i = 1}^{K + 1} a (i) = N)$
25	20 24	anbi12d	$⊢ g = a \to ((g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N) \leftrightarrow (a : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} a (i) = N))$
26	25	elabg	$⊢ a \in A \to (a \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow (a : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} a (i) = N))$
27	16 26	syl	$⊢ (φ \land a \in A) \to (a \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow (a : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} a (i) = N))$
28	27	biimpd	$⊢ (φ \land a \in A) \to (a \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \to (a : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} a (i) = N))$
29	19 28	mpd	$⊢ (φ \land a \in A) \to (a : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} a (i) = N)$
30	29	simpld	$⊢ (φ \land a \in A) \to a : (1 \dots K + 1) ⟶ ℕ_{0}$
31	30	3adant3	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to a : (1 \dots K + 1) ⟶ ℕ_{0}$
32		eqid	$⊢ (e \in (1 \dots K) ⟼ e + \sum_{l = 1}^{e} a (l)) = (e \in (1 \dots K) ⟼ e + \sum_{l = 1}^{e} a (l))$
33		fveq2	$⊢ i = l \to a (i) = a (l)$
34		nfcv	$⊢ \underline{Ⅎ} l (1 \dots K + 1)$
35		nfcv	$⊢ \underline{Ⅎ} i (1 \dots K + 1)$
36		nfcv	$⊢ \underline{Ⅎ} l a (i)$
37		nfcv	$⊢ \underline{Ⅎ} i a (l)$
38	33 34 35 36 37	cbvsum	$⊢ \sum_{i = 1}^{K + 1} a (i) = \sum_{l = 1}^{K + 1} a (l)$
39	29	simprd	$⊢ (φ \land a \in A) \to \sum_{i = 1}^{K + 1} a (i) = N$
40	38 39	eqtr3id	$⊢ (φ \land a \in A) \to \sum_{l = 1}^{K + 1} a (l) = N$
41	40	3adant3	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to \sum_{l = 1}^{K + 1} a (l) = N$
42	14 15 31 11 32 41	sticksstones7	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to (e \in (1 \dots K) ⟼ e + \sum_{l = 1}^{e} a (l)) (j) \in (1 \dots N + K)$
43	13 42	eqeltrrd	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to j + \sum_{l = 1}^{j} a (l) \in (1 \dots N + K)$
44	43	3expa	$⊢ ((φ \land a \in A) \land j \in (1 \dots K)) \to j + \sum_{l = 1}^{j} a (l) \in (1 \dots N + K)$
45		eqid	$⊢ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l))$
46	44 45	fmptd	$⊢ (φ \land a \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) : (1 \dots K) ⟶ (1 \dots N + K)$
47	1	ad3antrrr	$⊢ (((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \to N \in ℕ_{0}$
48	47	adantr	$⊢ ((((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \land x < y) \to N \in ℕ_{0}$
49	2	ad3antrrr	$⊢ (((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \to K \in ℕ_{0}$
50	49	adantr	$⊢ ((((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \land x < y) \to K \in ℕ_{0}$
51	26	adantl	$⊢ (φ \land a \in A) \to (a \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow (a : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} a (i) = N))$
52	51	biimpd	$⊢ (φ \land a \in A) \to (a \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \to (a : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} a (i) = N))$
53	19 52	mpd	$⊢ (φ \land a \in A) \to (a : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} a (i) = N)$
54	53	simpld	$⊢ (φ \land a \in A) \to a : (1 \dots K + 1) ⟶ ℕ_{0}$
55	54	adantr	$⊢ ((φ \land a \in A) \land x \in (1 \dots K)) \to a : (1 \dots K + 1) ⟶ ℕ_{0}$
56	55	adantr	$⊢ (((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \to a : (1 \dots K + 1) ⟶ ℕ_{0}$
57	56	adantr	$⊢ ((((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \land x < y) \to a : (1 \dots K + 1) ⟶ ℕ_{0}$
58		simpllr	$⊢ ((((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \land x < y) \to x \in (1 \dots K)$
59		simplr	$⊢ ((((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \land x < y) \to y \in (1 \dots K)$
60		simpr	$⊢ ((((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \land x < y) \to x < y$
61	48 50 57 58 59 60 45	sticksstones6	$⊢ ((((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \land x < y) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y)$
62	61	ex	$⊢ (((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \to (x < y \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y))$
63	62	ralrimiva	$⊢ ((φ \land a \in A) \land x \in (1 \dots K)) \to \forall y \in (1 \dots K) (x < y \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y))$
64	63	ralrimiva	$⊢ (φ \land a \in A) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y))$
65	46 64	jca	$⊢ (φ \land a \in A) \to ((j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y)))$
66		fzfid	$⊢ (φ \land a \in A) \to (1 \dots K) \in Fin$
67	46 66	fexd	$⊢ (φ \land a \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in V$
68		feq1	$⊢ f = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \to (f : (1 \dots K) ⟶ (1 \dots N + K) \leftrightarrow (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) : (1 \dots K) ⟶ (1 \dots N + K))$
69		fveq1	$⊢ f = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \to f (x) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x)$
70		fveq1	$⊢ f = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \to f (y) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y)$
71	69 70	breq12d	$⊢ f = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \to (f (x) < f (y) \leftrightarrow (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y))$
72	71	imbi2d	$⊢ f = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y)))$
73	72	2ralbidv	$⊢ f = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)) \leftrightarrow \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y)))$
74	68 73	anbi12d	$⊢ f = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \to ((f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y))) \leftrightarrow ((j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y))))$
75	74	elabg	$⊢ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in V \to ((j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \leftrightarrow ((j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y))))$
76	67 75	syl	$⊢ (φ \land a \in A) \to ((j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \leftrightarrow ((j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (x) < (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) (y))))$
77	65 76	mpbird	$⊢ (φ \land a \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
78	5	a1i	$⊢ (φ \land a \in A) \to B = \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
79	77 78	eleqtrrd	$⊢ (φ \land a \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in B$
80	79 3	fmptd	$⊢ φ \to F : A ⟶ B$

Metamath Proof Explorer

Theorem sticksstones8

Proof