Metamath Proof Explorer

Theorem fsumcom2

Description: Interchange order of summation. Note that B ( j ) and D ( k ) are not necessarily constant expressions. (Contributed by Mario Carneiro, 28-Apr-2014) (Revised by Mario Carneiro, 8-Apr-2016) (Proof shortened by JJ, 2-Aug-2021)

Ref Expression
Hypotheses fsumcom2.1 
|- ( ph -> A e. Fin )
fsumcom2.2 
|- ( ph -> C e. Fin )
fsumcom2.3 
|- ( ( ph /\ j e. A ) -> B e. Fin )
fsumcom2.4 
|- ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. C /\ j e. D ) ) )
fsumcom2.5 
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> E e. CC )
Assertion fsumcom2 
|- ( ph -> sum_ j e. A sum_ k e. B E = sum_ k e. C sum_ j e. D E )

Proof

Step Hyp Ref Expression
1 fsumcom2.1 
 |-  ( ph -> A e. Fin )
2 fsumcom2.2 
 |-  ( ph -> C e. Fin )
3 fsumcom2.3 
 |-  ( ( ph /\ j e. A ) -> B e. Fin )
4 fsumcom2.4 
 |-  ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. C /\ j e. D ) ) )
5 fsumcom2.5 
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> E e. CC )
6 relxp 
 |-  Rel ( { j } X. B )
7 6 rgenw 
 |-  A. j e. A Rel ( { j } X. B )
8 reliun 
 |-  ( Rel U_ j e. A ( { j } X. B ) <-> A. j e. A Rel ( { j } X. B ) )
9 7 8 mpbir 
 |-  Rel U_ j e. A ( { j } X. B )
10 relcnv 
 |-  Rel `' U_ k e. C ( { k } X. D )
11 ancom 
 |-  ( ( x = j /\ y = k ) <-> ( y = k /\ x = j ) )
12 vex 
 |-  x e. _V
13 vex 
 |-  y e. _V
14 12 13 opth 
 |-  ( <. x , y >. = <. j , k >. <-> ( x = j /\ y = k ) )
15 13 12 opth 
 |-  ( <. y , x >. = <. k , j >. <-> ( y = k /\ x = j ) )
16 11 14 15 3bitr4i 
 |-  ( <. x , y >. = <. j , k >. <-> <. y , x >. = <. k , j >. )
17 16 a1i 
 |-  ( ph -> ( <. x , y >. = <. j , k >. <-> <. y , x >. = <. k , j >. ) )
18 17 4 anbi12d 
 |-  ( ph -> ( ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. B ) ) <-> ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) ) )
19 18 2exbidv 
 |-  ( ph -> ( E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. B ) ) <-> E. j E. k ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) ) )
20 eliunxp 
 |-  ( <. x , y >. e. U_ j e. A ( { j } X. B ) <-> E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. B ) ) )
21 12 13 opelcnv 
 |-  ( <. x , y >. e. `' U_ k e. C ( { k } X. D ) <-> <. y , x >. e. U_ k e. C ( { k } X. D ) )
22 eliunxp 
 |-  ( <. y , x >. e. U_ k e. C ( { k } X. D ) <-> E. k E. j ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) )
23 excom 
 |-  ( E. k E. j ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) <-> E. j E. k ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) )
24 21 22 23 3bitri 
 |-  ( <. x , y >. e. `' U_ k e. C ( { k } X. D ) <-> E. j E. k ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) )
25 19 20 24 3bitr4g 
 |-  ( ph -> ( <. x , y >. e. U_ j e. A ( { j } X. B ) <-> <. x , y >. e. `' U_ k e. C ( { k } X. D ) ) )
26 9 10 25 eqrelrdv 
 |-  ( ph -> U_ j e. A ( { j } X. B ) = `' U_ k e. C ( { k } X. D ) )
27 nfcv 
 |-  F/_ m ( { j } X. B )
28 nfcv 
 |-  F/_ j { m }
29 nfcsb1v 
 |-  F/_ j [_ m / j ]_ B
30 28 29 nfxp 
 |-  F/_ j ( { m } X. [_ m / j ]_ B )
31 sneq 
 |-  ( j = m -> { j } = { m } )
32 csbeq1a 
 |-  ( j = m -> B = [_ m / j ]_ B )
33 31 32 xpeq12d 
 |-  ( j = m -> ( { j } X. B ) = ( { m } X. [_ m / j ]_ B ) )
34 27 30 33 cbviun 
 |-  U_ j e. A ( { j } X. B ) = U_ m e. A ( { m } X. [_ m / j ]_ B )
35 nfcv 
 |-  F/_ n ( { k } X. D )
36 nfcv 
 |-  F/_ k { n }
37 nfcsb1v 
 |-  F/_ k [_ n / k ]_ D
38 36 37 nfxp 
 |-  F/_ k ( { n } X. [_ n / k ]_ D )
39 sneq 
 |-  ( k = n -> { k } = { n } )
40 csbeq1a 
 |-  ( k = n -> D = [_ n / k ]_ D )
41 39 40 xpeq12d 
 |-  ( k = n -> ( { k } X. D ) = ( { n } X. [_ n / k ]_ D ) )
42 35 38 41 cbviun 
 |-  U_ k e. C ( { k } X. D ) = U_ n e. C ( { n } X. [_ n / k ]_ D )
43 42 cnveqi 
 |-  `' U_ k e. C ( { k } X. D ) = `' U_ n e. C ( { n } X. [_ n / k ]_ D )
44 26 34 43 3eqtr3g 
 |-  ( ph -> U_ m e. A ( { m } X. [_ m / j ]_ B ) = `' U_ n e. C ( { n } X. [_ n / k ]_ D ) )
45 44 sumeq1d 
 |-  ( ph -> sum_ z e. U_ m e. A ( { m } X. [_ m / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E = sum_ z e. `' U_ n e. C ( { n } X. [_ n / k ]_ D ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E )
46 vex 
 |-  n e. _V
47 vex 
 |-  m e. _V
48 46 47 op1std 
 |-  ( w = <. n , m >. -> ( 1st ` w ) = n )
49 48 csbeq1d 
 |-  ( w = <. n , m >. -> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E = [_ n / k ]_ [_ ( 2nd ` w ) / j ]_ E )
50 46 47 op2ndd 
 |-  ( w = <. n , m >. -> ( 2nd ` w ) = m )
51 50 csbeq1d 
 |-  ( w = <. n , m >. -> [_ ( 2nd ` w ) / j ]_ E = [_ m / j ]_ E )
52 51 csbeq2dv 
 |-  ( w = <. n , m >. -> [_ n / k ]_ [_ ( 2nd ` w ) / j ]_ E = [_ n / k ]_ [_ m / j ]_ E )
53 49 52 eqtrd 
 |-  ( w = <. n , m >. -> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E = [_ n / k ]_ [_ m / j ]_ E )
54 47 46 op2ndd 
 |-  ( z = <. m , n >. -> ( 2nd ` z ) = n )
55 54 csbeq1d 
 |-  ( z = <. m , n >. -> [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E = [_ n / k ]_ [_ ( 1st ` z ) / j ]_ E )
56 47 46 op1std 
 |-  ( z = <. m , n >. -> ( 1st ` z ) = m )
57 56 csbeq1d 
 |-  ( z = <. m , n >. -> [_ ( 1st ` z ) / j ]_ E = [_ m / j ]_ E )
58 57 csbeq2dv 
 |-  ( z = <. m , n >. -> [_ n / k ]_ [_ ( 1st ` z ) / j ]_ E = [_ n / k ]_ [_ m / j ]_ E )
59 55 58 eqtrd 
 |-  ( z = <. m , n >. -> [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E = [_ n / k ]_ [_ m / j ]_ E )
60 snfi 
 |-  { n } e. Fin
61 1 adantr 
 |-  ( ( ph /\ n e. C ) -> A e. Fin )
62 47 46 opelcnv 
 |-  ( <. m , n >. e. `' U_ k e. C ( { k } X. D ) <-> <. n , m >. e. U_ k e. C ( { k } X. D ) )
63 37 40 opeliunxp2f 
 |-  ( <. n , m >. e. U_ k e. C ( { k } X. D ) <-> ( n e. C /\ m e. [_ n / k ]_ D ) )
64 62 63 sylbbr 
 |-  ( ( n e. C /\ m e. [_ n / k ]_ D ) -> <. m , n >. e. `' U_ k e. C ( { k } X. D ) )
65 64 adantl 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> <. m , n >. e. `' U_ k e. C ( { k } X. D ) )
66 26 adantr 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> U_ j e. A ( { j } X. B ) = `' U_ k e. C ( { k } X. D ) )
67 65 66 eleqtrrd 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> <. m , n >. e. U_ j e. A ( { j } X. B ) )
68 eliun 
 |-  ( <. m , n >. e. U_ j e. A ( { j } X. B ) <-> E. j e. A <. m , n >. e. ( { j } X. B ) )
69 67 68 sylib 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> E. j e. A <. m , n >. e. ( { j } X. B ) )
70 simpr 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> <. m , n >. e. ( { j } X. B ) )
71 opelxp 
 |-  ( <. m , n >. e. ( { j } X. B ) <-> ( m e. { j } /\ n e. B ) )
72 70 71 sylib 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> ( m e. { j } /\ n e. B ) )
73 72 simpld 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> m e. { j } )
74 elsni 
 |-  ( m e. { j } -> m = j )
75 73 74 syl 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> m = j )
76 simpl 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> j e. A )
77 75 76 eqeltrd 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> m e. A )
78 77 rexlimiva 
 |-  ( E. j e. A <. m , n >. e. ( { j } X. B ) -> m e. A )
79 69 78 syl 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> m e. A )
80 79 expr 
 |-  ( ( ph /\ n e. C ) -> ( m e. [_ n / k ]_ D -> m e. A ) )
81 80 ssrdv 
 |-  ( ( ph /\ n e. C ) -> [_ n / k ]_ D C_ A )
82 61 81 ssfid 
 |-  ( ( ph /\ n e. C ) -> [_ n / k ]_ D e. Fin )
83 xpfi 
 |-  ( ( { n } e. Fin /\ [_ n / k ]_ D e. Fin ) -> ( { n } X. [_ n / k ]_ D ) e. Fin )
84 60 82 83 sylancr 
 |-  ( ( ph /\ n e. C ) -> ( { n } X. [_ n / k ]_ D ) e. Fin )
85 84 ralrimiva 
 |-  ( ph -> A. n e. C ( { n } X. [_ n / k ]_ D ) e. Fin )
86 iunfi 
 |-  ( ( C e. Fin /\ A. n e. C ( { n } X. [_ n / k ]_ D ) e. Fin ) -> U_ n e. C ( { n } X. [_ n / k ]_ D ) e. Fin )
87 2 85 86 syl2anc 
 |-  ( ph -> U_ n e. C ( { n } X. [_ n / k ]_ D ) e. Fin )
88 reliun 
 |-  ( Rel U_ n e. C ( { n } X. [_ n / k ]_ D ) <-> A. n e. C Rel ( { n } X. [_ n / k ]_ D ) )
89 relxp 
 |-  Rel ( { n } X. [_ n / k ]_ D )
90 89 a1i 
 |-  ( n e. C -> Rel ( { n } X. [_ n / k ]_ D ) )
91 88 90 mprgbir 
 |-  Rel U_ n e. C ( { n } X. [_ n / k ]_ D )
92 91 a1i 
 |-  ( ph -> Rel U_ n e. C ( { n } X. [_ n / k ]_ D ) )
93 csbeq1 
 |-  ( m = ( 2nd ` w ) -> [_ m / j ]_ E = [_ ( 2nd ` w ) / j ]_ E )
94 93 csbeq2dv 
 |-  ( m = ( 2nd ` w ) -> [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E = [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E )
95 94 eleq1d 
 |-  ( m = ( 2nd ` w ) -> ( [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E e. CC <-> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E e. CC ) )
96 csbeq1 
 |-  ( n = ( 1st ` w ) -> [_ n / k ]_ D = [_ ( 1st ` w ) / k ]_ D )
97 csbeq1 
 |-  ( n = ( 1st ` w ) -> [_ n / k ]_ [_ m / j ]_ E = [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E )
98 97 eleq1d 
 |-  ( n = ( 1st ` w ) -> ( [_ n / k ]_ [_ m / j ]_ E e. CC <-> [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E e. CC ) )
99 96 98 raleqbidv 
 |-  ( n = ( 1st ` w ) -> ( A. m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E e. CC <-> A. m e. [_ ( 1st ` w ) / k ]_ D [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E e. CC ) )
100 simpl 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> ph )
101 29 nfcri 
 |-  F/ j n e. [_ m / j ]_ B
102 74 equcomd 
 |-  ( m e. { j } -> j = m )
103 102 32 syl 
 |-  ( m e. { j } -> B = [_ m / j ]_ B )
104 103 eleq2d 
 |-  ( m e. { j } -> ( n e. B <-> n e. [_ m / j ]_ B ) )
105 104 biimpa 
 |-  ( ( m e. { j } /\ n e. B ) -> n e. [_ m / j ]_ B )
106 71 105 sylbi 
 |-  ( <. m , n >. e. ( { j } X. B ) -> n e. [_ m / j ]_ B )
107 106 a1i 
 |-  ( j e. A -> ( <. m , n >. e. ( { j } X. B ) -> n e. [_ m / j ]_ B ) )
108 101 107 rexlimi 
 |-  ( E. j e. A <. m , n >. e. ( { j } X. B ) -> n e. [_ m / j ]_ B )
109 69 108 syl 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> n e. [_ m / j ]_ B )
110 5 ralrimivva 
 |-  ( ph -> A. j e. A A. k e. B E e. CC )
111 nfcsb1v 
 |-  F/_ j [_ m / j ]_ E
112 111 nfel1 
 |-  F/ j [_ m / j ]_ E e. CC
113 29 112 nfralw 
 |-  F/ j A. k e. [_ m / j ]_ B [_ m / j ]_ E e. CC
114 csbeq1a 
 |-  ( j = m -> E = [_ m / j ]_ E )
115 114 eleq1d 
 |-  ( j = m -> ( E e. CC <-> [_ m / j ]_ E e. CC ) )
116 32 115 raleqbidv 
 |-  ( j = m -> ( A. k e. B E e. CC <-> A. k e. [_ m / j ]_ B [_ m / j ]_ E e. CC ) )
117 113 116 rspc 
 |-  ( m e. A -> ( A. j e. A A. k e. B E e. CC -> A. k e. [_ m / j ]_ B [_ m / j ]_ E e. CC ) )
118 110 117 mpan9 
 |-  ( ( ph /\ m e. A ) -> A. k e. [_ m / j ]_ B [_ m / j ]_ E e. CC )
119 nfcsb1v 
 |-  F/_ k [_ n / k ]_ [_ m / j ]_ E
120 119 nfel1 
 |-  F/ k [_ n / k ]_ [_ m / j ]_ E e. CC
121 csbeq1a 
 |-  ( k = n -> [_ m / j ]_ E = [_ n / k ]_ [_ m / j ]_ E )
122 121 eleq1d 
 |-  ( k = n -> ( [_ m / j ]_ E e. CC <-> [_ n / k ]_ [_ m / j ]_ E e. CC ) )
123 120 122 rspc 
 |-  ( n e. [_ m / j ]_ B -> ( A. k e. [_ m / j ]_ B [_ m / j ]_ E e. CC -> [_ n / k ]_ [_ m / j ]_ E e. CC ) )
124 118 123 syl5com 
 |-  ( ( ph /\ m e. A ) -> ( n e. [_ m / j ]_ B -> [_ n / k ]_ [_ m / j ]_ E e. CC ) )
125 124 impr 
 |-  ( ( ph /\ ( m e. A /\ n e. [_ m / j ]_ B ) ) -> [_ n / k ]_ [_ m / j ]_ E e. CC )
126 100 79 109 125 syl12anc 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> [_ n / k ]_ [_ m / j ]_ E e. CC )
127 126 ralrimivva 
 |-  ( ph -> A. n e. C A. m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E e. CC )
128 127 adantr 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> A. n e. C A. m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E e. CC )
129 simpr 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) )
130 eliun 
 |-  ( w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) <-> E. n e. C w e. ( { n } X. [_ n / k ]_ D ) )
131 129 130 sylib 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> E. n e. C w e. ( { n } X. [_ n / k ]_ D ) )
132 xp1st 
 |-  ( w e. ( { n } X. [_ n / k ]_ D ) -> ( 1st ` w ) e. { n } )
133 132 adantl 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 1st ` w ) e. { n } )
134 elsni 
 |-  ( ( 1st ` w ) e. { n } -> ( 1st ` w ) = n )
135 133 134 syl 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 1st ` w ) = n )
136 simpl 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> n e. C )
137 135 136 eqeltrd 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 1st ` w ) e. C )
138 137 rexlimiva 
 |-  ( E. n e. C w e. ( { n } X. [_ n / k ]_ D ) -> ( 1st ` w ) e. C )
139 131 138 syl 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> ( 1st ` w ) e. C )
140 99 128 139 rspcdva 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> A. m e. [_ ( 1st ` w ) / k ]_ D [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E e. CC )
141 xp2nd 
 |-  ( w e. ( { n } X. [_ n / k ]_ D ) -> ( 2nd ` w ) e. [_ n / k ]_ D )
142 141 adantl 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 2nd ` w ) e. [_ n / k ]_ D )
143 135 csbeq1d 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> [_ ( 1st ` w ) / k ]_ D = [_ n / k ]_ D )
144 142 143 eleqtrrd 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
145 144 rexlimiva 
 |-  ( E. n e. C w e. ( { n } X. [_ n / k ]_ D ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
146 131 145 syl 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
147 95 140 146 rspcdva 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E e. CC )
148 53 59 87 92 147 fsumcnv 
 |-  ( ph -> sum_ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E = sum_ z e. `' U_ n e. C ( { n } X. [_ n / k ]_ D ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E )
149 45 148 eqtr4d 
 |-  ( ph -> sum_ z e. U_ m e. A ( { m } X. [_ m / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E = sum_ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E )
150 3 ralrimiva 
 |-  ( ph -> A. j e. A B e. Fin )
151 29 nfel1 
 |-  F/ j [_ m / j ]_ B e. Fin
152 32 eleq1d 
 |-  ( j = m -> ( B e. Fin <-> [_ m / j ]_ B e. Fin ) )
153 151 152 rspc 
 |-  ( m e. A -> ( A. j e. A B e. Fin -> [_ m / j ]_ B e. Fin ) )
154 150 153 mpan9 
 |-  ( ( ph /\ m e. A ) -> [_ m / j ]_ B e. Fin )
155 59 1 154 125 fsum2d 
 |-  ( ph -> sum_ m e. A sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E = sum_ z e. U_ m e. A ( { m } X. [_ m / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E )
156 53 2 82 126 fsum2d 
 |-  ( ph -> sum_ n e. C sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E = sum_ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E )
157 149 155 156 3eqtr4d 
 |-  ( ph -> sum_ m e. A sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E = sum_ n e. C sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E )
158 nfcv 
 |-  F/_ m sum_ k e. B E
159 nfcv 
 |-  F/_ j n
160 159 111 nfcsbw 
 |-  F/_ j [_ n / k ]_ [_ m / j ]_ E
161 29 160 nfsum 
 |-  F/_ j sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E
162 nfcv 
 |-  F/_ n E
163 nfcsb1v 
 |-  F/_ k [_ n / k ]_ E
164 csbeq1a 
 |-  ( k = n -> E = [_ n / k ]_ E )
165 162 163 164 cbvsumi 
 |-  sum_ k e. B E = sum_ n e. B [_ n / k ]_ E
166 114 csbeq2dv 
 |-  ( j = m -> [_ n / k ]_ E = [_ n / k ]_ [_ m / j ]_ E )
167 166 adantr 
 |-  ( ( j = m /\ n e. B ) -> [_ n / k ]_ E = [_ n / k ]_ [_ m / j ]_ E )
168 32 167 sumeq12dv 
 |-  ( j = m -> sum_ n e. B [_ n / k ]_ E = sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E )
169 165 168 syl5eq 
 |-  ( j = m -> sum_ k e. B E = sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E )
170 158 161 169 cbvsumi 
 |-  sum_ j e. A sum_ k e. B E = sum_ m e. A sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E
171 nfcv 
 |-  F/_ n sum_ j e. D E
172 37 119 nfsum 
 |-  F/_ k sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E
173 nfcv 
 |-  F/_ m E
174 173 111 114 cbvsumi 
 |-  sum_ j e. D E = sum_ m e. D [_ m / j ]_ E
175 121 adantr 
 |-  ( ( k = n /\ m e. D ) -> [_ m / j ]_ E = [_ n / k ]_ [_ m / j ]_ E )
176 40 175 sumeq12dv 
 |-  ( k = n -> sum_ m e. D [_ m / j ]_ E = sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E )
177 174 176 syl5eq 
 |-  ( k = n -> sum_ j e. D E = sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E )
178 171 172 177 cbvsumi 
 |-  sum_ k e. C sum_ j e. D E = sum_ n e. C sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E
179 157 170 178 3eqtr4g 
 |-  ( ph -> sum_ j e. A sum_ k e. B E = sum_ k e. C sum_ j e. D E )