Metamath Proof Explorer

Theorem ballotlemrinv0

Description: Lemma for ballotlemrinv . (Contributed by Thierry Arnoux, 18-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 ballotlemrinv0 ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝐷 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐶 = ( ( 𝑆 ‘ 𝐷 ) “ 𝐷 ) ) )

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 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝑅 ‘ 𝐶 ) = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) )
13 simpr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) )
14 12 13 eqtr4d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝑅 ‘ 𝐶 ) = 𝐷 )
15 1 2 3 4 5 6 7 8 9 10 ballotlemrc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑅 ‘ 𝐶 ) ∈ ( 𝑂 ∖ 𝐸 ) )
16 15 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝑅 ‘ 𝐶 ) ∈ ( 𝑂 ∖ 𝐸 ) )
17 14 16 eqeltrrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → 𝐷 ∈ ( 𝑂 ∖ 𝐸 ) )
18 1 2 3 4 5 6 7 8 9 ballotlemsf1o ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) ) )
19 18 simprd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) )
20 19 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) )
21 20 eqcomd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝑆 ‘ 𝐶 ) = ◡ ( 𝑆 ‘ 𝐶 ) )
22 21 13 imaeq12d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) “ 𝐷 ) = ( ◡ ( 𝑆 ‘ 𝐶 ) “ ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) )
23 simpl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) )
24 1 2 3 4 5 6 7 8 9 10 ballotlemirc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐶 ) ) = ( 𝐼 ‘ 𝐶 ) )
25 24 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐶 ) ) = ( 𝐼 ‘ 𝐶 ) )
26 14 fveq2d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐶 ) ) = ( 𝐼 ‘ 𝐷 ) )
27 25 26 eqtr3d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) = ( 𝐼 ‘ 𝐷 ) )
28 1 2 3 4 5 6 7 8 9 ballotlemieq ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) = ( 𝐼 ‘ 𝐷 ) ) → ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐷 ) )
29 23 17 27 28 syl3anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐷 ) )
30 29 imaeq1d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) “ 𝐷 ) = ( ( 𝑆 ‘ 𝐷 ) “ 𝐷 ) )
31 18 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
32 f1of1 ⊢ ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
33 23 31 32 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
34 eldifi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝐶 ∈ 𝑂 )
35 1 2 3 ballotlemelo ⊢ ( 𝐶 ∈ 𝑂 ↔ ( 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝐶 ) = 𝑀 ) )
36 35 simplbi ⊢ ( 𝐶 ∈ 𝑂 → 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
37 23 34 36 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
38 f1imacnv ⊢ ( ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ◡ ( 𝑆 ‘ 𝐶 ) “ ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) = 𝐶 )
39 33 37 38 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( ◡ ( 𝑆 ‘ 𝐶 ) “ ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) = 𝐶 )
40 22 30 39 3eqtr3rd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → 𝐶 = ( ( 𝑆 ‘ 𝐷 ) “ 𝐷 ) )
41 17 40 jca ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐷 = ( ( 𝑆 ‘ 𝐶 ) “ 𝐶 ) ) → ( 𝐷 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐶 = ( ( 𝑆 ‘ 𝐷 ) “ 𝐷 ) ) )