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 opelxp 
 |-  ( <. m , n >. e. ( { j } X. B ) <-> ( m e. { j } /\ n e. B ) )
71 70 bilani 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> ( m e. { j } /\ n e. B ) )
72 71 simpld 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> m e. { j } )
73 elsni 
 |-  ( m e. { j } -> m = j )
74 72 73 syl 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> m = j )
75 simpl 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> j e. A )
76 74 75 eqeltrd 
 |-  ( ( j e. A /\ <. m , n >. e. ( { j } X. B ) ) -> m e. A )
77 76 rexlimiva 
 |-  ( E. j e. A <. m , n >. e. ( { j } X. B ) -> m e. A )
78 69 77 syl 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> m e. A )
79 78 expr 
 |-  ( ( ph /\ n e. C ) -> ( m e. [_ n / k ]_ D -> m e. A ) )
80 79 ssrdv 
 |-  ( ( ph /\ n e. C ) -> [_ n / k ]_ D C_ A )
81 61 80 ssfid 
 |-  ( ( ph /\ n e. C ) -> [_ n / k ]_ D e. Fin )
82 xpfi 
 |-  ( ( { n } e. Fin /\ [_ n / k ]_ D e. Fin ) -> ( { n } X. [_ n / k ]_ D ) e. Fin )
83 60 81 82 sylancr 
 |-  ( ( ph /\ n e. C ) -> ( { n } X. [_ n / k ]_ D ) e. Fin )
84 83 ralrimiva 
 |-  ( ph -> A. n e. C ( { n } X. [_ n / k ]_ D ) e. Fin )
85 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 )
86 2 84 85 syl2anc 
 |-  ( ph -> U_ n e. C ( { n } X. [_ n / k ]_ D ) e. Fin )
87 reliun 
 |-  ( Rel U_ n e. C ( { n } X. [_ n / k ]_ D ) <-> A. n e. C Rel ( { n } X. [_ n / k ]_ D ) )
88 relxp 
 |-  Rel ( { n } X. [_ n / k ]_ D )
89 88 a1i 
 |-  ( n e. C -> Rel ( { n } X. [_ n / k ]_ D ) )
90 87 89 mprgbir 
 |-  Rel U_ n e. C ( { n } X. [_ n / k ]_ D )
91 90 a1i 
 |-  ( ph -> Rel U_ n e. C ( { n } X. [_ n / k ]_ D ) )
92 csbeq1 
 |-  ( m = ( 2nd ` w ) -> [_ m / j ]_ E = [_ ( 2nd ` w ) / j ]_ E )
93 92 csbeq2dv 
 |-  ( m = ( 2nd ` w ) -> [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E = [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E )
94 93 eleq1d 
 |-  ( m = ( 2nd ` w ) -> ( [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E e. CC <-> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E e. CC ) )
95 csbeq1 
 |-  ( n = ( 1st ` w ) -> [_ n / k ]_ D = [_ ( 1st ` w ) / k ]_ D )
96 csbeq1 
 |-  ( n = ( 1st ` w ) -> [_ n / k ]_ [_ m / j ]_ E = [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E )
97 96 eleq1d 
 |-  ( n = ( 1st ` w ) -> ( [_ n / k ]_ [_ m / j ]_ E e. CC <-> [_ ( 1st ` w ) / k ]_ [_ m / j ]_ E e. CC ) )
98 95 97 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 ) )
99 simpl 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> ph )
100 29 nfcri 
 |-  F/ j n e. [_ m / j ]_ B
101 73 equcomd 
 |-  ( m e. { j } -> j = m )
102 101 32 syl 
 |-  ( m e. { j } -> B = [_ m / j ]_ B )
103 102 eleq2d 
 |-  ( m e. { j } -> ( n e. B <-> n e. [_ m / j ]_ B ) )
104 103 biimpa 
 |-  ( ( m e. { j } /\ n e. B ) -> n e. [_ m / j ]_ B )
105 70 104 sylbi 
 |-  ( <. m , n >. e. ( { j } X. B ) -> n e. [_ m / j ]_ B )
106 105 a1i 
 |-  ( j e. A -> ( <. m , n >. e. ( { j } X. B ) -> n e. [_ m / j ]_ B ) )
107 100 106 rexlimi 
 |-  ( E. j e. A <. m , n >. e. ( { j } X. B ) -> n e. [_ m / j ]_ B )
108 69 107 syl 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> n e. [_ m / j ]_ B )
109 5 ralrimivva 
 |-  ( ph -> A. j e. A A. k e. B E e. CC )
110 nfcsb1v 
 |-  F/_ j [_ m / j ]_ E
111 110 nfel1 
 |-  F/ j [_ m / j ]_ E e. CC
112 29 111 nfralw 
 |-  F/ j A. k e. [_ m / j ]_ B [_ m / j ]_ E e. CC
113 csbeq1a 
 |-  ( j = m -> E = [_ m / j ]_ E )
114 113 eleq1d 
 |-  ( j = m -> ( E e. CC <-> [_ m / j ]_ E e. CC ) )
115 32 114 raleqbidv 
 |-  ( j = m -> ( A. k e. B E e. CC <-> A. k e. [_ m / j ]_ B [_ m / j ]_ E e. CC ) )
116 112 115 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 ) )
117 109 116 mpan9 
 |-  ( ( ph /\ m e. A ) -> A. k e. [_ m / j ]_ B [_ m / j ]_ E e. CC )
118 nfcsb1v 
 |-  F/_ k [_ n / k ]_ [_ m / j ]_ E
119 118 nfel1 
 |-  F/ k [_ n / k ]_ [_ m / j ]_ E e. CC
120 csbeq1a 
 |-  ( k = n -> [_ m / j ]_ E = [_ n / k ]_ [_ m / j ]_ E )
121 120 eleq1d 
 |-  ( k = n -> ( [_ m / j ]_ E e. CC <-> [_ n / k ]_ [_ m / j ]_ E e. CC ) )
122 119 121 rspc 
 |-  ( n e. [_ m / j ]_ B -> ( A. k e. [_ m / j ]_ B [_ m / j ]_ E e. CC -> [_ n / k ]_ [_ m / j ]_ E e. CC ) )
123 117 122 syl5com 
 |-  ( ( ph /\ m e. A ) -> ( n e. [_ m / j ]_ B -> [_ n / k ]_ [_ m / j ]_ E e. CC ) )
124 123 impr 
 |-  ( ( ph /\ ( m e. A /\ n e. [_ m / j ]_ B ) ) -> [_ n / k ]_ [_ m / j ]_ E e. CC )
125 99 78 108 124 syl12anc 
 |-  ( ( ph /\ ( n e. C /\ m e. [_ n / k ]_ D ) ) -> [_ n / k ]_ [_ m / j ]_ E e. CC )
126 125 ralrimivva 
 |-  ( ph -> A. n e. C A. m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E e. CC )
127 126 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 )
128 eliun 
 |-  ( w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) <-> E. n e. C w e. ( { n } X. [_ n / k ]_ D ) )
129 128 bilani 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> E. n e. C w e. ( { n } X. [_ n / k ]_ D ) )
130 xp1st 
 |-  ( w e. ( { n } X. [_ n / k ]_ D ) -> ( 1st ` w ) e. { n } )
131 130 adantl 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 1st ` w ) e. { n } )
132 elsni 
 |-  ( ( 1st ` w ) e. { n } -> ( 1st ` w ) = n )
133 131 132 syl 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 1st ` w ) = n )
134 simpl 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> n e. C )
135 133 134 eqeltrd 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 1st ` w ) e. C )
136 135 rexlimiva 
 |-  ( E. n e. C w e. ( { n } X. [_ n / k ]_ D ) -> ( 1st ` w ) e. C )
137 129 136 syl 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> ( 1st ` w ) e. C )
138 98 127 137 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 )
139 xp2nd 
 |-  ( w e. ( { n } X. [_ n / k ]_ D ) -> ( 2nd ` w ) e. [_ n / k ]_ D )
140 139 adantl 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 2nd ` w ) e. [_ n / k ]_ D )
141 133 csbeq1d 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> [_ ( 1st ` w ) / k ]_ D = [_ n / k ]_ D )
142 140 141 eleqtrrd 
 |-  ( ( n e. C /\ w e. ( { n } X. [_ n / k ]_ D ) ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
143 142 rexlimiva 
 |-  ( E. n e. C w e. ( { n } X. [_ n / k ]_ D ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
144 129 143 syl 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
145 94 138 144 rspcdva 
 |-  ( ( ph /\ w e. U_ n e. C ( { n } X. [_ n / k ]_ D ) ) -> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E e. CC )
146 53 59 86 91 145 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 )
147 45 146 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 )
148 3 ralrimiva 
 |-  ( ph -> A. j e. A B e. Fin )
149 29 nfel1 
 |-  F/ j [_ m / j ]_ B e. Fin
150 32 eleq1d 
 |-  ( j = m -> ( B e. Fin <-> [_ m / j ]_ B e. Fin ) )
151 149 150 rspc 
 |-  ( m e. A -> ( A. j e. A B e. Fin -> [_ m / j ]_ B e. Fin ) )
152 148 151 mpan9 
 |-  ( ( ph /\ m e. A ) -> [_ m / j ]_ B e. Fin )
153 59 1 152 124 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 )
154 53 2 81 125 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 )
155 147 153 154 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 )
156 csbeq1a 
 |-  ( k = n -> E = [_ n / k ]_ E )
157 nfcv 
 |-  F/_ n E
158 nfcsb1v 
 |-  F/_ k [_ n / k ]_ E
159 156 157 158 cbvsum 
 |-  sum_ k e. B E = sum_ n e. B [_ n / k ]_ E
160 113 csbeq2dv 
 |-  ( j = m -> [_ n / k ]_ E = [_ n / k ]_ [_ m / j ]_ E )
161 160 adantr 
 |-  ( ( j = m /\ n e. B ) -> [_ n / k ]_ E = [_ n / k ]_ [_ m / j ]_ E )
162 32 161 sumeq12dv 
 |-  ( j = m -> sum_ n e. B [_ n / k ]_ E = sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E )
163 159 162 eqtrid 
 |-  ( j = m -> sum_ k e. B E = sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E )
164 nfcv 
 |-  F/_ m sum_ k e. B E
165 nfcv 
 |-  F/_ j n
166 165 110 nfcsbw 
 |-  F/_ j [_ n / k ]_ [_ m / j ]_ E
167 29 166 nfsum 
 |-  F/_ j sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E
168 163 164 167 cbvsum 
 |-  sum_ j e. A sum_ k e. B E = sum_ m e. A sum_ n e. [_ m / j ]_ B [_ n / k ]_ [_ m / j ]_ E
169 nfcv 
 |-  F/_ m E
170 113 169 110 cbvsum 
 |-  sum_ j e. D E = sum_ m e. D [_ m / j ]_ E
171 120 adantr 
 |-  ( ( k = n /\ m e. D ) -> [_ m / j ]_ E = [_ n / k ]_ [_ m / j ]_ E )
172 40 171 sumeq12dv 
 |-  ( k = n -> sum_ m e. D [_ m / j ]_ E = sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E )
173 170 172 eqtrid 
 |-  ( k = n -> sum_ j e. D E = sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E )
174 nfcv 
 |-  F/_ n sum_ j e. D E
175 37 118 nfsum 
 |-  F/_ k sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E
176 173 174 175 cbvsum 
 |-  sum_ k e. C sum_ j e. D E = sum_ n e. C sum_ m e. [_ n / k ]_ D [_ n / k ]_ [_ m / j ]_ E
177 155 168 176 3eqtr4g 
 |-  ( ph -> sum_ j e. A sum_ k e. B E = sum_ k e. C sum_ j e. D E )