ballotlemrinv0

	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) ⟼ sup (\{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)))$
	ballotth.r	$⊢ R = (c \in (O ∖ E) ⟼ S (c) [c])$
Assertion	ballotlemrinv0	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to (D \in (O ∖ E) \land C = S (D) [D])$

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) ⟼ sup (\{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		ballotth.r	$⊢ R = (c \in (O ∖ E) ⟼ S (c) [c])$
11	1 2 3 4 5 6 7 8 9 10	ballotlemrval	$⊢ C \in (O ∖ E) \to R (C) = S (C) [C]$
12	11	adantr	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to R (C) = S (C) [C]$
13		simpr	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to D = S (C) [C]$
14	12 13	eqtr4d	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to R (C) = D$
15	1 2 3 4 5 6 7 8 9 10	ballotlemrc	$⊢ C \in (O ∖ E) \to R (C) \in (O ∖ E)$
16	15	adantr	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to R (C) \in (O ∖ E)$
17	14 16	eqeltrrd	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to D \in (O ∖ E)$
18	1 2 3 4 5 6 7 8 9	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))$
19	18	simprd	$⊢ C \in (O ∖ E) \to {S (C)}^{-1} = S (C)$
20	19	adantr	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to {S (C)}^{-1} = S (C)$
21	20	eqcomd	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to S (C) = {S (C)}^{-1}$
22	21 13	imaeq12d	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to S (C) [D] = {S (C)}^{-1} [S (C) [C]]$
23		simpl	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to C \in (O ∖ E)$
24	1 2 3 4 5 6 7 8 9 10	ballotlemirc	$⊢ C \in (O ∖ E) \to I (R (C)) = I (C)$
25	24	adantr	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to I (R (C)) = I (C)$
26	14	fveq2d	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to I (R (C)) = I (D)$
27	25 26	eqtr3d	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to I (C) = I (D)$
28	1 2 3 4 5 6 7 8 9	ballotlemieq	$⊢ (C \in (O ∖ E) \land D \in (O ∖ E) \land I (C) = I (D)) \to S (C) = S (D)$
29	23 17 27 28	syl3anc	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to S (C) = S (D)$
30	29	imaeq1d	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to S (C) [D] = S (D) [D]$
31	18	simpld	$⊢ C \in (O ∖ E) \to S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N)$
32		f1of1	$⊢ S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \to S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N)$
33	23 31 32	3syl	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N)$
34		eldifi	$⊢ C \in (O ∖ E) \to C \in O$
35	1 2 3	ballotlemelo	$⊢ C \in O \leftrightarrow (C \subseteq (1 \dots M + N) \land \|C\| = M)$
36	35	simplbi	$⊢ C \in O \to C \subseteq (1 \dots M + N)$
37	23 34 36	3syl	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to C \subseteq (1 \dots M + N)$
38		f1imacnv	$⊢ (S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N) \land C \subseteq (1 \dots M + N)) \to {S (C)}^{-1} [S (C) [C]] = C$
39	33 37 38	syl2anc	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to {S (C)}^{-1} [S (C) [C]] = C$
40	22 30 39	3eqtr3rd	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to C = S (D) [D]$
41	17 40	jca	$⊢ (C \in (O ∖ E) \land D = S (C) [C]) \to (D \in (O ∖ E) \land C = S (D) [D])$

Metamath Proof Explorer

Theorem ballotlemrinv0

Proof