Theorem ballotlemgval

Description: Expand the value of .^ . (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	⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
	ballotlemg	⊢ ↑ = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
Assertion	ballotlemgval	⊢ ( ( 𝑈 ∈ Fin ∧ 𝑉 ∈ Fin ) → ( 𝑈 ↑ 𝑉 ) = ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ) )

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		ballotlemg	⊢ ↑ = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
12		ineq2	⊢ ( 𝑢 = 𝑈 → ( 𝑣 ∩ 𝑢 ) = ( 𝑣 ∩ 𝑈 ) )
13	12	fveq2d	⊢ ( 𝑢 = 𝑈 → ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) = ( ♯ ‘ ( 𝑣 ∩ 𝑈 ) ) )
14		difeq2	⊢ ( 𝑢 = 𝑈 → ( 𝑣 ∖ 𝑢 ) = ( 𝑣 ∖ 𝑈 ) )
15	14	fveq2d	⊢ ( 𝑢 = 𝑈 → ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) = ( ♯ ‘ ( 𝑣 ∖ 𝑈 ) ) )
16	13 15	oveq12d	⊢ ( 𝑢 = 𝑈 → ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) = ( ( ♯ ‘ ( 𝑣 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑈 ) ) ) )
17		ineq1	⊢ ( 𝑣 = 𝑉 → ( 𝑣 ∩ 𝑈 ) = ( 𝑉 ∩ 𝑈 ) )
18	17	fveq2d	⊢ ( 𝑣 = 𝑉 → ( ♯ ‘ ( 𝑣 ∩ 𝑈 ) ) = ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) )
19		difeq1	⊢ ( 𝑣 = 𝑉 → ( 𝑣 ∖ 𝑈 ) = ( 𝑉 ∖ 𝑈 ) )
20	19	fveq2d	⊢ ( 𝑣 = 𝑉 → ( ♯ ‘ ( 𝑣 ∖ 𝑈 ) ) = ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) )
21	18 20	oveq12d	⊢ ( 𝑣 = 𝑉 → ( ( ♯ ‘ ( 𝑣 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑈 ) ) ) = ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ) )
22		ovex	⊢ ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ) ∈ V
23	16 21 11 22	ovmpo	⊢ ( ( 𝑈 ∈ Fin ∧ 𝑉 ∈ Fin ) → ( 𝑈 ↑ 𝑉 ) = ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ) )