Metamath Proof Explorer

Theorem ballotlemrinv

Description: R is its own inverse : it is an involution. (Contributed by Thierry Arnoux, 10-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⟼xO
ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
ballotth.mgtn ⊢N<M
ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
ballotth.r ⊢R=c∈O∖E⟼S⁡cc
Assertion ballotlemrinv ⊢R-1=R

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⟼xO
5 ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
6 ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
7 ballotth.mgtn ⊢N<M
8 ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
9 ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
10 ballotth.r ⊢R=c∈O∖E⟼S⁡cc
11 1 2 3 4 5 6 7 8 9 10 ballotlemrinv0 ⊢c∈O∖E∧d=S⁡cc→d∈O∖E∧c=S⁡dd
12 1 2 3 4 5 6 7 8 9 10 ballotlemrinv0 ⊢d∈O∖E∧c=S⁡dd→c∈O∖E∧d=S⁡cc
13 11 12 impbii ⊢c∈O∖E∧d=S⁡cc↔d∈O∖E∧c=S⁡dd
14 13 a1i ⊢⊤→c∈O∖E∧d=S⁡cc↔d∈O∖E∧c=S⁡dd
15 14 mptcnv ⊢⊤→c∈O∖E⟼S⁡cc-1=d∈O∖E⟼S⁡dd
16 15 mptru ⊢c∈O∖E⟼S⁡cc-1=d∈O∖E⟼S⁡dd
17 fveq2 ⊢d=c→S⁡d=S⁡c
18 id ⊢d=c→d=c
19 17 18 imaeq12d ⊢d=c→S⁡dd=S⁡cc
20 19 cbvmptv ⊢d∈O∖E⟼S⁡dd=c∈O∖E⟼S⁡cc
21 16 20 eqtri ⊢c∈O∖E⟼S⁡cc-1=c∈O∖E⟼S⁡cc
22 10 cnveqi ⊢R-1=c∈O∖E⟼S⁡cc-1
23 21 22 10 3eqtr4i ⊢R-1=R