Metamath Proof Explorer

Theorem fsum2d

Description: Write a double sum as a sum over a two-dimensional region. Note that B ( j ) is a function of j . (Contributed by Mario Carneiro, 27-Apr-2014)

Ref Expression
Hypotheses fsum2d.1 
|- ( z = <. j , k >. -> D = C )
fsum2d.2 
|- ( ph -> A e. Fin )
fsum2d.3 
|- ( ( ph /\ j e. A ) -> B e. Fin )
fsum2d.4 
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
Assertion fsum2d 
|- ( ph -> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D )

Proof

Step Hyp Ref Expression
1 fsum2d.1 
 |-  ( z = <. j , k >. -> D = C )
2 fsum2d.2 
 |-  ( ph -> A e. Fin )
3 fsum2d.3 
 |-  ( ( ph /\ j e. A ) -> B e. Fin )
4 fsum2d.4 
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
5 ssid 
 |-  A C_ A
6 sseq1 
 |-  ( w = (/) -> ( w C_ A <-> (/) C_ A ) )
7 sumeq1 
 |-  ( w = (/) -> sum_ j e. w sum_ k e. B C = sum_ j e. (/) sum_ k e. B C )
8 iuneq1 
 |-  ( w = (/) -> U_ j e. w ( { j } X. B ) = U_ j e. (/) ( { j } X. B ) )
9 8 sumeq1d 
 |-  ( w = (/) -> sum_ z e. U_ j e. w ( { j } X. B ) D = sum_ z e. U_ j e. (/) ( { j } X. B ) D )
10 7 9 eqeq12d 
 |-  ( w = (/) -> ( sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D <-> sum_ j e. (/) sum_ k e. B C = sum_ z e. U_ j e. (/) ( { j } X. B ) D ) )
11 6 10 imbi12d 
 |-  ( w = (/) -> ( ( w C_ A -> sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D ) <-> ( (/) C_ A -> sum_ j e. (/) sum_ k e. B C = sum_ z e. U_ j e. (/) ( { j } X. B ) D ) ) )
12 11 imbi2d 
 |-  ( w = (/) -> ( ( ph -> ( w C_ A -> sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D ) ) <-> ( ph -> ( (/) C_ A -> sum_ j e. (/) sum_ k e. B C = sum_ z e. U_ j e. (/) ( { j } X. B ) D ) ) ) )
13 sseq1 
 |-  ( w = x -> ( w C_ A <-> x C_ A ) )
14 sumeq1 
 |-  ( w = x -> sum_ j e. w sum_ k e. B C = sum_ j e. x sum_ k e. B C )
15 iuneq1 
 |-  ( w = x -> U_ j e. w ( { j } X. B ) = U_ j e. x ( { j } X. B ) )
16 15 sumeq1d 
 |-  ( w = x -> sum_ z e. U_ j e. w ( { j } X. B ) D = sum_ z e. U_ j e. x ( { j } X. B ) D )
17 14 16 eqeq12d 
 |-  ( w = x -> ( sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D <-> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) )
18 13 17 imbi12d 
 |-  ( w = x -> ( ( w C_ A -> sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D ) <-> ( x C_ A -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) ) )
19 18 imbi2d 
 |-  ( w = x -> ( ( ph -> ( w C_ A -> sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D ) ) <-> ( ph -> ( x C_ A -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) ) ) )
20 sseq1 
 |-  ( w = ( x u. { y } ) -> ( w C_ A <-> ( x u. { y } ) C_ A ) )
21 sumeq1 
 |-  ( w = ( x u. { y } ) -> sum_ j e. w sum_ k e. B C = sum_ j e. ( x u. { y } ) sum_ k e. B C )
22 iuneq1 
 |-  ( w = ( x u. { y } ) -> U_ j e. w ( { j } X. B ) = U_ j e. ( x u. { y } ) ( { j } X. B ) )
23 22 sumeq1d 
 |-  ( w = ( x u. { y } ) -> sum_ z e. U_ j e. w ( { j } X. B ) D = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )
24 21 23 eqeq12d 
 |-  ( w = ( x u. { y } ) -> ( sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D <-> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) )
25 20 24 imbi12d 
 |-  ( w = ( x u. { y } ) -> ( ( w C_ A -> sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D ) <-> ( ( x u. { y } ) C_ A -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) )
26 25 imbi2d 
 |-  ( w = ( x u. { y } ) -> ( ( ph -> ( w C_ A -> sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D ) ) <-> ( ph -> ( ( x u. { y } ) C_ A -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) ) )
27 sseq1 
 |-  ( w = A -> ( w C_ A <-> A C_ A ) )
28 sumeq1 
 |-  ( w = A -> sum_ j e. w sum_ k e. B C = sum_ j e. A sum_ k e. B C )
29 iuneq1 
 |-  ( w = A -> U_ j e. w ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
30 29 sumeq1d 
 |-  ( w = A -> sum_ z e. U_ j e. w ( { j } X. B ) D = sum_ z e. U_ j e. A ( { j } X. B ) D )
31 28 30 eqeq12d 
 |-  ( w = A -> ( sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D <-> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D ) )
32 27 31 imbi12d 
 |-  ( w = A -> ( ( w C_ A -> sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D ) <-> ( A C_ A -> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D ) ) )
33 32 imbi2d 
 |-  ( w = A -> ( ( ph -> ( w C_ A -> sum_ j e. w sum_ k e. B C = sum_ z e. U_ j e. w ( { j } X. B ) D ) ) <-> ( ph -> ( A C_ A -> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D ) ) ) )
34 sum0 
 |-  sum_ z e. (/) D = 0
35 0iun 
 |-  U_ j e. (/) ( { j } X. B ) = (/)
36 35 sumeq1i 
 |-  sum_ z e. U_ j e. (/) ( { j } X. B ) D = sum_ z e. (/) D
37 sum0 
 |-  sum_ j e. (/) sum_ k e. B C = 0
38 34 36 37 3eqtr4ri 
 |-  sum_ j e. (/) sum_ k e. B C = sum_ z e. U_ j e. (/) ( { j } X. B ) D
39 38 2a1i 
 |-  ( ph -> ( (/) C_ A -> sum_ j e. (/) sum_ k e. B C = sum_ z e. U_ j e. (/) ( { j } X. B ) D ) )
40 ssun1 
 |-  x C_ ( x u. { y } )
41 sstr 
 |-  ( ( x C_ ( x u. { y } ) /\ ( x u. { y } ) C_ A ) -> x C_ A )
42 40 41 mpan 
 |-  ( ( x u. { y } ) C_ A -> x C_ A )
43 42 imim1i 
 |-  ( ( x C_ A -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) -> ( ( x u. { y } ) C_ A -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) )
44 simpll 
 |-  ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) -> ph )
45 44 2 syl 
 |-  ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) -> A e. Fin )
46 44 3 sylan 
 |-  ( ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) /\ j e. A ) -> B e. Fin )
47 44 4 sylan 
 |-  ( ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) /\ ( j e. A /\ k e. B ) ) -> C e. CC )
48 simplr 
 |-  ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) -> -. y e. x )
49 simpr 
 |-  ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) -> ( x u. { y } ) C_ A )
50 biid 
 |-  ( sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D <-> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D )
51 1 45 46 47 48 49 50 fsum2dlem 
 |-  ( ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) /\ sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )
52 51 exp31 
 |-  ( ( ph /\ -. y e. x ) -> ( ( x u. { y } ) C_ A -> ( sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) )
53 52 a2d 
 |-  ( ( ph /\ -. y e. x ) -> ( ( ( x u. { y } ) C_ A -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) -> ( ( x u. { y } ) C_ A -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) )
54 43 53 syl5 
 |-  ( ( ph /\ -. y e. x ) -> ( ( x C_ A -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) -> ( ( x u. { y } ) C_ A -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) )
55 54 expcom 
 |-  ( -. y e. x -> ( ph -> ( ( x C_ A -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) -> ( ( x u. { y } ) C_ A -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) ) )
56 55 a2d 
 |-  ( -. y e. x -> ( ( ph -> ( x C_ A -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) ) -> ( ph -> ( ( x u. { y } ) C_ A -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) ) )
57 56 adantl 
 |-  ( ( x e. Fin /\ -. y e. x ) -> ( ( ph -> ( x C_ A -> sum_ j e. x sum_ k e. B C = sum_ z e. U_ j e. x ( { j } X. B ) D ) ) -> ( ph -> ( ( x u. { y } ) C_ A -> sum_ j e. ( x u. { y } ) sum_ k e. B C = sum_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) ) )
58 12 19 26 33 39 57 findcard2s 
 |-  ( A e. Fin -> ( ph -> ( A C_ A -> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D ) ) )
59 2 58 mpcom 
 |-  ( ph -> ( A C_ A -> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D ) )
60 5 59 mpi 
 |-  ( ph -> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D )