Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(BaseSetβπ) =
(BaseSetβπ) |
2 | | nmcvcn.1 |
. . 3
β’ π =
(normCVβπ) |
3 | 1, 2 | nvf 29644 |
. 2
β’ (π β NrmCVec β π:(BaseSetβπ)βΆβ) |
4 | | simprr 772 |
. . . 4
β’ ((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π β β+)) β π β
β+) |
5 | 1, 2 | nvcl 29645 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ)) β (πβπ₯) β β) |
6 | 5 | ex 414 |
. . . . . . . . . . . . 13
β’ (π β NrmCVec β (π₯ β (BaseSetβπ) β (πβπ₯) β β)) |
7 | 1, 2 | nvcl 29645 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ π¦ β (BaseSetβπ)) β (πβπ¦) β β) |
8 | 7 | ex 414 |
. . . . . . . . . . . . 13
β’ (π β NrmCVec β (π¦ β (BaseSetβπ) β (πβπ¦) β β)) |
9 | 6, 8 | anim12d 610 |
. . . . . . . . . . . 12
β’ (π β NrmCVec β ((π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β ((πβπ₯) β β β§ (πβπ¦) β β))) |
10 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
11 | 10 | remet 24169 |
. . . . . . . . . . . . 13
β’ ((abs
β β ) βΎ (β Γ β)) β
(Metββ) |
12 | | metcl 23701 |
. . . . . . . . . . . . 13
β’ ((((abs
β β ) βΎ (β Γ β)) β (Metββ)
β§ (πβπ₯) β β β§ (πβπ¦) β β) β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β β) |
13 | 11, 12 | mp3an1 1449 |
. . . . . . . . . . . 12
β’ (((πβπ₯) β β β§ (πβπ¦) β β) β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β β) |
14 | 9, 13 | syl6 35 |
. . . . . . . . . . 11
β’ (π β NrmCVec β ((π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β β)) |
15 | 14 | 3impib 1117 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β β) |
16 | | nmcvcn.2 |
. . . . . . . . . . . 12
β’ πΆ = (IndMetβπ) |
17 | 1, 16 | imsmet 29675 |
. . . . . . . . . . 11
β’ (π β NrmCVec β πΆ β
(Metβ(BaseSetβπ))) |
18 | | metcl 23701 |
. . . . . . . . . . 11
β’ ((πΆ β
(Metβ(BaseSetβπ)) β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β (π₯πΆπ¦) β β) |
19 | 17, 18 | syl3an1 1164 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β (π₯πΆπ¦) β β) |
20 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (
+π£ βπ) = ( +π£ βπ) |
21 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
22 | 1, 20, 21, 2 | nvabs 29656 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β (absβ((πβπ₯) β (πβπ¦))) β€ (πβ(π₯( +π£ βπ)(-1(
Β·π OLD βπ)π¦)))) |
23 | 9 | 3impib 1117 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β ((πβπ₯) β β β§ (πβπ¦) β β)) |
24 | 10 | remetdval 24168 |
. . . . . . . . . . . 12
β’ (((πβπ₯) β β β§ (πβπ¦) β β) β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) = (absβ((πβπ₯) β (πβπ¦)))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) = (absβ((πβπ₯) β (πβπ¦)))) |
26 | 1, 20, 21, 2, 16 | imsdval2 29671 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β (π₯πΆπ¦) = (πβ(π₯( +π£ βπ)(-1(
Β·π OLD βπ)π¦)))) |
27 | 22, 25, 26 | 3brtr4d 5138 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β€ (π₯πΆπ¦)) |
28 | 15, 19, 27 | jca31 516 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β ((((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β β β§ (π₯πΆπ¦) β β) β§ ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β€ (π₯πΆπ¦))) |
29 | 28 | 3expa 1119 |
. . . . . . . 8
β’ (((π β NrmCVec β§ π₯ β (BaseSetβπ)) β§ π¦ β (BaseSetβπ)) β ((((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β β β§ (π₯πΆπ¦) β β) β§ ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β€ (π₯πΆπ¦))) |
30 | | rpre 12928 |
. . . . . . . 8
β’ (π β β+
β π β
β) |
31 | | lelttr 11250 |
. . . . . . . . . . 11
β’ ((((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β β β§ (π₯πΆπ¦) β β β§ π β β) β ((((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β€ (π₯πΆπ¦) β§ (π₯πΆπ¦) < π) β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) |
32 | 31 | 3expa 1119 |
. . . . . . . . . 10
β’
(((((πβπ₯)((abs β β ) βΎ
(β Γ β))(πβπ¦)) β β β§ (π₯πΆπ¦) β β) β§ π β β) β ((((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β€ (π₯πΆπ¦) β§ (π₯πΆπ¦) < π) β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) |
33 | 32 | expdimp 454 |
. . . . . . . . 9
β’
((((((πβπ₯)((abs β β ) βΎ
(β Γ β))(πβπ¦)) β β β§ (π₯πΆπ¦) β β) β§ π β β) β§ ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β€ (π₯πΆπ¦)) β ((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) |
34 | 33 | an32s 651 |
. . . . . . . 8
β’
((((((πβπ₯)((abs β β ) βΎ
(β Γ β))(πβπ¦)) β β β§ (π₯πΆπ¦) β β) β§ ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) β€ (π₯πΆπ¦)) β§ π β β) β ((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) |
35 | 29, 30, 34 | syl2an 597 |
. . . . . . 7
β’ ((((π β NrmCVec β§ π₯ β (BaseSetβπ)) β§ π¦ β (BaseSetβπ)) β§ π β β+) β ((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) |
36 | 35 | ex 414 |
. . . . . 6
β’ (((π β NrmCVec β§ π₯ β (BaseSetβπ)) β§ π¦ β (BaseSetβπ)) β (π β β+ β ((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π))) |
37 | 36 | ralrimdva 3148 |
. . . . 5
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ)) β (π β β+ β
βπ¦ β
(BaseSetβπ)((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π))) |
38 | 37 | impr 456 |
. . . 4
β’ ((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π β β+)) β
βπ¦ β
(BaseSetβπ)((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) |
39 | | breq2 5110 |
. . . . 5
β’ (π = π β ((π₯πΆπ¦) < π β (π₯πΆπ¦) < π)) |
40 | 39 | rspceaimv 3584 |
. . . 4
β’ ((π β β+
β§ βπ¦ β
(BaseSetβπ)((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) β βπ β β+ βπ¦ β (BaseSetβπ)((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) |
41 | 4, 38, 40 | syl2anc 585 |
. . 3
β’ ((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π β β+)) β
βπ β
β+ βπ¦ β (BaseSetβπ)((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) |
42 | 41 | ralrimivva 3194 |
. 2
β’ (π β NrmCVec β
βπ₯ β
(BaseSetβπ)βπ β β+ βπ β β+
βπ¦ β
(BaseSetβπ)((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)) |
43 | 1, 16 | imsxmet 29676 |
. . 3
β’ (π β NrmCVec β πΆ β
(βMetβ(BaseSetβπ))) |
44 | 10 | rexmet 24170 |
. . 3
β’ ((abs
β β ) βΎ (β Γ β)) β
(βMetββ) |
45 | | nmcvcn.j |
. . . 4
β’ π½ = (MetOpenβπΆ) |
46 | | nmcvcn.k |
. . . . 5
β’ πΎ = (topGenβran
(,)) |
47 | | eqid 2733 |
. . . . . 6
β’
(MetOpenβ((abs β β ) βΎ (β Γ
β))) = (MetOpenβ((abs β β ) βΎ (β Γ
β))) |
48 | 10, 47 | tgioo 24175 |
. . . . 5
β’
(topGenβran (,)) = (MetOpenβ((abs β β ) βΎ
(β Γ β))) |
49 | 46, 48 | eqtri 2761 |
. . . 4
β’ πΎ = (MetOpenβ((abs β
β ) βΎ (β Γ β))) |
50 | 45, 49 | metcn 23915 |
. . 3
β’ ((πΆ β
(βMetβ(BaseSetβπ)) β§ ((abs β β ) βΎ
(β Γ β)) β (βMetββ)) β (π β (π½ Cn πΎ) β (π:(BaseSetβπ)βΆβ β§ βπ₯ β (BaseSetβπ)βπ β β+ βπ β β+
βπ¦ β
(BaseSetβπ)((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)))) |
51 | 43, 44, 50 | sylancl 587 |
. 2
β’ (π β NrmCVec β (π β (π½ Cn πΎ) β (π:(BaseSetβπ)βΆβ β§ βπ₯ β (BaseSetβπ)βπ β β+ βπ β β+
βπ¦ β
(BaseSetβπ)((π₯πΆπ¦) < π β ((πβπ₯)((abs β β ) βΎ (β
Γ β))(πβπ¦)) < π)))) |
52 | 3, 42, 51 | mpbir2and 712 |
1
β’ (π β NrmCVec β π β (π½ Cn πΎ)) |