Step | Hyp | Ref
| Expression |
1 | | rrxtopnfi.1 |
. . 3
β’ (π β πΌ β Fin) |
2 | 1 | rrxtopn 45299 |
. 2
β’ (π β
(TopOpenβ(β^βπΌ)) = (MetOpenβ(π β (Baseβ(β^βπΌ)), π β (Baseβ(β^βπΌ)) β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))))))) |
3 | | eqid 2731 |
. . . . 5
β’
(β^βπΌ) =
(β^βπΌ) |
4 | | eqid 2731 |
. . . . 5
β’
(Baseβ(β^βπΌ)) = (Baseβ(β^βπΌ)) |
5 | 1, 3, 4 | rrxbasefi 25159 |
. . . 4
β’ (π β
(Baseβ(β^βπΌ)) = (β βm πΌ)) |
6 | 5 | adantr 480 |
. . . 4
β’ ((π β§ π β (Baseβ(β^βπΌ))) β
(Baseβ(β^βπΌ)) = (β βm πΌ)) |
7 | | simpl 482 |
. . . . 5
β’ ((π β§ (π β (Baseβ(β^βπΌ)) β§ π β (Baseβ(β^βπΌ)))) β π) |
8 | | simprl 768 |
. . . . . 6
β’ ((π β§ (π β (Baseβ(β^βπΌ)) β§ π β (Baseβ(β^βπΌ)))) β π β (Baseβ(β^βπΌ))) |
9 | | simpr 484 |
. . . . . . 7
β’ ((π β§ π β (Baseβ(β^βπΌ))) β π β (Baseβ(β^βπΌ))) |
10 | 9, 6 | eleqtrd 2834 |
. . . . . 6
β’ ((π β§ π β (Baseβ(β^βπΌ))) β π β (β βm πΌ)) |
11 | 8, 10 | syldan 590 |
. . . . 5
β’ ((π β§ (π β (Baseβ(β^βπΌ)) β§ π β (Baseβ(β^βπΌ)))) β π β (β βm πΌ)) |
12 | | simprr 770 |
. . . . . 6
β’ ((π β§ (π β (Baseβ(β^βπΌ)) β§ π β (Baseβ(β^βπΌ)))) β π β (Baseβ(β^βπΌ))) |
13 | | simpr 484 |
. . . . . . 7
β’ ((π β§ π β (Baseβ(β^βπΌ))) β π β (Baseβ(β^βπΌ))) |
14 | 5 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β (Baseβ(β^βπΌ))) β
(Baseβ(β^βπΌ)) = (β βm πΌ)) |
15 | 13, 14 | eleqtrd 2834 |
. . . . . 6
β’ ((π β§ π β (Baseβ(β^βπΌ))) β π β (β βm πΌ)) |
16 | 12, 15 | syldan 590 |
. . . . 5
β’ ((π β§ (π β (Baseβ(β^βπΌ)) β§ π β (Baseβ(β^βπΌ)))) β π β (β βm πΌ)) |
17 | | elmapi 8847 |
. . . . . . . . . . . . . 14
β’ (π β (β
βm πΌ)
β π:πΌβΆβ) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((π β (β
βm πΌ) β§
π β (β
βm πΌ))
β π:πΌβΆβ) |
19 | 18 | ffvelcdmda 7086 |
. . . . . . . . . . . 12
β’ (((π β (β
βm πΌ) β§
π β (β
βm πΌ))
β§ π₯ β πΌ) β (πβπ₯) β β) |
20 | | elmapi 8847 |
. . . . . . . . . . . . . 14
β’ (π β (β
βm πΌ)
β π:πΌβΆβ) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . 13
β’ ((π β (β
βm πΌ) β§
π β (β
βm πΌ))
β π:πΌβΆβ) |
22 | 21 | ffvelcdmda 7086 |
. . . . . . . . . . . 12
β’ (((π β (β
βm πΌ) β§
π β (β
βm πΌ))
β§ π₯ β πΌ) β (πβπ₯) β β) |
23 | 19, 22 | resubcld 11647 |
. . . . . . . . . . 11
β’ (((π β (β
βm πΌ) β§
π β (β
βm πΌ))
β§ π₯ β πΌ) β ((πβπ₯) β (πβπ₯)) β β) |
24 | 23 | resqcld 14095 |
. . . . . . . . . 10
β’ (((π β (β
βm πΌ) β§
π β (β
βm πΌ))
β§ π₯ β πΌ) β (((πβπ₯) β (πβπ₯))β2) β β) |
25 | | eqid 2731 |
. . . . . . . . . 10
β’ (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)) = (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)) |
26 | 24, 25 | fmptd 7115 |
. . . . . . . . 9
β’ ((π β (β
βm πΌ) β§
π β (β
βm πΌ))
β (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)):πΌβΆβ) |
27 | 26 | 3adant1 1129 |
. . . . . . . 8
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)):πΌβΆβ) |
28 | 1 | 3ad2ant1 1132 |
. . . . . . . . 9
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β πΌ β Fin) |
29 | | 0red 11222 |
. . . . . . . . 9
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β 0 β
β) |
30 | 27, 28, 29 | fidmfisupp 9375 |
. . . . . . . 8
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)) finSupp 0) |
31 | | regsumsupp 21395 |
. . . . . . . 8
β’ (((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)):πΌβΆβ β§ (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)) finSupp 0 β§ πΌ β Fin) β (βfld
Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))) = Ξ£π β ((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)) supp 0)((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))βπ)) |
32 | 27, 30, 28, 31 | syl3anc 1370 |
. . . . . . 7
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β (βfld
Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))) = Ξ£π β ((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)) supp 0)((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))βπ)) |
33 | | ax-resscn 11171 |
. . . . . . . . . . . . . . 15
β’ β
β β |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (β
βm πΌ)
β β β β) |
35 | 17, 34 | fssd 6735 |
. . . . . . . . . . . . 13
β’ (π β (β
βm πΌ)
β π:πΌβΆβ) |
36 | 35 | 3ad2ant2 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β π:πΌβΆβ) |
37 | 36 | ffvelcdmda 7086 |
. . . . . . . . . . 11
β’ (((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β§ π₯ β πΌ) β (πβπ₯) β β) |
38 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (β
βm πΌ)
β β β β) |
39 | 20, 38 | fssd 6735 |
. . . . . . . . . . . . 13
β’ (π β (β
βm πΌ)
β π:πΌβΆβ) |
40 | 39 | 3ad2ant3 1134 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β π:πΌβΆβ) |
41 | 40 | ffvelcdmda 7086 |
. . . . . . . . . . 11
β’ (((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β§ π₯ β πΌ) β (πβπ₯) β β) |
42 | 37, 41 | subcld 11576 |
. . . . . . . . . 10
β’ (((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β§ π₯ β πΌ) β ((πβπ₯) β (πβπ₯)) β β) |
43 | 42 | sqcld 14114 |
. . . . . . . . 9
β’ (((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β§ π₯ β πΌ) β (((πβπ₯) β (πβπ₯))β2) β β) |
44 | 43, 25 | fmptd 7115 |
. . . . . . . 8
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)):πΌβΆβ) |
45 | 28, 44 | fsumsupp0 44593 |
. . . . . . 7
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β Ξ£π β ((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)) supp 0)((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))βπ) = Ξ£π β πΌ ((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))βπ)) |
46 | | eqidd 2732 |
. . . . . . . . 9
β’ (((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β§ π β πΌ) β (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)) = (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))) |
47 | | fveq2 6891 |
. . . . . . . . . . . 12
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
48 | | fveq2 6891 |
. . . . . . . . . . . 12
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
49 | 47, 48 | oveq12d 7430 |
. . . . . . . . . . 11
β’ (π₯ = π β ((πβπ₯) β (πβπ₯)) = ((πβπ) β (πβπ))) |
50 | 49 | oveq1d 7427 |
. . . . . . . . . 10
β’ (π₯ = π β (((πβπ₯) β (πβπ₯))β2) = (((πβπ) β (πβπ))β2)) |
51 | 50 | adantl 481 |
. . . . . . . . 9
β’ ((((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β§ π β πΌ) β§ π₯ = π) β (((πβπ₯) β (πβπ₯))β2) = (((πβπ) β (πβπ))β2)) |
52 | | simpr 484 |
. . . . . . . . 9
β’ (((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β§ π β πΌ) β π β πΌ) |
53 | | ovexd 7447 |
. . . . . . . . 9
β’ (((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β§ π β πΌ) β (((πβπ) β (πβπ))β2) β V) |
54 | 46, 51, 52, 53 | fvmptd 7005 |
. . . . . . . 8
β’ (((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β§ π β πΌ) β ((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))βπ) = (((πβπ) β (πβπ))β2)) |
55 | 54 | sumeq2dv 15654 |
. . . . . . 7
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β Ξ£π β πΌ ((π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))βπ) = Ξ£π β πΌ (((πβπ) β (πβπ))β2)) |
56 | 32, 45, 55 | 3eqtrd 2775 |
. . . . . 6
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β (βfld
Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))) = Ξ£π β πΌ (((πβπ) β (πβπ))β2)) |
57 | 56 | fveq2d 6895 |
. . . . 5
β’ ((π β§ π β (β βm πΌ) β§ π β (β βm πΌ)) β
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)))) = (ββΞ£π β πΌ (((πβπ) β (πβπ))β2))) |
58 | 7, 11, 16, 57 | syl3anc 1370 |
. . . 4
β’ ((π β§ (π β (Baseβ(β^βπΌ)) β§ π β (Baseβ(β^βπΌ)))) β
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)))) = (ββΞ£π β πΌ (((πβπ) β (πβπ))β2))) |
59 | 5, 6, 58 | mpoeq123dva 7486 |
. . 3
β’ (π β (π β (Baseβ(β^βπΌ)), π β (Baseβ(β^βπΌ)) β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))))) = (π β (β βm πΌ), π β (β βm πΌ) β¦
(ββΞ£π
β πΌ (((πβπ) β (πβπ))β2)))) |
60 | 59 | fveq2d 6895 |
. 2
β’ (π β (MetOpenβ(π β
(Baseβ(β^βπΌ)), π β (Baseβ(β^βπΌ)) β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)))))) = (MetOpenβ(π β (β
βm πΌ),
π β (β
βm πΌ)
β¦ (ββΞ£π β πΌ (((πβπ) β (πβπ))β2))))) |
61 | 2, 60 | eqtrd 2771 |
1
β’ (π β
(TopOpenβ(β^βπΌ)) = (MetOpenβ(π β (β βm πΌ), π β (β βm πΌ) β¦
(ββΞ£π
β πΌ (((πβπ) β (πβπ))β2))))) |