Step | Hyp | Ref
| Expression |
1 | | nlelch.1 |
. . 3
β’ π β LinFn |
2 | 1 | nlelshi 31568 |
. 2
β’
(nullβπ)
β Sβ |
3 | | vex 3478 |
. . . . . 6
β’ π₯ β V |
4 | 3 | hlimveci 30698 |
. . . . 5
β’ (π βπ£
π₯ β π₯ β β) |
5 | 4 | adantl 482 |
. . . 4
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π₯ β β) |
6 | | eqid 2732 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
7 | 6 | cnfldhaus 24521 |
. . . . . 6
β’
(TopOpenββfld) β Haus |
8 | 7 | a1i 11 |
. . . . 5
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β
(TopOpenββfld) β Haus) |
9 | | eqid 2732 |
. . . . . . . . . 10
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
10 | | eqid 2732 |
. . . . . . . . . . 11
β’
(normβ β ββ ) =
(normβ β ββ ) |
11 | 9, 10 | hhims 30680 |
. . . . . . . . . 10
β’
(normβ β ββ ) =
(IndMetββ¨β¨ +β ,
Β·β β©,
normββ©) |
12 | | eqid 2732 |
. . . . . . . . . 10
β’
(MetOpenβ(normβ β
ββ )) = (MetOpenβ(normβ β
ββ )) |
13 | 9, 11, 12 | hhlm 30707 |
. . . . . . . . 9
β’
βπ£ =
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) |
14 | | resss 6006 |
. . . . . . . . 9
β’
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) β
(βπ‘β(MetOpenβ(normβ β
ββ ))) |
15 | 13, 14 | eqsstri 4016 |
. . . . . . . 8
β’
βπ£ β
(βπ‘β(MetOpenβ(normβ
β ββ ))) |
16 | 15 | ssbri 5193 |
. . . . . . 7
β’ (π βπ£
π₯ β π(βπ‘β(MetOpenβ(normβ
β ββ )))π₯) |
17 | 16 | adantl 482 |
. . . . . 6
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π(βπ‘β(MetOpenβ(normβ
β ββ )))π₯) |
18 | | nlelch.2 |
. . . . . . . 8
β’ π β ContFn |
19 | 10, 12, 6 | hhcnf 31413 |
. . . . . . . 8
β’ ContFn =
((MetOpenβ(normβ β ββ ))
Cn (TopOpenββfld)) |
20 | 18, 19 | eleqtri 2831 |
. . . . . . 7
β’ π β
((MetOpenβ(normβ β ββ ))
Cn (TopOpenββfld)) |
21 | 20 | a1i 11 |
. . . . . 6
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π β
((MetOpenβ(normβ β ββ ))
Cn (TopOpenββfld))) |
22 | 17, 21 | lmcn 23029 |
. . . . 5
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (π β π)(βπ‘β(TopOpenββfld))(πβπ₯)) |
23 | 1 | lnfnfi 31549 |
. . . . . . . . . 10
β’ π:
ββΆβ |
24 | | ffvelcdm 7083 |
. . . . . . . . . . 11
β’ ((π:ββΆ(nullβπ) β§ π β β) β (πβπ) β (nullβπ)) |
25 | 24 | adantlr 713 |
. . . . . . . . . 10
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β (πβπ) β (nullβπ)) |
26 | | elnlfn2 31437 |
. . . . . . . . . 10
β’ ((π: ββΆβ β§
(πβπ) β (nullβπ)) β (πβ(πβπ)) = 0) |
27 | 23, 25, 26 | sylancr 587 |
. . . . . . . . 9
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β (πβ(πβπ)) = 0) |
28 | | fvco3 6990 |
. . . . . . . . . 10
β’ ((π:ββΆ(nullβπ) β§ π β β) β ((π β π)βπ) = (πβ(πβπ))) |
29 | 28 | adantlr 713 |
. . . . . . . . 9
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β ((π β π)βπ) = (πβ(πβπ))) |
30 | | c0ex 11212 |
. . . . . . . . . . 11
β’ 0 β
V |
31 | 30 | fvconst2 7207 |
. . . . . . . . . 10
β’ (π β β β ((β
Γ {0})βπ) =
0) |
32 | 31 | adantl 482 |
. . . . . . . . 9
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β ((β Γ
{0})βπ) =
0) |
33 | 27, 29, 32 | 3eqtr4d 2782 |
. . . . . . . 8
β’ (((π:ββΆ(nullβπ) β§ π βπ£ π₯) β§ π β β) β ((π β π)βπ) = ((β Γ {0})βπ)) |
34 | 33 | ralrimiva 3146 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β βπ β β ((π β π)βπ) = ((β Γ {0})βπ)) |
35 | | ffn 6717 |
. . . . . . . . . 10
β’ (π: ββΆβ β
π Fn
β) |
36 | 23, 35 | ax-mp 5 |
. . . . . . . . 9
β’ π Fn β |
37 | | simpl 483 |
. . . . . . . . . 10
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π:ββΆ(nullβπ)) |
38 | 2 | shssii 30721 |
. . . . . . . . . 10
β’
(nullβπ)
β β |
39 | | fss 6734 |
. . . . . . . . . 10
β’ ((π:ββΆ(nullβπ) β§ (nullβπ) β β) β π:ββΆ β) |
40 | 37, 38, 39 | sylancl 586 |
. . . . . . . . 9
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π:ββΆ β) |
41 | | fnfco 6756 |
. . . . . . . . 9
β’ ((π Fn β β§ π:ββΆ β) β
(π β π) Fn β) |
42 | 36, 40, 41 | sylancr 587 |
. . . . . . . 8
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (π β π) Fn β) |
43 | 30 | fconst 6777 |
. . . . . . . . 9
β’ (β
Γ {0}):ββΆ{0} |
44 | | ffn 6717 |
. . . . . . . . 9
β’ ((β
Γ {0}):ββΆ{0} β (β Γ {0}) Fn
β) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . 8
β’ (β
Γ {0}) Fn β |
46 | | eqfnfv 7032 |
. . . . . . . 8
β’ (((π β π) Fn β β§ (β Γ {0}) Fn
β) β ((π β
π) = (β Γ {0})
β βπ β
β ((π β π)βπ) = ((β Γ {0})βπ))) |
47 | 42, 45, 46 | sylancl 586 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β ((π β π) = (β Γ {0}) β
βπ β β
((π β π)βπ) = ((β Γ {0})βπ))) |
48 | 34, 47 | mpbird 256 |
. . . . . 6
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (π β π) = (β Γ {0})) |
49 | 6 | cnfldtopon 24519 |
. . . . . . . 8
β’
(TopOpenββfld) β
(TopOnββ) |
50 | 49 | a1i 11 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β
(TopOpenββfld) β
(TopOnββ)) |
51 | | 0cnd 11211 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β 0 β
β) |
52 | | 1zzd 12597 |
. . . . . . 7
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β 1 β
β€) |
53 | | nnuz 12869 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
54 | 53 | lmconst 22985 |
. . . . . . 7
β’
(((TopOpenββfld) β (TopOnββ)
β§ 0 β β β§ 1 β β€) β (β Γ
{0})(βπ‘β(TopOpenββfld))0) |
55 | 50, 51, 52, 54 | syl3anc 1371 |
. . . . . 6
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (β Γ
{0})(βπ‘β(TopOpenββfld))0) |
56 | 48, 55 | eqbrtrd 5170 |
. . . . 5
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (π β π)(βπ‘β(TopOpenββfld))0) |
57 | 8, 22, 56 | lmmo 23104 |
. . . 4
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β (πβπ₯) = 0) |
58 | | elnlfn 31436 |
. . . . 5
β’ (π: ββΆβ β
(π₯ β (nullβπ) β (π₯ β β β§ (πβπ₯) = 0))) |
59 | 23, 58 | ax-mp 5 |
. . . 4
β’ (π₯ β (nullβπ) β (π₯ β β β§ (πβπ₯) = 0)) |
60 | 5, 57, 59 | sylanbrc 583 |
. . 3
β’ ((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π₯ β (nullβπ)) |
61 | 60 | gen2 1798 |
. 2
β’
βπβπ₯((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π₯ β (nullβπ)) |
62 | | isch2 30731 |
. 2
β’
((nullβπ)
β Cβ β ((nullβπ) β Sβ
β§ βπβπ₯((π:ββΆ(nullβπ) β§ π βπ£ π₯) β π₯ β (nullβπ)))) |
63 | 2, 61, 62 | mpbir2an 709 |
1
β’
(nullβπ)
β Cβ |