Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(TopOpenββfld) =
(TopOpenββfld) |
2 | 1 | cnfldhaus 24293 |
. . 3
β’
(TopOpenββfld) β Haus |
3 | 2 | a1i 11 |
. 2
β’ (π β
(TopOpenββfld) β Haus) |
4 | | occl.2 |
. . . . . . 7
β’ (π β πΉ β Cauchy) |
5 | | ax-hcompl 30443 |
. . . . . . 7
β’ (πΉ β Cauchy β
βπ₯ β β
πΉ
βπ£ π₯) |
6 | | hlimf 30478 |
. . . . . . . . . 10
β’
βπ£ :dom βπ£ βΆ
β |
7 | | ffn 6715 |
. . . . . . . . . 10
β’ (
βπ£ :dom βπ£ βΆ β
β βπ£ Fn dom βπ£
) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . 9
β’
βπ£ Fn dom βπ£ |
9 | | fnbr 6655 |
. . . . . . . . 9
β’ ((
βπ£ Fn dom βπ£ β§ πΉ βπ£
π₯) β πΉ β dom βπ£
) |
10 | 8, 9 | mpan 689 |
. . . . . . . 8
β’ (πΉ βπ£
π₯ β πΉ β dom βπ£
) |
11 | 10 | rexlimivw 3152 |
. . . . . . 7
β’
(βπ₯ β
β πΉ
βπ£ π₯ β πΉ β dom βπ£
) |
12 | 4, 5, 11 | 3syl 18 |
. . . . . 6
β’ (π β πΉ β dom βπ£
) |
13 | | ffun 6718 |
. . . . . . 7
β’ (
βπ£ :dom βπ£ βΆ β
β Fun βπ£ ) |
14 | | funfvbrb 7050 |
. . . . . . 7
β’ (Fun
βπ£ β (πΉ β dom βπ£
β πΉ
βπ£ ( βπ£ βπΉ))) |
15 | 6, 13, 14 | mp2b 10 |
. . . . . 6
β’ (πΉ β dom
βπ£ β πΉ βπ£ (
βπ£ βπΉ)) |
16 | 12, 15 | sylib 217 |
. . . . 5
β’ (π β πΉ βπ£ (
βπ£ βπΉ)) |
17 | | eqid 2733 |
. . . . . . . 8
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
18 | | eqid 2733 |
. . . . . . . . 9
β’
(normβ β ββ ) =
(normβ β ββ ) |
19 | 17, 18 | hhims 30413 |
. . . . . . . 8
β’
(normβ β ββ ) =
(IndMetββ¨β¨ +β ,
Β·β β©,
normββ©) |
20 | | eqid 2733 |
. . . . . . . 8
β’
(MetOpenβ(normβ β
ββ )) = (MetOpenβ(normβ β
ββ )) |
21 | 17, 19, 20 | hhlm 30440 |
. . . . . . 7
β’
βπ£ =
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) |
22 | | resss 6005 |
. . . . . . 7
β’
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) β
(βπ‘β(MetOpenβ(normβ β
ββ ))) |
23 | 21, 22 | eqsstri 4016 |
. . . . . 6
β’
βπ£ β
(βπ‘β(MetOpenβ(normβ
β ββ ))) |
24 | 23 | ssbri 5193 |
. . . . 5
β’ (πΉ βπ£ (
βπ£ βπΉ) β πΉ(βπ‘β(MetOpenβ(normβ
β ββ )))( βπ£ βπΉ)) |
25 | 16, 24 | syl 17 |
. . . 4
β’ (π β πΉ(βπ‘β(MetOpenβ(normβ
β ββ )))( βπ£ βπΉ)) |
26 | 18 | hilxmet 30436 |
. . . . . 6
β’
(normβ β ββ ) β
(βMetβ β) |
27 | 20 | mopntopon 23937 |
. . . . . 6
β’
((normβ β ββ ) β
(βMetβ β) β (MetOpenβ(normβ
β ββ )) β (TopOnβ
β)) |
28 | 26, 27 | mp1i 13 |
. . . . 5
β’ (π β
(MetOpenβ(normβ β ββ ))
β (TopOnβ β)) |
29 | 28 | cnmptid 23157 |
. . . . 5
β’ (π β (π₯ β β β¦ π₯) β
((MetOpenβ(normβ β ββ ))
Cn (MetOpenβ(normβ β ββ
)))) |
30 | | occl.1 |
. . . . . . 7
β’ (π β π΄ β β) |
31 | | occl.4 |
. . . . . . 7
β’ (π β π΅ β π΄) |
32 | 30, 31 | sseldd 3983 |
. . . . . 6
β’ (π β π΅ β β) |
33 | 28, 28, 32 | cnmptc 23158 |
. . . . 5
β’ (π β (π₯ β β β¦ π΅) β
((MetOpenβ(normβ β ββ ))
Cn (MetOpenβ(normβ β ββ
)))) |
34 | 17 | hhnv 30406 |
. . . . . 6
β’
β¨β¨ +β , Β·β
β©, normββ© β NrmCVec |
35 | 17 | hhip 30418 |
. . . . . . 7
β’
Β·ih =
(Β·πOLDββ¨β¨ +β
, Β·β β©,
normββ©) |
36 | 35, 19, 20, 1 | dipcn 29961 |
. . . . . 6
β’
(β¨β¨ +β , Β·β
β©, normββ© β NrmCVec β
Β·ih β
(((MetOpenβ(normβ β ββ ))
Γt (MetOpenβ(normβ β
ββ ))) Cn
(TopOpenββfld))) |
37 | 34, 36 | mp1i 13 |
. . . . 5
β’ (π β
Β·ih β
(((MetOpenβ(normβ β ββ ))
Γt (MetOpenβ(normβ β
ββ ))) Cn
(TopOpenββfld))) |
38 | 28, 29, 33, 37 | cnmpt12f 23162 |
. . . 4
β’ (π β (π₯ β β β¦ (π₯ Β·ih π΅)) β
((MetOpenβ(normβ β ββ ))
Cn (TopOpenββfld))) |
39 | 25, 38 | lmcn 22801 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯ Β·ih π΅)) β πΉ)(βπ‘β(TopOpenββfld))((π₯ β β β¦ (π₯ Β·ih π΅))β( βπ£ βπΉ))) |
40 | | occl.3 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆ(β₯βπ΄)) |
41 | 40 | ffvelcdmda 7084 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΉβπ) β (β₯βπ΄)) |
42 | | ocel 30522 |
. . . . . . . . . . . 12
β’ (π΄ β β β ((πΉβπ) β (β₯βπ΄) β ((πΉβπ) β β β§ βπ₯ β π΄ ((πΉβπ) Β·ih π₯) = 0))) |
43 | 30, 42 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((πΉβπ) β (β₯βπ΄) β ((πΉβπ) β β β§ βπ₯ β π΄ ((πΉβπ) Β·ih π₯) = 0))) |
44 | 43 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πΉβπ) β (β₯βπ΄) β ((πΉβπ) β β β§ βπ₯ β π΄ ((πΉβπ) Β·ih π₯) = 0))) |
45 | 41, 44 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πΉβπ) β β β§ βπ₯ β π΄ ((πΉβπ) Β·ih π₯) = 0)) |
46 | 45 | simpld 496 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΉβπ) β β) |
47 | | oveq1 7413 |
. . . . . . . . 9
β’ (π₯ = (πΉβπ) β (π₯ Β·ih π΅) = ((πΉβπ) Β·ih π΅)) |
48 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β β β¦ (π₯
Β·ih π΅)) = (π₯ β β β¦ (π₯ Β·ih π΅)) |
49 | | ovex 7439 |
. . . . . . . . 9
β’ ((πΉβπ) Β·ih π΅) β V |
50 | 47, 48, 49 | fvmpt 6996 |
. . . . . . . 8
β’ ((πΉβπ) β β β ((π₯ β β β¦ (π₯ Β·ih π΅))β(πΉβπ)) = ((πΉβπ) Β·ih π΅)) |
51 | 46, 50 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β ((π₯ β β β¦ (π₯ Β·ih π΅))β(πΉβπ)) = ((πΉβπ) Β·ih π΅)) |
52 | | oveq2 7414 |
. . . . . . . . 9
β’ (π₯ = π΅ β ((πΉβπ) Β·ih π₯) = ((πΉβπ) Β·ih π΅)) |
53 | 52 | eqeq1d 2735 |
. . . . . . . 8
β’ (π₯ = π΅ β (((πΉβπ) Β·ih π₯) = 0 β ((πΉβπ) Β·ih π΅) = 0)) |
54 | 45 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π β β) β βπ₯ β π΄ ((πΉβπ) Β·ih π₯) = 0) |
55 | 31 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π΅ β π΄) |
56 | 53, 54, 55 | rspcdva 3614 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΉβπ) Β·ih π΅) = 0) |
57 | 51, 56 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π β β) β ((π₯ β β β¦ (π₯ Β·ih π΅))β(πΉβπ)) = 0) |
58 | | ocss 30526 |
. . . . . . . . 9
β’ (π΄ β β β
(β₯βπ΄) β
β) |
59 | 30, 58 | syl 17 |
. . . . . . . 8
β’ (π β (β₯βπ΄) β
β) |
60 | 40, 59 | fssd 6733 |
. . . . . . 7
β’ (π β πΉ:ββΆ β) |
61 | | fvco3 6988 |
. . . . . . 7
β’ ((πΉ:ββΆ β β§
π β β) β
(((π₯ β β β¦
(π₯
Β·ih π΅)) β πΉ)βπ) = ((π₯ β β β¦ (π₯ Β·ih π΅))β(πΉβπ))) |
62 | 60, 61 | sylan 581 |
. . . . . 6
β’ ((π β§ π β β) β (((π₯ β β β¦ (π₯ Β·ih π΅)) β πΉ)βπ) = ((π₯ β β β¦ (π₯ Β·ih π΅))β(πΉβπ))) |
63 | | c0ex 11205 |
. . . . . . . 8
β’ 0 β
V |
64 | 63 | fvconst2 7202 |
. . . . . . 7
β’ (π β β β ((β
Γ {0})βπ) =
0) |
65 | 64 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β ((β Γ
{0})βπ) =
0) |
66 | 57, 62, 65 | 3eqtr4d 2783 |
. . . . 5
β’ ((π β§ π β β) β (((π₯ β β β¦ (π₯ Β·ih π΅)) β πΉ)βπ) = ((β Γ {0})βπ)) |
67 | 66 | ralrimiva 3147 |
. . . 4
β’ (π β βπ β β (((π₯ β β β¦ (π₯ Β·ih π΅)) β πΉ)βπ) = ((β Γ {0})βπ)) |
68 | | ovex 7439 |
. . . . . . 7
β’ (π₯
Β·ih π΅) β V |
69 | 68, 48 | fnmpti 6691 |
. . . . . 6
β’ (π₯ β β β¦ (π₯
Β·ih π΅)) Fn β |
70 | | fnfco 6754 |
. . . . . 6
β’ (((π₯ β β β¦ (π₯
Β·ih π΅)) Fn β β§ πΉ:ββΆ β) β ((π₯ β β β¦ (π₯
Β·ih π΅)) β πΉ) Fn β) |
71 | 69, 60, 70 | sylancr 588 |
. . . . 5
β’ (π β ((π₯ β β β¦ (π₯ Β·ih π΅)) β πΉ) Fn β) |
72 | 63 | fconst 6775 |
. . . . . 6
β’ (β
Γ {0}):ββΆ{0} |
73 | | ffn 6715 |
. . . . . 6
β’ ((β
Γ {0}):ββΆ{0} β (β Γ {0}) Fn
β) |
74 | 72, 73 | ax-mp 5 |
. . . . 5
β’ (β
Γ {0}) Fn β |
75 | | eqfnfv 7030 |
. . . . 5
β’ ((((π₯ β β β¦ (π₯
Β·ih π΅)) β πΉ) Fn β β§ (β Γ {0}) Fn
β) β (((π₯ β
β β¦ (π₯
Β·ih π΅)) β πΉ) = (β Γ {0}) β
βπ β β
(((π₯ β β β¦
(π₯
Β·ih π΅)) β πΉ)βπ) = ((β Γ {0})βπ))) |
76 | 71, 74, 75 | sylancl 587 |
. . . 4
β’ (π β (((π₯ β β β¦ (π₯ Β·ih π΅)) β πΉ) = (β Γ {0}) β
βπ β β
(((π₯ β β β¦
(π₯
Β·ih π΅)) β πΉ)βπ) = ((β Γ {0})βπ))) |
77 | 67, 76 | mpbird 257 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯ Β·ih π΅)) β πΉ) = (β Γ {0})) |
78 | | fvex 6902 |
. . . . 5
β’ (
βπ£ βπΉ) β V |
79 | 78 | hlimveci 30431 |
. . . 4
β’ (πΉ βπ£ (
βπ£ βπΉ) β ( βπ£
βπΉ) β
β) |
80 | | oveq1 7413 |
. . . . 5
β’ (π₯ = ( βπ£
βπΉ) β (π₯
Β·ih π΅) = (( βπ£
βπΉ)
Β·ih π΅)) |
81 | | ovex 7439 |
. . . . 5
β’ ((
βπ£ βπΉ) Β·ih π΅) β V |
82 | 80, 48, 81 | fvmpt 6996 |
. . . 4
β’ ((
βπ£ βπΉ) β β β ((π₯ β β β¦ (π₯ Β·ih π΅))β(
βπ£ βπΉ)) = (( βπ£
βπΉ)
Β·ih π΅)) |
83 | 16, 79, 82 | 3syl 18 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯ Β·ih π΅))β(
βπ£ βπΉ)) = (( βπ£
βπΉ)
Β·ih π΅)) |
84 | 39, 77, 83 | 3brtr3d 5179 |
. 2
β’ (π β (β Γ
{0})(βπ‘β(TopOpenββfld))((
βπ£ βπΉ) Β·ih π΅)) |
85 | 1 | cnfldtopon 24291 |
. . . 4
β’
(TopOpenββfld) β
(TopOnββ) |
86 | 85 | a1i 11 |
. . 3
β’ (π β
(TopOpenββfld) β
(TopOnββ)) |
87 | | 0cnd 11204 |
. . 3
β’ (π β 0 β
β) |
88 | | 1zzd 12590 |
. . 3
β’ (π β 1 β
β€) |
89 | | nnuz 12862 |
. . . 4
β’ β =
(β€β₯β1) |
90 | 89 | lmconst 22757 |
. . 3
β’
(((TopOpenββfld) β (TopOnββ)
β§ 0 β β β§ 1 β β€) β (β Γ
{0})(βπ‘β(TopOpenββfld))0) |
91 | 86, 87, 88, 90 | syl3anc 1372 |
. 2
β’ (π β (β Γ
{0})(βπ‘β(TopOpenββfld))0) |
92 | 3, 84, 91 | lmmo 22876 |
1
β’ (π β ((
βπ£ βπΉ) Β·ih π΅) = 0) |