Metamath Proof Explorer

Theorem ballotlemscr

Description: The image of ( RC ) by ( SC ) . (Contributed by Thierry Arnoux, 21-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 ballotlemscr ⊢ C ∈ O ∖ E → S ⁡ C R ⁡ C = C

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 ballotlemrval ⊢ C ∈ O ∖ E → R ⁡ C = S ⁡ C C
12 11 imaeq2d ⊢ C ∈ O ∖ E → S ⁡ C R ⁡ C = S ⁡ C S ⁡ C C
13 1 2 3 4 5 6 7 8 9 ballotlemsf1o ⊢ C ∈ O ∖ E → S ⁡ C : 1 … M + N ⟶ 1-1 onto 1 … M + N ∧ S ⁡ C -1 = S ⁡ C
14 13 simprd ⊢ C ∈ O ∖ E → S ⁡ C -1 = S ⁡ C
15 14 imaeq1d ⊢ C ∈ O ∖ E → S ⁡ C -1 S ⁡ C C = S ⁡ C S ⁡ C C
16 13 simpld ⊢ C ∈ O ∖ E → S ⁡ C : 1 … M + N ⟶ 1-1 onto 1 … M + N
17 f1of1 ⊢ S ⁡ C : 1 … M + N ⟶ 1-1 onto 1 … M + N → S ⁡ C : 1 … M + N ⟶ 1-1 1 … M + N
18 16 17 syl ⊢ C ∈ O ∖ E → S ⁡ C : 1 … M + N ⟶ 1-1 1 … M + N
19 eldifi ⊢ C ∈ O ∖ E → C ∈ O
20 1 2 3 ballotlemelo ⊢ C ∈ O ↔ C ⊆ 1 … M + N ∧ C = M
21 20 simplbi ⊢ C ∈ O → C ⊆ 1 … M + N
22 19 21 syl ⊢ C ∈ O ∖ E → C ⊆ 1 … M + N
23 f1imacnv ⊢ S ⁡ C : 1 … M + N ⟶ 1-1 1 … M + N ∧ C ⊆ 1 … M + N → S ⁡ C -1 S ⁡ C C = C
24 18 22 23 syl2anc ⊢ C ∈ O ∖ E → S ⁡ C -1 S ⁡ C C = C
25 12 15 24 3eqtr2d ⊢ C ∈ O ∖ E → S ⁡ C R ⁡ C = C