Metamath Proof Explorer


Theorem ballotlemrv

Description: Value of R evaluated at J . (Contributed by Thierry Arnoux, 17-Apr-2017)

Ref Expression
Hypotheses ballotth.m M
ballotth.n N
ballotth.o O = c 𝒫 1 M + N | c = M
ballotth.p P = x 𝒫 O x O
ballotth.f F = c O i 1 i c 1 i c
ballotth.e E = c O | i 1 M + N 0 < F c i
ballotth.mgtn N < M
ballotth.i I = c O E sup k 1 M + N | F c k = 0 <
ballotth.s S = c O E i 1 M + N if i I c I c + 1 - i i
ballotth.r R = c O E S c c
Assertion ballotlemrv C O E J 1 M + N J R C if J I C I C + 1 - J J C

Proof

Step Hyp Ref Expression
1 ballotth.m M
2 ballotth.n N
3 ballotth.o O = c 𝒫 1 M + N | c = M
4 ballotth.p P = x 𝒫 O x O
5 ballotth.f F = c O i 1 i c 1 i c
6 ballotth.e E = c O | i 1 M + N 0 < F c i
7 ballotth.mgtn N < M
8 ballotth.i I = c O E sup k 1 M + N | F c k = 0 <
9 ballotth.s S = c O E i 1 M + N if i I c I c + 1 - i i
10 ballotth.r R = c O E S c c
11 simpl C O E J 1 M + N C O E
12 1 2 3 4 5 6 7 8 9 ballotlemsf1o C O E S C : 1 M + N 1-1 onto 1 M + N S C -1 = S C
13 12 simpld C O E S C : 1 M + N 1-1 onto 1 M + N
14 f1ofun S C : 1 M + N 1-1 onto 1 M + N Fun S C
15 11 13 14 3syl C O E J 1 M + N Fun S C
16 simpr C O E J 1 M + N J 1 M + N
17 f1odm S C : 1 M + N 1-1 onto 1 M + N dom S C = 1 M + N
18 11 13 17 3syl C O E J 1 M + N dom S C = 1 M + N
19 16 18 eleqtrrd C O E J 1 M + N J dom S C
20 fvimacnv Fun S C J dom S C S C J C J S C -1 C
21 15 19 20 syl2anc C O E J 1 M + N S C J C J S C -1 C
22 1 2 3 4 5 6 7 8 9 ballotlemsv C O E J 1 M + N S C J = if J I C I C + 1 - J J
23 22 eleq1d C O E J 1 M + N S C J C if J I C I C + 1 - J J C
24 12 simprd C O E S C -1 = S C
25 24 imaeq1d C O E S C -1 C = S C C
26 1 2 3 4 5 6 7 8 9 10 ballotlemrval C O E R C = S C C
27 25 26 eqtr4d C O E S C -1 C = R C
28 27 eleq2d C O E J S C -1 C J R C
29 11 28 syl C O E J 1 M + N J S C -1 C J R C
30 21 23 29 3bitr3rd C O E J 1 M + N J R C if J I C I C + 1 - J J C