Metamath Proof Explorer

Theorem 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 ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
ballotth.mgtn ⊢ 𝑁 < 𝑀
ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
ballotlemg ⊢ ↑ = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
Assertion ballotlemfrc ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = ( 𝐶 ↑ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
7 ballotth.mgtn ⊢ 𝑁 < 𝑀
8 ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
9 ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
11 ballotlemg ⊢ ↑ = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
12 1 2 3 4 5 6 7 8 9 ballotlemsf1o ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) ) )
13 12 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
14 f1of1 ⊢ ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
15 13 14 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
16 15 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
17 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
18 17 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
19 18 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
20 elfzuz3 ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) )
21 19 20 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) )
22 elfzuz3 ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ( ℤ≥ ‘ 𝐽 ) )
23 22 adantl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ( ℤ≥ ‘ 𝐽 ) )
24 uztrn ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ ( ℤ≥ ‘ 𝐽 ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝐽 ) )
25 21 23 24 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝐽 ) )
26 fzss2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝐽 ) → ( 1 ... 𝐽 ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
27 25 26 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 1 ... 𝐽 ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
28 ssinss1 ⊢ ( ( 1 ... 𝐽 ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
29 27 28 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
30 f1ores ⊢ ( ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ↾ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) : ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) –1-1-onto→ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) )
31 16 29 30 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ↾ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) : ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) –1-1-onto→ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) )
32 ovex ⊢ ( 1 ... 𝐽 ) ∈ V
33 32 inex1 ⊢ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ∈ V
34 33 f1oen ⊢ ( ( ( 𝑆 ‘ 𝐶 ) ↾ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) : ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) –1-1-onto→ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) → ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ≈ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) )
35 hasheni ⊢ ( ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ≈ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) = ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) ) )
36 31 34 35 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) = ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) ) )
37 27 ssdifssd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
38 f1ores ⊢ ( ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ↾ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) : ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) –1-1-onto→ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) )
39 16 37 38 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ↾ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) : ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) –1-1-onto→ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) )
40 difexg ⊢ ( ( 1 ... 𝐽 ) ∈ V → ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ∈ V )
41 32 40 ax-mp ⊢ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ∈ V
42 41 f1oen ⊢ ( ( ( 𝑆 ‘ 𝐶 ) ↾ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) : ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) –1-1-onto→ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) → ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ≈ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) )
43 hasheni ⊢ ( ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ≈ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) = ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) ) )
44 39 42 43 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) = ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) ) )
45 36 44 oveq12d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) ) = ( ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) ) − ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) ) ) )
46 1 2 3 4 5 6 7 8 9 10 ballotlemro ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑅 ‘ 𝐶 ) ∈ 𝑂 )
47 46 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑅 ‘ 𝐶 ) ∈ 𝑂 )
48 elfzelz ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℤ )
49 48 adantl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ℤ )
50 1 2 3 4 5 47 49 ballotlemfval ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) ) )
51 fzfi ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin
52 eldifi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝐶 ∈ 𝑂 )
53 1 2 3 ballotlemelo ⊢ ( 𝐶 ∈ 𝑂 ↔ ( 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝐶 ) = 𝑀 ) )
54 53 simplbi ⊢ ( 𝐶 ∈ 𝑂 → 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
55 52 54 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
56 55 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
57 ssfi ⊢ ( ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 𝐶 ∈ Fin )
58 51 56 57 sylancr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐶 ∈ Fin )
59 fzfid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∈ Fin )
60 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval ⊢ ( ( 𝐶 ∈ Fin ∧ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∈ Fin ) → ( 𝐶 ↑ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) = ( ( ♯ ‘ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∖ 𝐶 ) ) ) )
61 58 59 60 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐶 ↑ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) = ( ( ♯ ‘ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∖ 𝐶 ) ) ) )
62 dff1o3 ⊢ ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) ↔ ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ Fun ◡ ( 𝑆 ‘ 𝐶 ) ) )
63 62 simprbi ⊢ ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) → Fun ◡ ( 𝑆 ‘ 𝐶 ) )
64 imain ⊢ ( Fun ◡ ( 𝑆 ‘ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ∩ ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) ) )
65 13 63 64 3syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ∩ ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) ) )
66 65 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ∩ ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) ) )
67 1 2 3 4 5 6 7 8 9 ballotlemsima ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) )
68 1 2 3 4 5 6 7 8 9 10 ballotlemscr ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) = 𝐶 )
69 68 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) = 𝐶 )
70 67 69 ineq12d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ∩ ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∩ 𝐶 ) )
71 66 70 eqtrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∩ 𝐶 ) )
72 71 fveq2d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) ) = ( ♯ ‘ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∩ 𝐶 ) ) )
73 imadif ⊢ ( Fun ◡ ( 𝑆 ‘ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ∖ ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) ) )
74 13 63 73 3syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ∖ ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) ) )
75 74 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ∖ ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) ) )
76 67 69 difeq12d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ∖ ( ( 𝑆 ‘ 𝐶 ) “ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∖ 𝐶 ) )
77 75 76 eqtrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) = ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∖ 𝐶 ) )
78 77 fveq2d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) ) = ( ♯ ‘ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∖ 𝐶 ) ) )
79 72 78 oveq12d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) ) − ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) ) ) = ( ( ♯ ‘ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∖ 𝐶 ) ) ) )
80 61 79 eqtr4d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐶 ↑ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) = ( ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∩ ( 𝑅 ‘ 𝐶 ) ) ) ) − ( ♯ ‘ ( ( 𝑆 ‘ 𝐶 ) “ ( ( 1 ... 𝐽 ) ∖ ( 𝑅 ‘ 𝐶 ) ) ) ) ) )
81 45 50 80 3eqtr4d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = ( 𝐶 ↑ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) )