Metamath Proof Explorer

Theorem ballotlemgun

Description: A property of the defined .^ operator. (Contributed by Thierry Arnoux, 26-Apr-2017)

Ref Expression
Hypotheses ballotth.m 
|- M e. NN
ballotth.n 
|- N e. NN
ballotth.o 
|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
ballotth.p 
|- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
ballotth.f 
|- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
ballotth.e 
|- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }
ballotth.mgtn 
|- N < M
ballotth.i 
|- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )
ballotth.s 
|- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )
ballotth.r 
|- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )
ballotlemg 
|- .^ = ( u e. Fin , v e. Fin |-> ( ( # ` ( v i^i u ) ) - ( # ` ( v \ u ) ) ) )
ballotlemgun.1 
|- ( ph -> U e. Fin )
ballotlemgun.2 
|- ( ph -> V e. Fin )
ballotlemgun.3 
|- ( ph -> W e. Fin )
ballotlemgun.4 
|- ( ph -> ( V i^i W ) = (/) )
Assertion ballotlemgun 
|- ( ph -> ( U .^ ( V u. W ) ) = ( ( U .^ V ) + ( U .^ W ) ) )

Proof

Step Hyp Ref Expression
1 ballotth.m 
 |-  M e. NN
2 ballotth.n 
 |-  N e. NN
3 ballotth.o 
 |-  O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
4 ballotth.p 
 |-  P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
5 ballotth.f 
 |-  F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
6 ballotth.e 
 |-  E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }
7 ballotth.mgtn 
 |-  N < M
8 ballotth.i 
 |-  I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )
9 ballotth.s 
 |-  S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )
10 ballotth.r 
 |-  R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )
11 ballotlemg 
 |-  .^ = ( u e. Fin , v e. Fin |-> ( ( # ` ( v i^i u ) ) - ( # ` ( v \ u ) ) ) )
12 ballotlemgun.1 
 |-  ( ph -> U e. Fin )
13 ballotlemgun.2 
 |-  ( ph -> V e. Fin )
14 ballotlemgun.3 
 |-  ( ph -> W e. Fin )
15 ballotlemgun.4 
 |-  ( ph -> ( V i^i W ) = (/) )
16 indir 
 |-  ( ( V u. W ) i^i U ) = ( ( V i^i U ) u. ( W i^i U ) )
17 16 fveq2i 
 |-  ( # ` ( ( V u. W ) i^i U ) ) = ( # ` ( ( V i^i U ) u. ( W i^i U ) ) )
18 infi 
 |-  ( V e. Fin -> ( V i^i U ) e. Fin )
19 13 18 syl 
 |-  ( ph -> ( V i^i U ) e. Fin )
20 infi 
 |-  ( W e. Fin -> ( W i^i U ) e. Fin )
21 14 20 syl 
 |-  ( ph -> ( W i^i U ) e. Fin )
22 15 ineq1d 
 |-  ( ph -> ( ( V i^i W ) i^i U ) = ( (/) i^i U ) )
23 inindir 
 |-  ( ( V i^i W ) i^i U ) = ( ( V i^i U ) i^i ( W i^i U ) )
24 0in 
 |-  ( (/) i^i U ) = (/)
25 22 23 24 3eqtr3g 
 |-  ( ph -> ( ( V i^i U ) i^i ( W i^i U ) ) = (/) )
26 hashun 
 |-  ( ( ( V i^i U ) e. Fin /\ ( W i^i U ) e. Fin /\ ( ( V i^i U ) i^i ( W i^i U ) ) = (/) ) -> ( # ` ( ( V i^i U ) u. ( W i^i U ) ) ) = ( ( # ` ( V i^i U ) ) + ( # ` ( W i^i U ) ) ) )
27 19 21 25 26 syl3anc 
 |-  ( ph -> ( # ` ( ( V i^i U ) u. ( W i^i U ) ) ) = ( ( # ` ( V i^i U ) ) + ( # ` ( W i^i U ) ) ) )
28 17 27 syl5eq 
 |-  ( ph -> ( # ` ( ( V u. W ) i^i U ) ) = ( ( # ` ( V i^i U ) ) + ( # ` ( W i^i U ) ) ) )
29 difundir 
 |-  ( ( V u. W ) \ U ) = ( ( V \ U ) u. ( W \ U ) )
30 29 fveq2i 
 |-  ( # ` ( ( V u. W ) \ U ) ) = ( # ` ( ( V \ U ) u. ( W \ U ) ) )
31 diffi 
 |-  ( V e. Fin -> ( V \ U ) e. Fin )
32 13 31 syl 
 |-  ( ph -> ( V \ U ) e. Fin )
33 diffi 
 |-  ( W e. Fin -> ( W \ U ) e. Fin )
34 14 33 syl 
 |-  ( ph -> ( W \ U ) e. Fin )
35 15 difeq1d 
 |-  ( ph -> ( ( V i^i W ) \ U ) = ( (/) \ U ) )
36 difindir 
 |-  ( ( V i^i W ) \ U ) = ( ( V \ U ) i^i ( W \ U ) )
37 0dif 
 |-  ( (/) \ U ) = (/)
38 35 36 37 3eqtr3g 
 |-  ( ph -> ( ( V \ U ) i^i ( W \ U ) ) = (/) )
39 hashun 
 |-  ( ( ( V \ U ) e. Fin /\ ( W \ U ) e. Fin /\ ( ( V \ U ) i^i ( W \ U ) ) = (/) ) -> ( # ` ( ( V \ U ) u. ( W \ U ) ) ) = ( ( # ` ( V \ U ) ) + ( # ` ( W \ U ) ) ) )
40 32 34 38 39 syl3anc 
 |-  ( ph -> ( # ` ( ( V \ U ) u. ( W \ U ) ) ) = ( ( # ` ( V \ U ) ) + ( # ` ( W \ U ) ) ) )
41 30 40 syl5eq 
 |-  ( ph -> ( # ` ( ( V u. W ) \ U ) ) = ( ( # ` ( V \ U ) ) + ( # ` ( W \ U ) ) ) )
42 28 41 oveq12d 
 |-  ( ph -> ( ( # ` ( ( V u. W ) i^i U ) ) - ( # ` ( ( V u. W ) \ U ) ) ) = ( ( ( # ` ( V i^i U ) ) + ( # ` ( W i^i U ) ) ) - ( ( # ` ( V \ U ) ) + ( # ` ( W \ U ) ) ) ) )
43 hashcl 
 |-  ( ( V i^i U ) e. Fin -> ( # ` ( V i^i U ) ) e. NN0 )
44 13 18 43 3syl 
 |-  ( ph -> ( # ` ( V i^i U ) ) e. NN0 )
45 44 nn0cnd 
 |-  ( ph -> ( # ` ( V i^i U ) ) e. CC )
46 hashcl 
 |-  ( ( W i^i U ) e. Fin -> ( # ` ( W i^i U ) ) e. NN0 )
47 14 20 46 3syl 
 |-  ( ph -> ( # ` ( W i^i U ) ) e. NN0 )
48 47 nn0cnd 
 |-  ( ph -> ( # ` ( W i^i U ) ) e. CC )
49 hashcl 
 |-  ( ( V \ U ) e. Fin -> ( # ` ( V \ U ) ) e. NN0 )
50 13 31 49 3syl 
 |-  ( ph -> ( # ` ( V \ U ) ) e. NN0 )
51 50 nn0cnd 
 |-  ( ph -> ( # ` ( V \ U ) ) e. CC )
52 hashcl 
 |-  ( ( W \ U ) e. Fin -> ( # ` ( W \ U ) ) e. NN0 )
53 14 33 52 3syl 
 |-  ( ph -> ( # ` ( W \ U ) ) e. NN0 )
54 53 nn0cnd 
 |-  ( ph -> ( # ` ( W \ U ) ) e. CC )
55 45 48 51 54 addsub4d 
 |-  ( ph -> ( ( ( # ` ( V i^i U ) ) + ( # ` ( W i^i U ) ) ) - ( ( # ` ( V \ U ) ) + ( # ` ( W \ U ) ) ) ) = ( ( ( # ` ( V i^i U ) ) - ( # ` ( V \ U ) ) ) + ( ( # ` ( W i^i U ) ) - ( # ` ( W \ U ) ) ) ) )
56 42 55 eqtrd 
 |-  ( ph -> ( ( # ` ( ( V u. W ) i^i U ) ) - ( # ` ( ( V u. W ) \ U ) ) ) = ( ( ( # ` ( V i^i U ) ) - ( # ` ( V \ U ) ) ) + ( ( # ` ( W i^i U ) ) - ( # ` ( W \ U ) ) ) ) )
57 unfi 
 |-  ( ( V e. Fin /\ W e. Fin ) -> ( V u. W ) e. Fin )
58 13 14 57 syl2anc 
 |-  ( ph -> ( V u. W ) e. Fin )
59 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval 
 |-  ( ( U e. Fin /\ ( V u. W ) e. Fin ) -> ( U .^ ( V u. W ) ) = ( ( # ` ( ( V u. W ) i^i U ) ) - ( # ` ( ( V u. W ) \ U ) ) ) )
60 12 58 59 syl2anc 
 |-  ( ph -> ( U .^ ( V u. W ) ) = ( ( # ` ( ( V u. W ) i^i U ) ) - ( # ` ( ( V u. W ) \ U ) ) ) )
61 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval 
 |-  ( ( U e. Fin /\ V e. Fin ) -> ( U .^ V ) = ( ( # ` ( V i^i U ) ) - ( # ` ( V \ U ) ) ) )
62 12 13 61 syl2anc 
 |-  ( ph -> ( U .^ V ) = ( ( # ` ( V i^i U ) ) - ( # ` ( V \ U ) ) ) )
63 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval 
 |-  ( ( U e. Fin /\ W e. Fin ) -> ( U .^ W ) = ( ( # ` ( W i^i U ) ) - ( # ` ( W \ U ) ) ) )
64 12 14 63 syl2anc 
 |-  ( ph -> ( U .^ W ) = ( ( # ` ( W i^i U ) ) - ( # ` ( W \ U ) ) ) )
65 62 64 oveq12d 
 |-  ( ph -> ( ( U .^ V ) + ( U .^ W ) ) = ( ( ( # ` ( V i^i U ) ) - ( # ` ( V \ U ) ) ) + ( ( # ` ( W i^i U ) ) - ( # ` ( W \ U ) ) ) ) )
66 56 60 65 3eqtr4d 
 |-  ( ph -> ( U .^ ( V u. W ) ) = ( ( U .^ V ) + ( U .^ W ) ) )