ballotlemfrc

Description: Express the value of ( F( RC ) ) in terms of the newly defined .^ . (Contributed by Thierry Arnoux, 21-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) ⟼ 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])$
	ballotlemg	$⊢ \underset{˙}{\times} = (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|)$
Assertion	ballotlemfrc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) = C \underset{˙}{\times} (S (C) (J) \dots I (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) ⟼ 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		ballotlemg	$⊢ \underset{˙}{\times} = (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|)$
12	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))$
13	12	simpld	$⊢ C \in (O ∖ E) \to S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N)$
14		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)$
15	13 14	syl	$⊢ C \in (O ∖ E) \to S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N)$
16	15	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N)$
17	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)$
18	17	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
19	18	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in (1 \dots M + N)$
20		elfzuz3	$⊢ I (C) \in (1 \dots M + N) \to M + N \in ℤ_{\geq I (C)}$
21	19 20	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to M + N \in ℤ_{\geq I (C)}$
22		elfzuz3	$⊢ J \in (1 \dots I (C)) \to I (C) \in ℤ_{\geq J}$
23	22	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in ℤ_{\geq J}$
24		uztrn	$⊢ (M + N \in ℤ_{\geq I (C)} \land I (C) \in ℤ_{\geq J}) \to M + N \in ℤ_{\geq J}$
25	21 23 24	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to M + N \in ℤ_{\geq J}$
26		fzss2	$⊢ M + N \in ℤ_{\geq J} \to (1 \dots J) \subseteq (1 \dots M + N)$
27	25 26	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (1 \dots J) \subseteq (1 \dots M + N)$
28		ssinss1	$⊢ (1 \dots J) \subseteq (1 \dots M + N) \to (1 \dots J) \cap R (C) \subseteq (1 \dots M + N)$
29	27 28	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (1 \dots J) \cap R (C) \subseteq (1 \dots M + N)$
30		f1ores	$⊢ (S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N) \land (1 \dots J) \cap R (C) \subseteq (1 \dots M + N)) \to ({S (C) ↾}_{((1 \dots J) \cap R (C))}) : (1 \dots J) \cap R (C) \underset{1-1 onto}{⟶} S (C) [(1 \dots J) \cap R (C)]$
31	16 29 30	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to ({S (C) ↾}_{((1 \dots J) \cap R (C))}) : (1 \dots J) \cap R (C) \underset{1-1 onto}{⟶} S (C) [(1 \dots J) \cap R (C)]$
32		ovex	$⊢ (1 \dots J) \in V$
33	32	inex1	$⊢ (1 \dots J) \cap R (C) \in V$
34	33	f1oen	$⊢ ({S (C) ↾}_{((1 \dots J) \cap R (C))}) : (1 \dots J) \cap R (C) \underset{1-1 onto}{⟶} S (C) [(1 \dots J) \cap R (C)] \to ((1 \dots J) \cap R (C)) \approx S (C) [(1 \dots J) \cap R (C)]$
35		hasheni	$⊢ ((1 \dots J) \cap R (C)) \approx S (C) [(1 \dots J) \cap R (C)] \to \|(1 \dots J) \cap R (C)\| = \|S (C) [(1 \dots J) \cap R (C)]\|$
36	31 34 35	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to \|(1 \dots J) \cap R (C)\| = \|S (C) [(1 \dots J) \cap R (C)]\|$
37	27	ssdifssd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (1 \dots J) ∖ R (C) \subseteq (1 \dots M + N)$
38		f1ores	$⊢ (S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N) \land (1 \dots J) ∖ R (C) \subseteq (1 \dots M + N)) \to ({S (C) ↾}_{((1 \dots J) ∖ R (C))}) : (1 \dots J) ∖ R (C) \underset{1-1 onto}{⟶} S (C) [(1 \dots J) ∖ R (C)]$
39	16 37 38	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to ({S (C) ↾}_{((1 \dots J) ∖ R (C))}) : (1 \dots J) ∖ R (C) \underset{1-1 onto}{⟶} S (C) [(1 \dots J) ∖ R (C)]$
40		difexg	$⊢ (1 \dots J) \in V \to (1 \dots J) ∖ R (C) \in V$
41	32 40	ax-mp	$⊢ (1 \dots J) ∖ R (C) \in V$
42	41	f1oen	$⊢ ({S (C) ↾}_{((1 \dots J) ∖ R (C))}) : (1 \dots J) ∖ R (C) \underset{1-1 onto}{⟶} S (C) [(1 \dots J) ∖ R (C)] \to ((1 \dots J) ∖ R (C)) \approx S (C) [(1 \dots J) ∖ R (C)]$
43		hasheni	$⊢ ((1 \dots J) ∖ R (C)) \approx S (C) [(1 \dots J) ∖ R (C)] \to \|(1 \dots J) ∖ R (C)\| = \|S (C) [(1 \dots J) ∖ R (C)]\|$
44	39 42 43	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to \|(1 \dots J) ∖ R (C)\| = \|S (C) [(1 \dots J) ∖ R (C)]\|$
45	36 44	oveq12d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to \|(1 \dots J) \cap R (C)\| - \|(1 \dots J) ∖ R (C)\| = \|S (C) [(1 \dots J) \cap R (C)]\| - \|S (C) [(1 \dots J) ∖ R (C)]\|$
46	1 2 3 4 5 6 7 8 9 10	ballotlemro	$⊢ C \in (O ∖ E) \to R (C) \in O$
47	46	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to R (C) \in O$
48		elfzelz	$⊢ J \in (1 \dots I (C)) \to J \in ℤ$
49	48	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in ℤ$
50	1 2 3 4 5 47 49	ballotlemfval	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) = \|(1 \dots J) \cap R (C)\| - \|(1 \dots J) ∖ R (C)\|$
51		fzfi	$⊢ (1 \dots M + N) \in Fin$
52		eldifi	$⊢ C \in (O ∖ E) \to C \in O$
53	1 2 3	ballotlemelo	$⊢ C \in O \leftrightarrow (C \subseteq (1 \dots M + N) \land \|C\| = M)$
54	53	simplbi	$⊢ C \in O \to C \subseteq (1 \dots M + N)$
55	52 54	syl	$⊢ C \in (O ∖ E) \to C \subseteq (1 \dots M + N)$
56	55	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to C \subseteq (1 \dots M + N)$
57		ssfi	$⊢ ((1 \dots M + N) \in Fin \land C \subseteq (1 \dots M + N)) \to C \in Fin$
58	51 56 57	sylancr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to C \in Fin$
59		fzfid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (S (C) (J) \dots I (C)) \in Fin$
60	1 2 3 4 5 6 7 8 9 10 11	ballotlemgval	$⊢ (C \in Fin \land (S (C) (J) \dots I (C)) \in Fin) \to C \underset{˙}{\times} (S (C) (J) \dots I (C)) = \|(S (C) (J) \dots I (C)) \cap C\| - \|(S (C) (J) \dots I (C)) ∖ C\|$
61	58 59 60	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to C \underset{˙}{\times} (S (C) (J) \dots I (C)) = \|(S (C) (J) \dots I (C)) \cap C\| - \|(S (C) (J) \dots I (C)) ∖ C\|$
62		dff1o3	$⊢ S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \leftrightarrow (S (C) : (1 \dots M + N) \underset{onto}{⟶} (1 \dots M + N) \land Fun {S (C)}^{-1})$
63	62	simprbi	$⊢ S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \to Fun {S (C)}^{-1}$
64		imain	$⊢ Fun {S (C)}^{-1} \to S (C) [(1 \dots J) \cap R (C)] = S (C) [(1 \dots J)] \cap S (C) [R (C)]$
65	13 63 64	3syl	$⊢ C \in (O ∖ E) \to S (C) [(1 \dots J) \cap R (C)] = S (C) [(1 \dots J)] \cap S (C) [R (C)]$
66	65	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J) \cap R (C)] = S (C) [(1 \dots J)] \cap S (C) [R (C)]$
67	1 2 3 4 5 6 7 8 9	ballotlemsima	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J)] = (S (C) (J) \dots I (C))$
68	1 2 3 4 5 6 7 8 9 10	ballotlemscr	$⊢ C \in (O ∖ E) \to S (C) [R (C)] = C$
69	68	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [R (C)] = C$
70	67 69	ineq12d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J)] \cap S (C) [R (C)] = (S (C) (J) \dots I (C)) \cap C$
71	66 70	eqtrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J) \cap R (C)] = (S (C) (J) \dots I (C)) \cap C$
72	71	fveq2d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to \|S (C) [(1 \dots J) \cap R (C)]\| = \|(S (C) (J) \dots I (C)) \cap C\|$
73		imadif	$⊢ Fun {S (C)}^{-1} \to S (C) [(1 \dots J) ∖ R (C)] = S (C) [(1 \dots J)] ∖ S (C) [R (C)]$
74	13 63 73	3syl	$⊢ C \in (O ∖ E) \to S (C) [(1 \dots J) ∖ R (C)] = S (C) [(1 \dots J)] ∖ S (C) [R (C)]$
75	74	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J) ∖ R (C)] = S (C) [(1 \dots J)] ∖ S (C) [R (C)]$
76	67 69	difeq12d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J)] ∖ S (C) [R (C)] = (S (C) (J) \dots I (C)) ∖ C$
77	75 76	eqtrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J) ∖ R (C)] = (S (C) (J) \dots I (C)) ∖ C$
78	77	fveq2d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to \|S (C) [(1 \dots J) ∖ R (C)]\| = \|(S (C) (J) \dots I (C)) ∖ C\|$
79	72 78	oveq12d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to \|S (C) [(1 \dots J) \cap R (C)]\| - \|S (C) [(1 \dots J) ∖ R (C)]\| = \|(S (C) (J) \dots I (C)) \cap C\| - \|(S (C) (J) \dots I (C)) ∖ C\|$
80	61 79	eqtr4d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to C \underset{˙}{\times} (S (C) (J) \dots I (C)) = \|S (C) [(1 \dots J) \cap R (C)]\| - \|S (C) [(1 \dots J) ∖ R (C)]\|$
81	45 50 80	3eqtr4d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) = C \underset{˙}{\times} (S (C) (J) \dots I (C))$

Metamath Proof Explorer

Theorem ballotlemfrc

Proof