sticksstones9

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

	Ref	Expression
Hypotheses	sticksstones9.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones9.2	$⊢ φ \to K = 0$
	sticksstones9.3	$⊢ G = (b \in B ⟼ if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))))$
	sticksstones9.4	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
	sticksstones9.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	sticksstones9	$⊢ φ \to G : B ⟶ A$

Proof

Step	Hyp	Ref	Expression
1		sticksstones9.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones9.2	$⊢ φ \to K = 0$
3		sticksstones9.3	$⊢ G = (b \in B ⟼ if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))))$
4		sticksstones9.4	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
5		sticksstones9.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	2	iftrued	$⊢ φ \to if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))) = \{⟨1, N⟩\}$
7	6	adantr	$⊢ (φ \land b \in B) \to if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))) = \{⟨1, N⟩\}$
8		eqid	$⊢ \{⟨1, N⟩\} = \{⟨1, N⟩\}$
9		1nn	$⊢ 1 \in ℕ$
10	9	a1i	$⊢ φ \to 1 \in ℕ$
11		fsng	$⊢ (1 \in ℕ \land N \in ℕ_{0}) \to (\{⟨1, N⟩\} : \{1\} ⟶ \{N\} \leftrightarrow \{⟨1, N⟩\} = \{⟨1, N⟩\})$
12	10 1 11	syl2anc	$⊢ φ \to (\{⟨1, N⟩\} : \{1\} ⟶ \{N\} \leftrightarrow \{⟨1, N⟩\} = \{⟨1, N⟩\})$
13	8 12	mpbiri	$⊢ φ \to \{⟨1, N⟩\} : \{1\} ⟶ \{N\}$
14	1	snssd	$⊢ φ \to \{N\} \subseteq ℕ_{0}$
15	13 14	jca	$⊢ φ \to (\{⟨1, N⟩\} : \{1\} ⟶ \{N\} \land \{N\} \subseteq ℕ_{0})$
16		fss	$⊢ (\{⟨1, N⟩\} : \{1\} ⟶ \{N\} \land \{N\} \subseteq ℕ_{0}) \to \{⟨1, N⟩\} : \{1\} ⟶ ℕ_{0}$
17	15 16	syl	$⊢ φ \to \{⟨1, N⟩\} : \{1\} ⟶ ℕ_{0}$
18	2	oveq1d	$⊢ φ \to K + 1 = 0 + 1$
19		0p1e1	$⊢ 0 + 1 = 1$
20	18 19	eqtrdi	$⊢ φ \to K + 1 = 1$
21	20	oveq2d	$⊢ φ \to (1 \dots K + 1) = (1 \dots 1)$
22		1zzd	$⊢ φ \to 1 \in ℤ$
23		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
24	22 23	syl	$⊢ φ \to (1 \dots 1) = \{1\}$
25	21 24	eqtrd	$⊢ φ \to (1 \dots K + 1) = \{1\}$
26	25	eqcomd	$⊢ φ \to \{1\} = (1 \dots K + 1)$
27	26	feq2d	$⊢ φ \to (\{⟨1, N⟩\} : \{1\} ⟶ ℕ_{0} \leftrightarrow \{⟨1, N⟩\} : (1 \dots K + 1) ⟶ ℕ_{0})$
28	17 27	mpbid	$⊢ φ \to \{⟨1, N⟩\} : (1 \dots K + 1) ⟶ ℕ_{0}$
29	25	sumeq1d	$⊢ φ \to \sum_{i = 1}^{K + 1} \{⟨1, N⟩\} (i) = \sum_{i \in \{1\}} \{⟨1, N⟩\} (i)$
30		fvsng	$⊢ (1 \in ℕ \land N \in ℕ_{0}) \to \{⟨1, N⟩\} (1) = N$
31	10 1 30	syl2anc	$⊢ φ \to \{⟨1, N⟩\} (1) = N$
32	1	nn0cnd	$⊢ φ \to N \in ℂ$
33	31 32	eqeltrd	$⊢ φ \to \{⟨1, N⟩\} (1) \in ℂ$
34	10 33	jca	$⊢ φ \to (1 \in ℕ \land \{⟨1, N⟩\} (1) \in ℂ)$
35		fveq2	$⊢ i = 1 \to \{⟨1, N⟩\} (i) = \{⟨1, N⟩\} (1)$
36	35	sumsn	$⊢ (1 \in ℕ \land \{⟨1, N⟩\} (1) \in ℂ) \to \sum_{i \in \{1\}} \{⟨1, N⟩\} (i) = \{⟨1, N⟩\} (1)$
37	34 36	syl	$⊢ φ \to \sum_{i \in \{1\}} \{⟨1, N⟩\} (i) = \{⟨1, N⟩\} (1)$
38	10 1	jca	$⊢ φ \to (1 \in ℕ \land N \in ℕ_{0})$
39	38 30	syl	$⊢ φ \to \{⟨1, N⟩\} (1) = N$
40	37 39	eqtrd	$⊢ φ \to \sum_{i \in \{1\}} \{⟨1, N⟩\} (i) = N$
41	29 40	eqtrd	$⊢ φ \to \sum_{i = 1}^{K + 1} \{⟨1, N⟩\} (i) = N$
42	28 41	jca	$⊢ φ \to (\{⟨1, N⟩\} : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} \{⟨1, N⟩\} (i) = N)$
43	42	adantr	$⊢ (φ \land b \in B) \to (\{⟨1, N⟩\} : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} \{⟨1, N⟩\} (i) = N)$
44		snex	$⊢ \{⟨1, N⟩\} \in V$
45		feq1	$⊢ g = \{⟨1, N⟩\} \to (g : (1 \dots K + 1) ⟶ ℕ_{0} \leftrightarrow \{⟨1, N⟩\} : (1 \dots K + 1) ⟶ ℕ_{0})$
46		simpl	$⊢ (g = \{⟨1, N⟩\} \land i \in (1 \dots K + 1)) \to g = \{⟨1, N⟩\}$
47	46	fveq1d	$⊢ (g = \{⟨1, N⟩\} \land i \in (1 \dots K + 1)) \to g (i) = \{⟨1, N⟩\} (i)$
48	47	sumeq2dv	$⊢ g = \{⟨1, N⟩\} \to \sum_{i = 1}^{K + 1} g (i) = \sum_{i = 1}^{K + 1} \{⟨1, N⟩\} (i)$
49	48	eqeq1d	$⊢ g = \{⟨1, N⟩\} \to (\sum_{i = 1}^{K + 1} g (i) = N \leftrightarrow \sum_{i = 1}^{K + 1} \{⟨1, N⟩\} (i) = N)$
50	45 49	anbi12d	$⊢ g = \{⟨1, N⟩\} \to ((g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N) \leftrightarrow (\{⟨1, N⟩\} : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} \{⟨1, N⟩\} (i) = N))$
51	50	elabg	$⊢ \{⟨1, N⟩\} \in V \to (\{⟨1, N⟩\} \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow (\{⟨1, N⟩\} : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} \{⟨1, N⟩\} (i) = N))$
52	44 51	ax-mp	$⊢ \{⟨1, N⟩\} \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow (\{⟨1, N⟩\} : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} \{⟨1, N⟩\} (i) = N)$
53	43 52	sylibr	$⊢ (φ \land b \in B) \to \{⟨1, N⟩\} \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
54	4	a1i	$⊢ (φ \land b \in B) \to A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
55	53 54	eleqtrrd	$⊢ (φ \land b \in B) \to \{⟨1, N⟩\} \in A$
56	7 55	eqeltrd	$⊢ (φ \land b \in B) \to if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))) \in A$
57	56 3	fmptd	$⊢ φ \to G : B ⟶ A$

Metamath Proof Explorer

Theorem sticksstones9

Proof