Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tsmsxp Structured version   Unicode version

Theorem tsmsxp 18184
 Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 15550 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 18182 for the main proof; this part mostly sets up the local assumptions. (Contributed by Mario Carneiro, 21-Sep-2015.)
Hypotheses
Ref Expression
tsmsxp.b
tsmsxp.g CMnd
tsmsxp.2
tsmsxp.a
tsmsxp.c
tsmsxp.f
tsmsxp.h
tsmsxp.1 tsums
Assertion
Ref Expression
tsmsxp tsums tsums
Distinct variable groups:   ,,   ,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)   (,)

Proof of Theorem tsmsxp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tsmsxp.2 . . . . . . . . . . 11
2 tgptmd 18109 . . . . . . . . . . 11 TopMnd
31, 2syl 16 . . . . . . . . . 10 TopMnd
433ad2ant1 978 . . . . . . . . 9 TopMnd
5 simp2 958 . . . . . . . . 9
6 eqid 2436 . . . . . . . . . . . . 13
7 tsmsxp.b . . . . . . . . . . . . 13
86, 7tmdtopon 18111 . . . . . . . . . . . 12 TopMnd TopOn
94, 8syl 16 . . . . . . . . . . 11 TopOn
10 toponss 16994 . . . . . . . . . . 11 TopOn
119, 5, 10syl2anc 643 . . . . . . . . . 10
12 simp3 959 . . . . . . . . . 10
1311, 12sseldd 3349 . . . . . . . . 9
14 tmdmnd 18105 . . . . . . . . . . 11 TopMnd
154, 14syl 16 . . . . . . . . . 10
16 eqid 2436 . . . . . . . . . . 11
177, 16mndidcl 14714 . . . . . . . . . 10
1815, 17syl 16 . . . . . . . . 9
19 eqid 2436 . . . . . . . . . . . 12
207, 19, 16mndrid 14717 . . . . . . . . . . 11
2115, 13, 20syl2anc 643 . . . . . . . . . 10
2221, 12eqeltrd 2510 . . . . . . . . 9
237, 6, 19tmdcn2 18119 . . . . . . . . 9 TopMnd
244, 5, 13, 18, 22, 23syl23anc 1191 . . . . . . . 8
25 r19.29 2846 . . . . . . . . 9 g g
26 simp31 993 . . . . . . . . . . . . . . . 16
27 elfpw 7408 . . . . . . . . . . . . . . . . . . . . . . 23
2827simplbi 447 . . . . . . . . . . . . . . . . . . . . . 22
2928ad2antrl 709 . . . . . . . . . . . . . . . . . . . . 21 g
30 dmss 5069 . . . . . . . . . . . . . . . . . . . . 21
3129, 30syl 16 . . . . . . . . . . . . . . . . . . . 20 g
32 dmxpss 5300 . . . . . . . . . . . . . . . . . . . 20
3331, 32syl6ss 3360 . . . . . . . . . . . . . . . . . . 19 g
3427simprbi 451 . . . . . . . . . . . . . . . . . . . . 21
3534ad2antrl 709 . . . . . . . . . . . . . . . . . . . 20 g
36 dmfi 7389 . . . . . . . . . . . . . . . . . . . 20
3735, 36syl 16 . . . . . . . . . . . . . . . . . . 19 g
38 elfpw 7408 . . . . . . . . . . . . . . . . . . 19
3933, 37, 38sylanbrc 646 . . . . . . . . . . . . . . . . . 18 g
40 eqid 2436 . . . . . . . . . . . . . . . . . . . . . . 23 .g .g
41 simpl11 1032 . . . . . . . . . . . . . . . . . . . . . . . 24 g
42 tsmsxp.g . . . . . . . . . . . . . . . . . . . . . . . 24 CMnd
4341, 42syl 16 . . . . . . . . . . . . . . . . . . . . . . 23 g CMnd
4441, 3syl 16 . . . . . . . . . . . . . . . . . . . . . . 23 g TopMnd
45 simprrl 741 . . . . . . . . . . . . . . . . . . . . . . . 24 g
46 elfpw 7408 . . . . . . . . . . . . . . . . . . . . . . . . 25
4746simprbi 451 . . . . . . . . . . . . . . . . . . . . . . . 24
4845, 47syl 16 . . . . . . . . . . . . . . . . . . . . . . 23 g
49 simpl2r 1011 . . . . . . . . . . . . . . . . . . . . . . 23 g
5044, 14syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 g
5150, 17syl 16 . . . . . . . . . . . . . . . . . . . . . . 23 g
52 hashcl 11639 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5348, 52syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 g
547, 40, 16mulgnn0z 14910 . . . . . . . . . . . . . . . . . . . . . . . . 25 .g
5550, 53, 54syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24 g .g
56 simpl32 1039 . . . . . . . . . . . . . . . . . . . . . . . 24 g
5755, 56eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . . 23 g .g
586, 7, 40, 43, 44, 48, 49, 51, 57tmdgsum2 18126 . . . . . . . . . . . . . . . . . . . . . 22 g g
59 simp111 1086 . . . . . . . . . . . . . . . . . . . . . . . . . 26 g g
6059, 42syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g CMnd
6159, 1syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
62 tsmsxp.a . . . . . . . . . . . . . . . . . . . . . . . . . 26
6359, 62syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
64 tsmsxp.c . . . . . . . . . . . . . . . . . . . . . . . . . 26
6559, 64syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
66 tsmsxp.f . . . . . . . . . . . . . . . . . . . . . . . . . 26
6759, 66syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
68 tsmsxp.h . . . . . . . . . . . . . . . . . . . . . . . . . 26
6959, 68syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
70 tsmsxp.1 . . . . . . . . . . . . . . . . . . . . . . . . . 26 tsums
7159, 70sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g tsums
72 eqid 2436 . . . . . . . . . . . . . . . . . . . . . . . . 25
73 simp3l 985 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
74 simp3rl 1030 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
75 simp2rl 1026 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
76 simp2rr 1027 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
77 simp2ll 1024 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g
787, 60, 61, 63, 65, 67, 69, 71, 6, 16, 19, 72, 73, 74, 75, 76, 77tsmsxplem1 18182 . . . . . . . . . . . . . . . . . . . . . . . 24 g g g
79433adant3 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g CMnd
80613adant3r 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
81633adant3r 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
82653adant3r 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
83673adant3r 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
84693adant3r 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
85413adant3 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 g g g
8685, 70sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g tsums
87 simp3ll 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
88743adant3r 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
89 simp2rl 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
90 simp133 1094 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
91 simp3rl 1030 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
92 simp2ll 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 g g g
93 simp2rr 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 g g g
94 simp3rr 1031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 g g g g
9594simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 g g g
96 relxp 4983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
97 relss 4963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9828, 96, 97ee10 1385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
99 relssdmrn 5390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
10098, 99syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
101 xpss12 4981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
102100, 101sylan9ss 3361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
10392, 93, 95, 102syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g
10494simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g g
105 elfpw 7408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
106 xpss12 4981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
107 xpfi 7378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
108106, 107anim12i 550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
109108an4s 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
11046, 105, 109syl2anb 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111 elfpw 7408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
112110, 111sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
11389, 91, 112syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 g g g
114 simp2lr 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 g g g g
115 sseq2 3370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
116 reseq2 5141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
117116oveq2d 6097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 g g
118117eleq1d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 g g
119115, 118imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 g g
120119rspcv 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 g g
121113, 114, 103, 120syl3c 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g g
122 simp3lr 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 g g g g
123122simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 g g g g
124 oveq2 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 g g
125124eleq1d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 g g
126125cbvralv 2932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 g g
127123, 126sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 g g g g
1287, 79, 80, 81, 82, 83, 84, 86, 6, 16, 19, 72, 87, 88, 89, 90, 91, 103, 104, 121, 127tsmsxplem2 18183 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 g g g g
1291283exp 1152 . . . . . . . . . . . . . . . . . . . . . . . . . 26 g g g g
130129exp4a 590 . . . . . . . . . . . . . . . . . . . . . . . . 25 g g g g
1311303imp1 1166 . . . . . . . . . . . . . . . . . . . . . . . 24 g g g g
13278, 131rexlimddv 2834 . . . . . . . . . . . . . . . . . . . . . . 23 g g g
1331323expa 1153 . . . . . . . . . . . . . . . . . . . . . 22 g g g
13458, 133rexlimddv 2834 . . . . . . . . . . . . . . . . . . . . 21 g g
135134anassrs 630 . . . . . . . . . . . . . . . . . . . 20 g g
136135expr 599 . . . . . . . . . . . . . . . . . . 19 g g
137136ralrimiva 2789 . . . . . . . . . . . . . . . . . 18 g g
138 sseq1 3369 . . . . . . . . . . . . . . . . . . . . 21
139138imbi1d 309 . . . . . . . . . . . . . . . . . . . 20 g g
140139ralbidv 2725 . . . . . . . . . . . . . . . . . . 19 g g
141140rspcev 3052 . . . . . . . . . . . . . . . . . 18 g g
14239, 137, 141syl2anc 643 . . . . . . . . . . . . . . . . 17 g g
143142rexlimdvaa 2831 . . . . . . . . . . . . . . . 16 g g
14426, 143embantd 52 . . . . . . . . . . . . . . 15 g g
1451443expia 1155 . . . . . . . . . . . . . 14 g g
146145anassrs 630 . . . . . . . . . . . . 13 g g
147146rexlimdva 2830 . . . . . . . . . . . 12 g g
148147com23 74 . . . . . . . . . . 11 g g
149148imp3a 421 . . . . . . . . . 10 g g
150149rexlimdva 2830 . . . . . . . . 9 g