Step | Hyp | Ref
| Expression |
1 | | hmopidmch.1 |
. . . 4
β’ π β HrmOp |
2 | | hmoplin 30926 |
. . . 4
β’ (π β HrmOp β π β LinOp) |
3 | 1, 2 | ax-mp 5 |
. . 3
β’ π β LinOp |
4 | 3 | rnelshi 31043 |
. 2
β’ ran π β
Sβ |
5 | | eqid 2733 |
. . . . . . . 8
β’
(normβ β ββ ) =
(normβ β ββ ) |
6 | 5 | hilxmet 30179 |
. . . . . . 7
β’
(normβ β ββ ) β
(βMetβ β) |
7 | | eqid 2733 |
. . . . . . . 8
β’
(MetOpenβ(normβ β
ββ )) = (MetOpenβ(normβ β
ββ )) |
8 | 7 | methaus 23892 |
. . . . . . 7
β’
((normβ β ββ ) β
(βMetβ β) β (MetOpenβ(normβ
β ββ )) β Haus) |
9 | 6, 8 | mp1i 13 |
. . . . . 6
β’ ((π:ββΆran π β§ π βπ£ π₯) β
(MetOpenβ(normβ β ββ ))
β Haus) |
10 | | eqid 2733 |
. . . . . . . . . . . 12
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
11 | 10, 5 | hhims 30156 |
. . . . . . . . . . . 12
β’
(normβ β ββ ) =
(IndMetββ¨β¨ +β ,
Β·β β©,
normββ©) |
12 | 10, 11, 7 | hhlm 30183 |
. . . . . . . . . . 11
β’
βπ£ =
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) |
13 | | resss 5963 |
. . . . . . . . . . 11
β’
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) β
(βπ‘β(MetOpenβ(normβ β
ββ ))) |
14 | 12, 13 | eqsstri 3979 |
. . . . . . . . . 10
β’
βπ£ β
(βπ‘β(MetOpenβ(normβ
β ββ ))) |
15 | 14 | ssbri 5151 |
. . . . . . . . 9
β’ (π βπ£
π₯ β π(βπ‘β(MetOpenβ(normβ
β ββ )))π₯) |
16 | 15 | adantl 483 |
. . . . . . . 8
β’ ((π:ββΆran π β§ π βπ£ π₯) β π(βπ‘β(MetOpenβ(normβ
β ββ )))π₯) |
17 | 7 | mopntopon 23808 |
. . . . . . . . . 10
β’
((normβ β ββ ) β
(βMetβ β) β (MetOpenβ(normβ
β ββ )) β (TopOnβ
β)) |
18 | 6, 17 | mp1i 13 |
. . . . . . . . 9
β’ ((π:ββΆran π β§ π βπ£ π₯) β
(MetOpenβ(normβ β ββ ))
β (TopOnβ β)) |
19 | 3 | lnopfi 30953 |
. . . . . . . . . . . 12
β’ π: ββΆ
β |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
β’ ((π:ββΆran π β§ π βπ£ π₯) β π: ββΆ β) |
21 | 20 | feqmptd 6911 |
. . . . . . . . . 10
β’ ((π:ββΆran π β§ π βπ£ π₯) β π = (π¦ β β β¦ (πβπ¦))) |
22 | | hmopbdoptHIL 30972 |
. . . . . . . . . . . . 13
β’ (π β HrmOp β π β
BndLinOp) |
23 | 1, 22 | ax-mp 5 |
. . . . . . . . . . . 12
β’ π β
BndLinOp |
24 | | lnopcnbd 31020 |
. . . . . . . . . . . . 13
β’ (π β LinOp β (π β ContOp β π β
BndLinOp)) |
25 | 3, 24 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (π β ContOp β π β
BndLinOp) |
26 | 23, 25 | mpbir 230 |
. . . . . . . . . . 11
β’ π β ContOp |
27 | 5, 7 | hhcno 30888 |
. . . . . . . . . . 11
β’ ContOp =
((MetOpenβ(normβ β ββ ))
Cn (MetOpenβ(normβ β ββ
))) |
28 | 26, 27 | eleqtri 2832 |
. . . . . . . . . 10
β’ π β
((MetOpenβ(normβ β ββ ))
Cn (MetOpenβ(normβ β ββ
))) |
29 | 21, 28 | eqeltrrdi 2843 |
. . . . . . . . 9
β’ ((π:ββΆran π β§ π βπ£ π₯) β (π¦ β β β¦ (πβπ¦)) β
((MetOpenβ(normβ β ββ ))
Cn (MetOpenβ(normβ β ββ
)))) |
30 | 18 | cnmptid 23028 |
. . . . . . . . 9
β’ ((π:ββΆran π β§ π βπ£ π₯) β (π¦ β β β¦ π¦) β
((MetOpenβ(normβ β ββ ))
Cn (MetOpenβ(normβ β ββ
)))) |
31 | 10 | hhnv 30149 |
. . . . . . . . . 10
β’
β¨β¨ +β , Β·β
β©, normββ© β NrmCVec |
32 | 10 | hhvs 30154 |
. . . . . . . . . . 11
β’
ββ = ( βπ£ ββ¨β¨
+β , Β·β β©,
normββ©) |
33 | 11, 7, 32 | vmcn 29683 |
. . . . . . . . . 10
β’
(β¨β¨ +β , Β·β
β©, normββ© β NrmCVec β
ββ β (((MetOpenβ(normβ
β ββ )) Γt
(MetOpenβ(normβ β ββ )))
Cn (MetOpenβ(normβ β ββ
)))) |
34 | 31, 33 | mp1i 13 |
. . . . . . . . 9
β’ ((π:ββΆran π β§ π βπ£ π₯) β
ββ β (((MetOpenβ(normβ
β ββ )) Γt
(MetOpenβ(normβ β ββ )))
Cn (MetOpenβ(normβ β ββ
)))) |
35 | 18, 29, 30, 34 | cnmpt12f 23033 |
. . . . . . . 8
β’ ((π:ββΆran π β§ π βπ£ π₯) β (π¦ β β β¦ ((πβπ¦) ββ π¦)) β
((MetOpenβ(normβ β ββ ))
Cn (MetOpenβ(normβ β ββ
)))) |
36 | 16, 35 | lmcn 22672 |
. . . . . . 7
β’ ((π:ββΆran π β§ π βπ£ π₯) β ((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π)(βπ‘β(MetOpenβ(normβ
β ββ )))((π¦ β β
β¦ ((πβπ¦) ββ π¦))βπ₯)) |
37 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π:ββΆran π β§ π βπ£ π₯) β π:ββΆran π) |
38 | 4 | shssii 30197 |
. . . . . . . . . . . . . 14
β’ ran π β
β |
39 | | fss 6686 |
. . . . . . . . . . . . . 14
β’ ((π:ββΆran π β§ ran π β β) β π:ββΆ β) |
40 | 37, 38, 39 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π:ββΆran π β§ π βπ£ π₯) β π:ββΆ β) |
41 | 40 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β (πβπ) β β) |
42 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πβπ) β (πβπ¦) = (πβ(πβπ))) |
43 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πβπ) β π¦ = (πβπ)) |
44 | 42, 43 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π¦ = (πβπ) β ((πβπ¦) ββ π¦) = ((πβ(πβπ)) ββ (πβπ))) |
45 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π¦ β β β¦ ((πβπ¦) ββ π¦)) = (π¦ β β β¦ ((πβπ¦) ββ π¦)) |
46 | | ovex 7391 |
. . . . . . . . . . . . 13
β’ ((πβ(πβπ)) ββ (πβπ)) β V |
47 | 44, 45, 46 | fvmpt 6949 |
. . . . . . . . . . . 12
β’ ((πβπ) β β β ((π¦ β β β¦ ((πβπ¦) ββ π¦))β(πβπ)) = ((πβ(πβπ)) ββ (πβπ))) |
48 | 41, 47 | syl 17 |
. . . . . . . . . . 11
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β ((π¦ β β β¦ ((πβπ¦) ββ π¦))β(πβπ)) = ((πβ(πβπ)) ββ (πβπ))) |
49 | | ffn 6669 |
. . . . . . . . . . . . . . . 16
β’ (π: ββΆ β β
π Fn
β) |
50 | 19, 49 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ π Fn β |
51 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (πβπ₯) β (πβπ¦) = (πβ(πβπ₯))) |
52 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (πβπ₯) β π¦ = (πβπ₯)) |
53 | 51, 52 | eqeq12d 2749 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (πβπ₯) β ((πβπ¦) = π¦ β (πβ(πβπ₯)) = (πβπ₯))) |
54 | 53 | ralrn 7039 |
. . . . . . . . . . . . . . 15
β’ (π Fn β β
(βπ¦ β ran π(πβπ¦) = π¦ β βπ₯ β β (πβ(πβπ₯)) = (πβπ₯))) |
55 | 50, 54 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
(βπ¦ β
ran π(πβπ¦) = π¦ β βπ₯ β β (πβ(πβπ₯)) = (πβπ₯)) |
56 | 19, 19 | hocoi 30748 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β ((π β π)βπ₯) = (πβ(πβπ₯))) |
57 | | hmopidmch.2 |
. . . . . . . . . . . . . . . 16
β’ (π β π) = π |
58 | 57 | fveq1i 6844 |
. . . . . . . . . . . . . . 15
β’ ((π β π)βπ₯) = (πβπ₯) |
59 | 56, 58 | eqtr3di 2788 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (πβ(πβπ₯)) = (πβπ₯)) |
60 | 55, 59 | mprgbir 3068 |
. . . . . . . . . . . . 13
β’
βπ¦ β ran
π(πβπ¦) = π¦ |
61 | | ffvelcdm 7033 |
. . . . . . . . . . . . . 14
β’ ((π:ββΆran π β§ π β β) β (πβπ) β ran π) |
62 | 61 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β (πβπ) β ran π) |
63 | 42, 43 | eqeq12d 2749 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πβπ) β ((πβπ¦) = π¦ β (πβ(πβπ)) = (πβπ))) |
64 | 63 | rspccv 3577 |
. . . . . . . . . . . . 13
β’
(βπ¦ β
ran π(πβπ¦) = π¦ β ((πβπ) β ran π β (πβ(πβπ)) = (πβπ))) |
65 | 60, 62, 64 | mpsyl 68 |
. . . . . . . . . . . 12
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β (πβ(πβπ)) = (πβπ)) |
66 | 65, 41 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β (πβ(πβπ)) β β) |
67 | | hvsubeq0 30052 |
. . . . . . . . . . . . 13
β’ (((πβ(πβπ)) β β β§ (πβπ) β β) β (((πβ(πβπ)) ββ (πβπ)) = 0β β (πβ(πβπ)) = (πβπ))) |
68 | 66, 41, 67 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β (((πβ(πβπ)) ββ (πβπ)) = 0β β (πβ(πβπ)) = (πβπ))) |
69 | 65, 68 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β ((πβ(πβπ)) ββ (πβπ)) = 0β) |
70 | 48, 69 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β ((π¦ β β β¦ ((πβπ¦) ββ π¦))β(πβπ)) = 0β) |
71 | | fvco3 6941 |
. . . . . . . . . . 11
β’ ((π:ββΆran π β§ π β β) β (((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π)βπ) = ((π¦ β β β¦ ((πβπ¦) ββ π¦))β(πβπ))) |
72 | 71 | adantlr 714 |
. . . . . . . . . 10
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β (((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π)βπ) = ((π¦ β β β¦ ((πβπ¦) ββ π¦))β(πβπ))) |
73 | | ax-hv0cl 29987 |
. . . . . . . . . . . . 13
β’
0β β β |
74 | 73 | elexi 3463 |
. . . . . . . . . . . 12
β’
0β β V |
75 | 74 | fvconst2 7154 |
. . . . . . . . . . 11
β’ (π β β β ((β
Γ {0β})βπ) = 0β) |
76 | 75 | adantl 483 |
. . . . . . . . . 10
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β ((β Γ
{0β})βπ) = 0β) |
77 | 70, 72, 76 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ (((π:ββΆran π β§ π βπ£ π₯) β§ π β β) β (((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π)βπ) = ((β Γ
{0β})βπ)) |
78 | 77 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π:ββΆran π β§ π βπ£ π₯) β βπ β β (((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π)βπ) = ((β Γ
{0β})βπ)) |
79 | | ovex 7391 |
. . . . . . . . . . 11
β’ ((πβπ¦) ββ π¦) β V |
80 | 79, 45 | fnmpti 6645 |
. . . . . . . . . 10
β’ (π¦ β β β¦ ((πβπ¦) ββ π¦)) Fn β |
81 | | fnfco 6708 |
. . . . . . . . . 10
β’ (((π¦ β β β¦ ((πβπ¦) ββ π¦)) Fn β β§ π:ββΆ β) β
((π¦ β β β¦
((πβπ¦) ββ
π¦)) β π) Fn β) |
82 | 80, 40, 81 | sylancr 588 |
. . . . . . . . 9
β’ ((π:ββΆran π β§ π βπ£ π₯) β ((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π) Fn β) |
83 | 74 | fconst 6729 |
. . . . . . . . . 10
β’ (β
Γ
{0β}):ββΆ{0β} |
84 | | ffn 6669 |
. . . . . . . . . 10
β’ ((β
Γ {0β}):ββΆ{0β} β
(β Γ {0β}) Fn β) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . 9
β’ (β
Γ {0β}) Fn β |
86 | | eqfnfv 6983 |
. . . . . . . . 9
β’ ((((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π) Fn β β§ (β Γ
{0β}) Fn β) β (((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π) = (β Γ {0β})
β βπ β
β (((π¦ β β
β¦ ((πβπ¦) ββ
π¦)) β π)βπ) = ((β Γ
{0β})βπ))) |
87 | 82, 85, 86 | sylancl 587 |
. . . . . . . 8
β’ ((π:ββΆran π β§ π βπ£ π₯) β (((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π) = (β Γ {0β})
β βπ β
β (((π¦ β β
β¦ ((πβπ¦) ββ
π¦)) β π)βπ) = ((β Γ
{0β})βπ))) |
88 | 78, 87 | mpbird 257 |
. . . . . . 7
β’ ((π:ββΆran π β§ π βπ£ π₯) β ((π¦ β β β¦ ((πβπ¦) ββ π¦)) β π) = (β Γ
{0β})) |
89 | | vex 3448 |
. . . . . . . . . 10
β’ π₯ β V |
90 | 89 | hlimveci 30174 |
. . . . . . . . 9
β’ (π βπ£
π₯ β π₯ β β) |
91 | 90 | adantl 483 |
. . . . . . . 8
β’ ((π:ββΆran π β§ π βπ£ π₯) β π₯ β β) |
92 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (πβπ¦) = (πβπ₯)) |
93 | | id 22 |
. . . . . . . . . 10
β’ (π¦ = π₯ β π¦ = π₯) |
94 | 92, 93 | oveq12d 7376 |
. . . . . . . . 9
β’ (π¦ = π₯ β ((πβπ¦) ββ π¦) = ((πβπ₯) ββ π₯)) |
95 | | ovex 7391 |
. . . . . . . . 9
β’ ((πβπ₯) ββ π₯) β V |
96 | 94, 45, 95 | fvmpt 6949 |
. . . . . . . 8
β’ (π₯ β β β ((π¦ β β β¦ ((πβπ¦) ββ π¦))βπ₯) = ((πβπ₯) ββ π₯)) |
97 | 91, 96 | syl 17 |
. . . . . . 7
β’ ((π:ββΆran π β§ π βπ£ π₯) β ((π¦ β β β¦ ((πβπ¦) ββ π¦))βπ₯) = ((πβπ₯) ββ π₯)) |
98 | 36, 88, 97 | 3brtr3d 5137 |
. . . . . 6
β’ ((π:ββΆran π β§ π βπ£ π₯) β (β Γ
{0β})(βπ‘β(MetOpenβ(normβ
β ββ )))((πβπ₯)
ββ π₯)) |
99 | 73 | a1i 11 |
. . . . . . 7
β’ ((π:ββΆran π β§ π βπ£ π₯) β 0β
β β) |
100 | | 1zzd 12539 |
. . . . . . 7
β’ ((π:ββΆran π β§ π βπ£ π₯) β 1 β
β€) |
101 | | nnuz 12811 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
102 | 101 | lmconst 22628 |
. . . . . . 7
β’
(((MetOpenβ(normβ β
ββ )) β (TopOnβ β) β§
0β β β β§ 1 β β€) β (β
Γ
{0β})(βπ‘β(MetOpenβ(normβ
β ββ )))0β) |
103 | 18, 99, 100, 102 | syl3anc 1372 |
. . . . . 6
β’ ((π:ββΆran π β§ π βπ£ π₯) β (β Γ
{0β})(βπ‘β(MetOpenβ(normβ
β ββ )))0β) |
104 | 9, 98, 103 | lmmo 22747 |
. . . . 5
β’ ((π:ββΆran π β§ π βπ£ π₯) β ((πβπ₯) ββ π₯) =
0β) |
105 | 19 | ffvelcdmi 7035 |
. . . . . . 7
β’ (π₯ β β β (πβπ₯) β β) |
106 | 91, 105 | syl 17 |
. . . . . 6
β’ ((π:ββΆran π β§ π βπ£ π₯) β (πβπ₯) β β) |
107 | | hvsubeq0 30052 |
. . . . . 6
β’ (((πβπ₯) β β β§ π₯ β β) β (((πβπ₯) ββ π₯) = 0β β
(πβπ₯) = π₯)) |
108 | 106, 91, 107 | syl2anc 585 |
. . . . 5
β’ ((π:ββΆran π β§ π βπ£ π₯) β (((πβπ₯) ββ π₯) = 0β β
(πβπ₯) = π₯)) |
109 | 104, 108 | mpbid 231 |
. . . 4
β’ ((π:ββΆran π β§ π βπ£ π₯) β (πβπ₯) = π₯) |
110 | | fnfvelrn 7032 |
. . . . 5
β’ ((π Fn β β§ π₯ β β) β (πβπ₯) β ran π) |
111 | 50, 91, 110 | sylancr 588 |
. . . 4
β’ ((π:ββΆran π β§ π βπ£ π₯) β (πβπ₯) β ran π) |
112 | 109, 111 | eqeltrrd 2835 |
. . 3
β’ ((π:ββΆran π β§ π βπ£ π₯) β π₯ β ran π) |
113 | 112 | gen2 1799 |
. 2
β’
βπβπ₯((π:ββΆran π β§ π βπ£ π₯) β π₯ β ran π) |
114 | | isch2 30207 |
. 2
β’ (ran
π β
Cβ β (ran π β Sβ
β§ βπβπ₯((π:ββΆran π β§ π βπ£ π₯) β π₯ β ran π))) |
115 | 4, 113, 114 | mpbir2an 710 |
1
β’ ran π β
Cβ |