Step | Hyp | Ref
| Expression |
1 | | nlelch.1 |
. . 3
β’ π β LinFn |
2 | 1 | nlelshi 31344 |
. 2
β’
(nullβπ)
β Sβ |
3 | | vex 3479 |
. . . . . 6
β’ π₯ β V |
4 | 3 | hlimveci 30474 |
. . . . 5
β’ (π βπ£
π₯ β π₯ β β) |
5 | 4 | adantl 483 |
. . . 4
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π₯ β β) |
6 | | eqid 2733 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
7 | 6 | cnfldhaus 24301 |
. . . . . 6
β’
(TopOpenββfld) β Haus |
8 | 7 | a1i 11 |
. . . . 5
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β
(TopOpenββfld) β Haus) |
9 | | eqid 2733 |
. . . . . . . . . 10
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
10 | | eqid 2733 |
. . . . . . . . . . 11
β’
(normβ β ββ ) =
(normβ β ββ ) |
11 | 9, 10 | hhims 30456 |
. . . . . . . . . 10
β’
(normβ β ββ ) =
(IndMetββ¨β¨ +β ,
Β·β β©,
normββ©) |
12 | | eqid 2733 |
. . . . . . . . . 10
β’
(MetOpenβ(normβ β
ββ )) = (MetOpenβ(normβ β
ββ )) |
13 | 9, 11, 12 | hhlm 30483 |
. . . . . . . . 9
β’
βπ£ =
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) |
14 | | resss 6007 |
. . . . . . . . 9
β’
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) β
(βπ‘β(MetOpenβ(normβ β
ββ ))) |
15 | 13, 14 | eqsstri 4017 |
. . . . . . . 8
β’
βπ£ β
(βπ‘β(MetOpenβ(normβ
β ββ ))) |
16 | 15 | ssbri 5194 |
. . . . . . 7
β’ (π βπ£
π₯ β π(βπ‘β(MetOpenβ(normβ
β ββ )))π₯) |
17 | 16 | adantl 483 |
. . . . . 6
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π(βπ‘β(MetOpenβ(normβ
β ββ )))π₯) |
18 | | nlelch.2 |
. . . . . . . 8
β’ π β ContFn |
19 | 10, 12, 6 | hhcnf 31189 |
. . . . . . . 8
β’ ContFn =
((MetOpenβ(normβ β ββ ))
Cn (TopOpenββfld)) |
20 | 18, 19 | eleqtri 2832 |
. . . . . . 7
β’ π β
((MetOpenβ(normβ β ββ ))
Cn (TopOpenββfld)) |
21 | 20 | a1i 11 |
. . . . . 6
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π β
((MetOpenβ(normβ β ββ ))
Cn (TopOpenββfld))) |
22 | 17, 21 | lmcn 22809 |
. . . . 5
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (π β π)(βπ‘β(TopOpenββfld))(πβπ₯)) |
23 | 1 | lnfnfi 31325 |
. . . . . . . . . 10
β’ π:
ββΆβ |
24 | | ffvelcdm 7084 |
. . . . . . . . . . 11
β’ ((π:ββΆ(nullβπ) β§ π β β) β (πβπ) β (nullβπ)) |
25 | 24 | adantlr 714 |
. . . . . . . . . 10
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β (πβπ) β (nullβπ)) |
26 | | elnlfn2 31213 |
. . . . . . . . . 10
β’ ((π: ββΆβ β§
(πβπ) β (nullβπ)) β (πβ(πβπ)) = 0) |
27 | 23, 25, 26 | sylancr 588 |
. . . . . . . . 9
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β (πβ(πβπ)) = 0) |
28 | | fvco3 6991 |
. . . . . . . . . 10
β’ ((π:ββΆ(nullβπ) β§ π β β) β ((π β π)βπ) = (πβ(πβπ))) |
29 | 28 | adantlr 714 |
. . . . . . . . 9
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β ((π β π)βπ) = (πβ(πβπ))) |
30 | | c0ex 11208 |
. . . . . . . . . . 11
β’ 0 β
V |
31 | 30 | fvconst2 7205 |
. . . . . . . . . 10
β’ (π β β β ((β
Γ {0})βπ) =
0) |
32 | 31 | adantl 483 |
. . . . . . . . 9
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β ((β Γ
{0})βπ) =
0) |
33 | 27, 29, 32 | 3eqtr4d 2783 |
. . . . . . . 8
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β ((π β π)βπ) = ((β Γ {0})βπ)) |
34 | 33 | ralrimiva 3147 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β βπ β β ((π β π)βπ) = ((β Γ {0})βπ)) |
35 | | ffn 6718 |
. . . . . . . . . 10
β’ (π: ββΆβ β
π Fn
β) |
36 | 23, 35 | ax-mp 5 |
. . . . . . . . 9
β’ π Fn β |
37 | | simpl 484 |
. . . . . . . . . 10
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π:ββΆ(nullβπ)) |
38 | 2 | shssii 30497 |
. . . . . . . . . 10
β’
(nullβπ)
β β |
39 | | fss 6735 |
. . . . . . . . . 10
β’ ((π:ββΆ(nullβπ) β§ (nullβπ) β β) β π:ββΆ β) |
40 | 37, 38, 39 | sylancl 587 |
. . . . . . . . 9
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π:ββΆ β) |
41 | | fnfco 6757 |
. . . . . . . . 9
β’ ((π Fn β β§ π:ββΆ β) β
(π β π) Fn β) |
42 | 36, 40, 41 | sylancr 588 |
. . . . . . . 8
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (π β π) Fn β) |
43 | 30 | fconst 6778 |
. . . . . . . . 9
β’ (β
Γ {0}):ββΆ{0} |
44 | | ffn 6718 |
. . . . . . . . 9
β’ ((β
Γ {0}):ββΆ{0} β (β Γ {0}) Fn
β) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . 8
β’ (β
Γ {0}) Fn β |
46 | | eqfnfv 7033 |
. . . . . . . 8
β’ (((π β π) Fn β β§ (β Γ {0}) Fn
β) β ((π β
π) = (β Γ {0})
β βπ β
β ((π β π)βπ) = ((β Γ {0})βπ))) |
47 | 42, 45, 46 | sylancl 587 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β ((π β π) = (β Γ {0}) β
βπ β β
((π β π)βπ) = ((β Γ {0})βπ))) |
48 | 34, 47 | mpbird 257 |
. . . . . 6
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (π β π) = (β Γ {0})) |
49 | 6 | cnfldtopon 24299 |
. . . . . . . 8
β’
(TopOpenββfld) β
(TopOnββ) |
50 | 49 | a1i 11 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β
(TopOpenββfld) β
(TopOnββ)) |
51 | | 0cnd 11207 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β 0 β
β) |
52 | | 1zzd 12593 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β 1 β
β€) |
53 | | nnuz 12865 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
54 | 53 | lmconst 22765 |
. . . . . . 7
β’
(((TopOpenββfld) β (TopOnββ)
β§ 0 β β β§ 1 β β€) β (β Γ
{0})(βπ‘β(TopOpenββfld))0) |
55 | 50, 51, 52, 54 | syl3anc 1372 |
. . . . . 6
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (β Γ
{0})(βπ‘β(TopOpenββfld))0) |
56 | 48, 55 | eqbrtrd 5171 |
. . . . 5
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (π β π)(βπ‘β(TopOpenββfld))0) |
57 | 8, 22, 56 | lmmo 22884 |
. . . 4
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (πβπ₯) = 0) |
58 | | elnlfn 31212 |
. . . . 5
β’ (π: ββΆβ β
(π₯ β (nullβπ) β (π₯ β β β§ (πβπ₯) = 0))) |
59 | 23, 58 | ax-mp 5 |
. . . 4
β’ (π₯ β (nullβπ) β (π₯ β β β§ (πβπ₯) = 0)) |
60 | 5, 57, 59 | sylanbrc 584 |
. . 3
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π₯ β (nullβπ)) |
61 | 60 | gen2 1799 |
. 2
β’
βπβπ₯((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π₯ β (nullβπ)) |
62 | | isch2 30507 |
. 2
β’
((nullβπ)
β Cβ β ((nullβπ) β Sβ
β§ βπβπ₯((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π₯ β (nullβπ)))) |
63 | 2, 61, 62 | mpbir2an 710 |
1
β’
(nullβπ)
β Cβ |