ballotlemsf1o

Description: The defined S is a bijection, and an involution. (Contributed by Thierry Arnoux, 14-Apr-2017)

	Ref	Expression
Hypotheses	ballotth.m	$⊢ M \in ℕ$
	ballotth.n	$⊢ N \in ℕ$
	ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
	ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
	ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
	ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
	ballotth.mgtn	$⊢ N < M$
	ballotth.i	$⊢ I = (c \in (O ∖ E) ⟼ inf (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
	ballotth.s	$⊢ S = (c \in (O ∖ E) ⟼ (i \in (1 \dots M + N) ⟼ if (i \leq I (c), I (c) + 1 - i, i)))$
Assertion	ballotlemsf1o	$⊢ C \in (O ∖ E) \to (S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \land {S (C)}^{-1} = S (C))$

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	$⊢ M \in ℕ$
2		ballotth.n	$⊢ N \in ℕ$
3		ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
4		ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
5		ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
6		ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
7		ballotth.mgtn	$⊢ N < M$
8		ballotth.i	$⊢ I = (c \in (O ∖ E) ⟼ inf (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
9		ballotth.s	$⊢ S = (c \in (O ∖ E) ⟼ (i \in (1 \dots M + N) ⟼ if (i \leq I (c), I (c) + 1 - i, i)))$
10	1 2 3 4 5 6 7 8 9	ballotlemsval	$⊢ C \in (O ∖ E) \to S (C) = (i \in (1 \dots M + N) ⟼ if (i \leq I (C), I (C) + 1 - i, i))$
11	1 2 3 4 5 6 7 8 9	ballotlemsv	$⊢ (C \in (O ∖ E) \land i \in (1 \dots M + N)) \to S (C) (i) = if (i \leq I (C), I (C) + 1 - i, i)$
12	1 2 3 4 5 6 7 8 9	ballotlemsdom	$⊢ (C \in (O ∖ E) \land i \in (1 \dots M + N)) \to S (C) (i) \in (1 \dots M + N)$
13	11 12	eqeltrrd	$⊢ (C \in (O ∖ E) \land i \in (1 \dots M + N)) \to if (i \leq I (C), I (C) + 1 - i, i) \in (1 \dots M + N)$
14	1 2 3 4 5 6 7 8 9	ballotlemsv	$⊢ (C \in (O ∖ E) \land j \in (1 \dots M + N)) \to S (C) (j) = if (j \leq I (C), I (C) + 1 - j, j)$
15	1 2 3 4 5 6 7 8 9	ballotlemsdom	$⊢ (C \in (O ∖ E) \land j \in (1 \dots M + N)) \to S (C) (j) \in (1 \dots M + N)$
16	14 15	eqeltrrd	$⊢ (C \in (O ∖ E) \land j \in (1 \dots M + N)) \to if (j \leq I (C), I (C) + 1 - j, j) \in (1 \dots M + N)$
17		oveq2	$⊢ i = I (C) + 1 - j \to I (C) + 1 - i = I (C) + 1 - (I (C) + 1 - j)$
18		id	$⊢ i = j \to i = j$
19		breq1	$⊢ i = I (C) + 1 - j \to (i \leq I (C) \leftrightarrow I (C) + 1 - j \leq I (C))$
20		breq1	$⊢ i = j \to (i \leq I (C) \leftrightarrow j \leq I (C))$
21	1 2 3 4 5 6 7 8	ballotlemiex	$⊢ C \in (O ∖ E) \to (I (C) \in (1 \dots M + N) \land F (C) (I (C)) = 0)$
22	21	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
23		elfzelz	$⊢ I (C) \in (1 \dots M + N) \to I (C) \in ℤ$
24	23	peano2zd	$⊢ I (C) \in (1 \dots M + N) \to I (C) + 1 \in ℤ$
25	22 24	syl	$⊢ C \in (O ∖ E) \to I (C) + 1 \in ℤ$
26	25	zcnd	$⊢ C \in (O ∖ E) \to I (C) + 1 \in ℂ$
27	26	adantr	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to I (C) + 1 \in ℂ$
28		elfzelz	$⊢ j \in (1 \dots M + N) \to j \in ℤ$
29	28	zcnd	$⊢ j \in (1 \dots M + N) \to j \in ℂ$
30	29	ad2antll	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to j \in ℂ$
31	27 30	nncand	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to I (C) + 1 - (I (C) + 1 - j) = j$
32	31	eqcomd	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to j = I (C) + 1 - (I (C) + 1 - j)$
33	22 23	syl	$⊢ C \in (O ∖ E) \to I (C) \in ℤ$
34	33	adantr	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to I (C) \in ℤ$
35		elfznn	$⊢ j \in (1 \dots M + N) \to j \in ℕ$
36	35	ad2antll	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to j \in ℕ$
37	34 36	ltesubnnd	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to I (C) + 1 - j \leq I (C)$
38	37	adantr	$⊢ ((C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \land j \leq I (C)) \to I (C) + 1 - j \leq I (C)$
39		vex	$⊢ j \in V$
40	39	a1i	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to j \in V$
41		ovexd	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to I (C) + 1 - j \in V$
42	17 18 19 20 32 38 40 41	ifeqeqx	$⊢ ((C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \land i = if (j \leq I (C), I (C) + 1 - j, j)) \to j = if (i \leq I (C), I (C) + 1 - i, i)$
43		oveq2	$⊢ j = I (C) + 1 - i \to I (C) + 1 - j = I (C) + 1 - (I (C) + 1 - i)$
44		id	$⊢ j = i \to j = i$
45		breq1	$⊢ j = I (C) + 1 - i \to (j \leq I (C) \leftrightarrow I (C) + 1 - i \leq I (C))$
46		breq1	$⊢ j = i \to (j \leq I (C) \leftrightarrow i \leq I (C))$
47		elfzelz	$⊢ i \in (1 \dots M + N) \to i \in ℤ$
48	47	zcnd	$⊢ i \in (1 \dots M + N) \to i \in ℂ$
49	48	ad2antrl	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to i \in ℂ$
50	27 49	nncand	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to I (C) + 1 - (I (C) + 1 - i) = i$
51	50	eqcomd	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to i = I (C) + 1 - (I (C) + 1 - i)$
52	34	adantr	$⊢ ((C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \land i \leq I (C)) \to I (C) \in ℤ$
53		simplrl	$⊢ ((C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \land i \leq I (C)) \to i \in (1 \dots M + N)$
54		elfznn	$⊢ i \in (1 \dots M + N) \to i \in ℕ$
55	53 54	syl	$⊢ ((C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \land i \leq I (C)) \to i \in ℕ$
56	52 55	ltesubnnd	$⊢ ((C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \land i \leq I (C)) \to I (C) + 1 - i \leq I (C)$
57		vex	$⊢ i \in V$
58	57	a1i	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to i \in V$
59		ovexd	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to I (C) + 1 - i \in V$
60	43 44 45 46 51 56 58 59	ifeqeqx	$⊢ ((C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \land j = if (i \leq I (C), I (C) + 1 - i, i)) \to i = if (j \leq I (C), I (C) + 1 - j, j)$
61	42 60	impbida	$⊢ (C \in (O ∖ E) \land (i \in (1 \dots M + N) \land j \in (1 \dots M + N))) \to (i = if (j \leq I (C), I (C) + 1 - j, j) \leftrightarrow j = if (i \leq I (C), I (C) + 1 - i, i))$
62	10 13 16 61	f1o3d	$⊢ C \in (O ∖ E) \to (S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \land {S (C)}^{-1} = (j \in (1 \dots M + N) ⟼ if (j \leq I (C), I (C) + 1 - j, j)))$
63	62	simpld	$⊢ C \in (O ∖ E) \to S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N)$
64		oveq2	$⊢ i = j \to I (C) + 1 - i = I (C) + 1 - j$
65	20 64 18	ifbieq12d	$⊢ i = j \to if (i \leq I (C), I (C) + 1 - i, i) = if (j \leq I (C), I (C) + 1 - j, j)$
66	65	cbvmptv	$⊢ (i \in (1 \dots M + N) ⟼ if (i \leq I (C), I (C) + 1 - i, i)) = (j \in (1 \dots M + N) ⟼ if (j \leq I (C), I (C) + 1 - j, j))$
67	66	a1i	$⊢ C \in (O ∖ E) \to (i \in (1 \dots M + N) ⟼ if (i \leq I (C), I (C) + 1 - i, i)) = (j \in (1 \dots M + N) ⟼ if (j \leq I (C), I (C) + 1 - j, j))$
68	62	simprd	$⊢ C \in (O ∖ E) \to {S (C)}^{-1} = (j \in (1 \dots M + N) ⟼ if (j \leq I (C), I (C) + 1 - j, j))$
69	67 10 68	3eqtr4rd	$⊢ C \in (O ∖ E) \to {S (C)}^{-1} = S (C)$
70	63 69	jca	$⊢ C \in (O ∖ E) \to (S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \land {S (C)}^{-1} = S (C))$

Metamath Proof Explorer

Theorem ballotlemsf1o

Proof