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 ⟼ 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 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 ⟼ 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 1 2 3 4 5 6 7 8 9 10 ballotlemrinv0 ⊢ c ∈ O ∖ E ∧ d = S ⁡ c c → d ∈ O ∖ E ∧ c = S ⁡ d d
12 1 2 3 4 5 6 7 8 9 10 ballotlemrinv0 ⊢ d ∈ O ∖ E ∧ c = S ⁡ d d → c ∈ O ∖ E ∧ d = S ⁡ c c
13 11 12 impbii ⊢ c ∈ O ∖ E ∧ d = S ⁡ c c ↔ d ∈ O ∖ E ∧ c = S ⁡ d d
14 13 a1i ⊢ ⊤ → c ∈ O ∖ E ∧ d = S ⁡ c c ↔ d ∈ O ∖ E ∧ c = S ⁡ d d
15 14 mptcnv ⊢ ⊤ → c ∈ O ∖ E ⟼ S ⁡ c c -1 = d ∈ O ∖ E ⟼ S ⁡ d d
16 15 mptru ⊢ c ∈ O ∖ E ⟼ S ⁡ c c -1 = d ∈ O ∖ E ⟼ S ⁡ d d
17 fveq2 ⊢ d = c → S ⁡ d = S ⁡ c
18 id ⊢ d = c → d = c
19 17 18 imaeq12d ⊢ d = c → S ⁡ d d = S ⁡ c c
20 19 cbvmptv ⊢ d ∈ O ∖ E ⟼ S ⁡ d d = c ∈ O ∖ E ⟼ S ⁡ c c
21 16 20 eqtri ⊢ c ∈ O ∖ E ⟼ S ⁡ c c -1 = c ∈ O ∖ E ⟼ S ⁡ c c
22 10 cnveqi ⊢ R -1 = c ∈ O ∖ E ⟼ S ⁡ c c -1
23 21 22 10 3eqtr4i ⊢ R -1 = R