Step | Hyp | Ref
| Expression |
1 | | df-esum 32667 |
. . . 4
β’
Ξ£*π
β π΄π΅ = βͺ
((β*π βΎs (0[,]+β))
tsums (π β π΄ β¦ π΅)) |
2 | | xrge0base 31918 |
. . . . . 6
β’
(0[,]+β) = (Baseβ(β*π
βΎs (0[,]+β))) |
3 | | xrge00 31919 |
. . . . . 6
β’ 0 =
(0gβ(β*π
βΎs (0[,]+β))) |
4 | | xrge0cmn 20855 |
. . . . . . 7
β’
(β*π βΎs
(0[,]+β)) β CMnd |
5 | 4 | a1i 11 |
. . . . . 6
β’ (π β
(β*π βΎs (0[,]+β))
β CMnd) |
6 | | xrge0tps 32563 |
. . . . . . 7
β’
(β*π βΎs
(0[,]+β)) β TopSp |
7 | 6 | a1i 11 |
. . . . . 6
β’ (π β
(β*π βΎs (0[,]+β))
β TopSp) |
8 | | esumpfinvalf.a |
. . . . . 6
β’ (π β π΄ β Fin) |
9 | | esumpfinvalf.2 |
. . . . . . 7
β’
β²ππ |
10 | | esumpfinvalf.1 |
. . . . . . 7
β’
β²ππ΄ |
11 | | nfcv 2908 |
. . . . . . 7
β’
β²π(0[,]+β) |
12 | | icossicc 13360 |
. . . . . . . 8
β’
(0[,)+β) β (0[,]+β) |
13 | | esumpfinvalf.b |
. . . . . . . 8
β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) |
14 | 12, 13 | sselid 3947 |
. . . . . . 7
β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) |
15 | | eqid 2737 |
. . . . . . 7
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
16 | 9, 10, 11, 14, 15 | fmptdF 31614 |
. . . . . 6
β’ (π β (π β π΄ β¦ π΅):π΄βΆ(0[,]+β)) |
17 | | c0ex 11156 |
. . . . . . . 8
β’ 0 β
V |
18 | 17 | a1i 11 |
. . . . . . 7
β’ (π β 0 β
V) |
19 | 16, 8, 18 | fdmfifsupp 9322 |
. . . . . 6
β’ (π β (π β π΄ β¦ π΅) finSupp 0) |
20 | | xrge0topn 32564 |
. . . . . . 7
β’
(TopOpenβ(β*π
βΎs (0[,]+β))) = ((ordTopβ β€ )
βΎt (0[,]+β)) |
21 | 20 | eqcomi 2746 |
. . . . . 6
β’
((ordTopβ β€ ) βΎt (0[,]+β)) =
(TopOpenβ(β*π βΎs
(0[,]+β))) |
22 | | xrhaus 22752 |
. . . . . . . 8
β’
(ordTopβ β€ ) β Haus |
23 | | ovex 7395 |
. . . . . . . 8
β’
(0[,]+β) β V |
24 | | resthaus 22735 |
. . . . . . . 8
β’
(((ordTopβ β€ ) β Haus β§ (0[,]+β) β V)
β ((ordTopβ β€ ) βΎt (0[,]+β)) β
Haus) |
25 | 22, 23, 24 | mp2an 691 |
. . . . . . 7
β’
((ordTopβ β€ ) βΎt (0[,]+β)) β
Haus |
26 | 25 | a1i 11 |
. . . . . 6
β’ (π β ((ordTopβ β€ )
βΎt (0[,]+β)) β Haus) |
27 | 2, 3, 5, 7, 8, 16,
19, 21, 26 | haustsmsid 23508 |
. . . . 5
β’ (π β
((β*π βΎs (0[,]+β))
tsums (π β π΄ β¦ π΅)) =
{((β*π βΎs (0[,]+β))
Ξ£g (π β π΄ β¦ π΅))}) |
28 | 27 | unieqd 4884 |
. . . 4
β’ (π β βͺ ((β*π
βΎs (0[,]+β)) tsums (π β π΄ β¦ π΅)) = βͺ
{((β*π βΎs (0[,]+β))
Ξ£g (π β π΄ β¦ π΅))}) |
29 | 1, 28 | eqtrid 2789 |
. . 3
β’ (π β Ξ£*π β π΄π΅ = βͺ
{((β*π βΎs (0[,]+β))
Ξ£g (π β π΄ β¦ π΅))}) |
30 | | ovex 7395 |
. . . 4
β’
((β*π βΎs
(0[,]+β)) Ξ£g (π β π΄ β¦ π΅)) β V |
31 | 30 | unisn 4892 |
. . 3
β’ βͺ {((β*π
βΎs (0[,]+β)) Ξ£g (π β π΄ β¦ π΅))} =
((β*π βΎs (0[,]+β))
Ξ£g (π β π΄ β¦ π΅)) |
32 | 29, 31 | eqtrdi 2793 |
. 2
β’ (π β Ξ£*π β π΄π΅ = ((β*π
βΎs (0[,]+β)) Ξ£g (π β π΄ β¦ π΅))) |
33 | | nfcv 2908 |
. . . 4
β’
β²π(0[,)+β) |
34 | 9, 10, 33, 13, 15 | fmptdF 31614 |
. . 3
β’ (π β (π β π΄ β¦ π΅):π΄βΆ(0[,)+β)) |
35 | | esumpfinvallem 32713 |
. . 3
β’ ((π΄ β Fin β§ (π β π΄ β¦ π΅):π΄βΆ(0[,)+β)) β
(βfld Ξ£g (π β π΄ β¦ π΅)) =
((β*π βΎs (0[,]+β))
Ξ£g (π β π΄ β¦ π΅))) |
36 | 8, 34, 35 | syl2anc 585 |
. 2
β’ (π β (βfld
Ξ£g (π β π΄ β¦ π΅)) =
((β*π βΎs (0[,]+β))
Ξ£g (π β π΄ β¦ π΅))) |
37 | | rge0ssre 13380 |
. . . . . . . 8
β’
(0[,)+β) β β |
38 | | ax-resscn 11115 |
. . . . . . . 8
β’ β
β β |
39 | 37, 38 | sstri 3958 |
. . . . . . 7
β’
(0[,)+β) β β |
40 | 39, 13 | sselid 3947 |
. . . . . 6
β’ ((π β§ π β π΄) β π΅ β β) |
41 | 40 | sbt 2070 |
. . . . 5
β’ [π / π]((π β§ π β π΄) β π΅ β β) |
42 | | sbim 2300 |
. . . . . 6
β’ ([π / π]((π β§ π β π΄) β π΅ β β) β ([π / π](π β§ π β π΄) β [π / π]π΅ β β)) |
43 | | sban 2084 |
. . . . . . . 8
β’ ([π / π](π β§ π β π΄) β ([π / π]π β§ [π / π]π β π΄)) |
44 | 9 | sbf 2263 |
. . . . . . . . 9
β’ ([π / π]π β π) |
45 | 10 | clelsb1fw 2912 |
. . . . . . . . 9
β’ ([π / π]π β π΄ β π β π΄) |
46 | 44, 45 | anbi12i 628 |
. . . . . . . 8
β’ (([π / π]π β§ [π / π]π β π΄) β (π β§ π β π΄)) |
47 | 43, 46 | bitri 275 |
. . . . . . 7
β’ ([π / π](π β§ π β π΄) β (π β§ π β π΄)) |
48 | | sbsbc 3748 |
. . . . . . . 8
β’ ([π / π]π΅ β β β [π / π]π΅ β β) |
49 | | sbcel1g 4378 |
. . . . . . . . 9
β’ (π β V β ([π / π]π΅ β β β β¦π / πβ¦π΅ β β)) |
50 | 49 | elv 3454 |
. . . . . . . 8
β’
([π / π]π΅ β β β β¦π / πβ¦π΅ β β) |
51 | 48, 50 | bitri 275 |
. . . . . . 7
β’ ([π / π]π΅ β β β β¦π / πβ¦π΅ β β) |
52 | 47, 51 | imbi12i 351 |
. . . . . 6
β’ (([π / π](π β§ π β π΄) β [π / π]π΅ β β) β ((π β§ π β π΄) β β¦π / πβ¦π΅ β β)) |
53 | 42, 52 | bitri 275 |
. . . . 5
β’ ([π / π]((π β§ π β π΄) β π΅ β β) β ((π β§ π β π΄) β β¦π / πβ¦π΅ β β)) |
54 | 41, 53 | mpbi 229 |
. . . 4
β’ ((π β§ π β π΄) β β¦π / πβ¦π΅ β β) |
55 | 8, 54 | gsumfsum 20880 |
. . 3
β’ (π β (βfld
Ξ£g (π β π΄ β¦ β¦π / πβ¦π΅)) = Ξ£π β π΄ β¦π / πβ¦π΅) |
56 | | nfcv 2908 |
. . . . 5
β’
β²ππ΄ |
57 | | nfcv 2908 |
. . . . 5
β’
β²ππ΅ |
58 | | nfcsb1v 3885 |
. . . . 5
β’
β²πβ¦π / πβ¦π΅ |
59 | | csbeq1a 3874 |
. . . . 5
β’ (π = π β π΅ = β¦π / πβ¦π΅) |
60 | 10, 56, 57, 58, 59 | cbvmptf 5219 |
. . . 4
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ β¦π / πβ¦π΅) |
61 | 60 | oveq2i 7373 |
. . 3
β’
(βfld Ξ£g (π β π΄ β¦ π΅)) = (βfld
Ξ£g (π β π΄ β¦ β¦π / πβ¦π΅)) |
62 | 59, 56, 10, 57, 58 | cbvsum 15587 |
. . 3
β’
Ξ£π β
π΄ π΅ = Ξ£π β π΄ β¦π / πβ¦π΅ |
63 | 55, 61, 62 | 3eqtr4g 2802 |
. 2
β’ (π β (βfld
Ξ£g (π β π΄ β¦ π΅)) = Ξ£π β π΄ π΅) |
64 | 32, 36, 63 | 3eqtr2d 2783 |
1
β’ (π β Ξ£*π β π΄π΅ = Ξ£π β π΄ π΅) |