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 a (i)$
35		nfcv	$⊢ \underline{Ⅎ} i a (l)$
36	33 34 35	cbvsum	$⊢ \sum_{i = 1}^{K + 1} a (i) = \sum_{l = 1}^{K + 1} a (l)$
37	29	simprd	$⊢ (φ \land a \in A) \to \sum_{i = 1}^{K + 1} a (i) = N$
38	36 37	eqtr3id	$⊢ (φ \land a \in A) \to \sum_{l = 1}^{K + 1} a (l) = N$
39	38	3adant3	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to \sum_{l = 1}^{K + 1} a (l) = N$
40	14 15 31 11 32 39	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)$
41	13 40	eqeltrrd	$⊢ (φ \land a \in A \land j \in (1 \dots K)) \to j + \sum_{l = 1}^{j} a (l) \in (1 \dots N + K)$
42	41	3expa	$⊢ ((φ \land a \in A) \land j \in (1 \dots K)) \to j + \sum_{l = 1}^{j} a (l) \in (1 \dots N + K)$
43		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))$
44	42 43	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)$
45	1	ad3antrrr	$⊢ (((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \to N \in ℕ_{0}$
46	45	adantr	$⊢ ((((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \land x < y) \to N \in ℕ_{0}$
47	2	ad3antrrr	$⊢ (((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \to K \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 K \in ℕ_{0}$
49	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))$
50	49	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))$
51	19 50	mpd	$⊢ (φ \land a \in A) \to (a : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} a (i) = N)$
52	51	simpld	$⊢ (φ \land a \in A) \to a : (1 \dots K + 1) ⟶ ℕ_{0}$
53	52	adantr	$⊢ ((φ \land a \in A) \land x \in (1 \dots K)) \to a : (1 \dots K + 1) ⟶ ℕ_{0}$
54	53	adantr	$⊢ (((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \to a : (1 \dots K + 1) ⟶ ℕ_{0}$
55	54	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}$
56		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)$
57		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)$
58		simpr	$⊢ ((((φ \land a \in A) \land x \in (1 \dots K)) \land y \in (1 \dots K)) \land x < y) \to x < y$
59	46 48 55 56 57 58 43	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)$
60	59	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))$
61	60	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))$
62	61	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))$
63	44 62	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)))$
64		fzfid	$⊢ (φ \land a \in A) \to (1 \dots K) \in Fin$
65	44 64	fexd	$⊢ (φ \land a \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in V$
66		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))$
67		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)$
68		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)$
69	67 68	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))$
70	69	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)))$
71	70	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)))$
72	66 71	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))))$
73	72	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))))$
74	65 73	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))))$
75	63 74	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)))\}$
76	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)))\}$
77	75 76	eleqtrrd	$⊢ (φ \land a \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in B$
78	77 3	fmptd	$⊢ φ \to F : A ⟶ B$

Metamath Proof Explorer

Theorem sticksstones8

Proof