Metamath Proof Explorer


Theorem ballotlemscr

Description: The image of ( RC ) by ( SC ) . (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 𝑅 = ( 𝑐 ∈ ( 𝑂𝐸 ) ↦ ( ( 𝑆𝑐 ) “ 𝑐 ) )
Assertion ballotlemscr ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝑆𝐶 ) “ ( 𝑅𝐶 ) ) = 𝐶 )

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 1 2 3 4 5 6 7 8 9 10 ballotlemrval ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 𝑅𝐶 ) = ( ( 𝑆𝐶 ) “ 𝐶 ) )
12 11 imaeq2d ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝑆𝐶 ) “ ( 𝑅𝐶 ) ) = ( ( 𝑆𝐶 ) “ ( ( 𝑆𝐶 ) “ 𝐶 ) ) )
13 1 2 3 4 5 6 7 8 9 ballotlemsf1o ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝑆𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( 𝑆𝐶 ) = ( 𝑆𝐶 ) ) )
14 13 simprd ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 𝑆𝐶 ) = ( 𝑆𝐶 ) )
15 14 imaeq1d ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝑆𝐶 ) “ ( ( 𝑆𝐶 ) “ 𝐶 ) ) = ( ( 𝑆𝐶 ) “ ( ( 𝑆𝐶 ) “ 𝐶 ) ) )
16 13 simpld ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 𝑆𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
17 f1of1 ( ( 𝑆𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝑆𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
18 16 17 syl ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 𝑆𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
19 eldifi ( 𝐶 ∈ ( 𝑂𝐸 ) → 𝐶𝑂 )
20 1 2 3 ballotlemelo ( 𝐶𝑂 ↔ ( 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝐶 ) = 𝑀 ) )
21 20 simplbi ( 𝐶𝑂𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
22 19 21 syl ( 𝐶 ∈ ( 𝑂𝐸 ) → 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
23 f1imacnv ( ( ( 𝑆𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆𝐶 ) “ ( ( 𝑆𝐶 ) “ 𝐶 ) ) = 𝐶 )
24 18 22 23 syl2anc ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝑆𝐶 ) “ ( ( 𝑆𝐶 ) “ 𝐶 ) ) = 𝐶 )
25 12 15 24 3eqtr2d ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝑆𝐶 ) “ ( 𝑅𝐶 ) ) = 𝐶 )