Step | Hyp | Ref
| Expression |
1 | | cphphl 24558 |
. . . . 5
β’ (π β βPreHil β
π β
PreHil) |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
3 | | ipcn.f |
. . . . . 6
β’ , =
(Β·ifβπ) |
4 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
5 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
6 | 2, 3, 4, 5 | phlipf 21079 |
. . . . 5
β’ (π β PreHil β ,
:((Baseβπ) Γ
(Baseβπ))βΆ(Baseβ(Scalarβπ))) |
7 | 1, 6 | syl 17 |
. . . 4
β’ (π β βPreHil β
,
:((Baseβπ) Γ
(Baseβπ))βΆ(Baseβ(Scalarβπ))) |
8 | | cphclm 24576 |
. . . . 5
β’ (π β βPreHil β
π β
βMod) |
9 | 4, 5 | clmsscn 24465 |
. . . . 5
β’ (π β βMod β
(Baseβ(Scalarβπ)) β β) |
10 | 8, 9 | syl 17 |
. . . 4
β’ (π β βPreHil β
(Baseβ(Scalarβπ)) β β) |
11 | 7, 10 | fssd 6690 |
. . 3
β’ (π β βPreHil β
,
:((Baseβπ) Γ
(Baseβπ))βΆβ) |
12 | | eqid 2733 |
. . . . . . 7
β’
(Β·πβπ) =
(Β·πβπ) |
13 | | eqid 2733 |
. . . . . . 7
β’
(distβπ) =
(distβπ) |
14 | | eqid 2733 |
. . . . . . 7
β’
(normβπ) =
(normβπ) |
15 | | eqid 2733 |
. . . . . . 7
β’ ((π / 2) / (((normβπ)βπ₯) + 1)) = ((π / 2) / (((normβπ)βπ₯) + 1)) |
16 | | eqid 2733 |
. . . . . . 7
β’ ((π / 2) / (((normβπ)βπ¦) + ((π / 2) / (((normβπ)βπ₯) + 1)))) = ((π / 2) / (((normβπ)βπ¦) + ((π / 2) / (((normβπ)βπ₯) + 1)))) |
17 | | simpll 766 |
. . . . . . 7
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ π β β+) β π β
βPreHil) |
18 | | simplrl 776 |
. . . . . . 7
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ π β β+) β π₯ β (Baseβπ)) |
19 | | simplrr 777 |
. . . . . . 7
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ π β β+) β π¦ β (Baseβπ)) |
20 | | simpr 486 |
. . . . . . 7
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ π β β+) β π β
β+) |
21 | 2, 12, 13, 14, 15, 16, 17, 18, 19, 20 | ipcnlem1 24632 |
. . . . . 6
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ π β β+) β
βπ β
β+ βπ§ β (Baseβπ)βπ€ β (Baseβπ)(((π₯(distβπ)π§) < π β§ (π¦(distβπ)π€) < π ) β (absβ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€))) < π)) |
22 | 21 | ralrimiva 3140 |
. . . . 5
β’ ((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β βπ β β+ βπ β β+
βπ§ β
(Baseβπ)βπ€ β (Baseβπ)(((π₯(distβπ)π§) < π β§ (π¦(distβπ)π€) < π ) β (absβ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€))) < π)) |
23 | | simplrl 776 |
. . . . . . . . . . . 12
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β π₯ β (Baseβπ)) |
24 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β π§ β (Baseβπ)) |
25 | 23, 24 | ovresd 7525 |
. . . . . . . . . . 11
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β (π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) = (π₯(distβπ)π§)) |
26 | 25 | breq1d 5119 |
. . . . . . . . . 10
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β ((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β (π₯(distβπ)π§) < π )) |
27 | | simplrr 777 |
. . . . . . . . . . . 12
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β π¦ β (Baseβπ)) |
28 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β π€ β (Baseβπ)) |
29 | 27, 28 | ovresd 7525 |
. . . . . . . . . . 11
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) = (π¦(distβπ)π€)) |
30 | 29 | breq1d 5119 |
. . . . . . . . . 10
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β ((π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π β (π¦(distβπ)π€) < π )) |
31 | 26, 30 | anbi12d 632 |
. . . . . . . . 9
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β (((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯(distβπ)π§) < π β§ (π¦(distβπ)π€) < π ))) |
32 | 11 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β , :((Baseβπ) Γ (Baseβπ))βΆβ) |
33 | 32, 23, 27 | fovcdmd 7530 |
. . . . . . . . . . . 12
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β (π₯ , π¦) β β) |
34 | 32, 24, 28 | fovcdmd 7530 |
. . . . . . . . . . . 12
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β (π§ , π€) β β) |
35 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (abs
β β ) = (abs β β ) |
36 | 35 | cnmetdval 24157 |
. . . . . . . . . . . 12
β’ (((π₯ , π¦) β β β§ (π§ , π€) β β) β ((π₯ , π¦)(abs β β )(π§ , π€)) = (absβ((π₯ , π¦) β (π§ , π€)))) |
37 | 33, 34, 36 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β ((π₯ , π¦)(abs β β )(π§ , π€)) = (absβ((π₯ , π¦) β (π§ , π€)))) |
38 | 2, 12, 3 | ipfval 21076 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯ , π¦) = (π₯(Β·πβπ)π¦)) |
39 | 23, 27, 38 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β (π₯ , π¦) = (π₯(Β·πβπ)π¦)) |
40 | 2, 12, 3 | ipfval 21076 |
. . . . . . . . . . . . . 14
β’ ((π§ β (Baseβπ) β§ π€ β (Baseβπ)) β (π§ , π€) = (π§(Β·πβπ)π€)) |
41 | 40 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β (π§ , π€) = (π§(Β·πβπ)π€)) |
42 | 39, 41 | oveq12d 7379 |
. . . . . . . . . . . 12
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β ((π₯ , π¦) β (π§ , π€)) = ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€))) |
43 | 42 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β (absβ((π₯ , π¦) β (π§ , π€))) = (absβ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€)))) |
44 | 37, 43 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β ((π₯ , π¦)(abs β β )(π§ , π€)) = (absβ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€)))) |
45 | 44 | breq1d 5119 |
. . . . . . . . 9
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β (((π₯ , π¦)(abs β β )(π§ , π€)) < π β (absβ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€))) < π)) |
46 | 31, 45 | imbi12d 345 |
. . . . . . . 8
β’ (((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β§ (π§ β (Baseβπ) β§ π€ β (Baseβπ))) β ((((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ , π¦)(abs β β )(π§ , π€)) < π) β (((π₯(distβπ)π§) < π β§ (π¦(distβπ)π€) < π ) β (absβ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€))) < π))) |
47 | 46 | 2ralbidva 3207 |
. . . . . . 7
β’ ((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (βπ§ β (Baseβπ)βπ€ β (Baseβπ)(((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ , π¦)(abs β β )(π§ , π€)) < π) β βπ§ β (Baseβπ)βπ€ β (Baseβπ)(((π₯(distβπ)π§) < π β§ (π¦(distβπ)π€) < π ) β (absβ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€))) < π))) |
48 | 47 | rexbidv 3172 |
. . . . . 6
β’ ((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (βπ β β+ βπ§ β (Baseβπ)βπ€ β (Baseβπ)(((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ , π¦)(abs β β )(π§ , π€)) < π) β βπ β β+ βπ§ β (Baseβπ)βπ€ β (Baseβπ)(((π₯(distβπ)π§) < π β§ (π¦(distβπ)π€) < π ) β (absβ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€))) < π))) |
49 | 48 | ralbidv 3171 |
. . . . 5
β’ ((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (βπ β β+ βπ β β+
βπ§ β
(Baseβπ)βπ€ β (Baseβπ)(((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ , π¦)(abs β β )(π§ , π€)) < π) β βπ β β+ βπ β β+
βπ§ β
(Baseβπ)βπ€ β (Baseβπ)(((π₯(distβπ)π§) < π β§ (π¦(distβπ)π€) < π ) β (absβ((π₯(Β·πβπ)π¦) β (π§(Β·πβπ)π€))) < π))) |
50 | 22, 49 | mpbird 257 |
. . . 4
β’ ((π β βPreHil β§
(π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β βπ β β+ βπ β β+
βπ§ β
(Baseβπ)βπ€ β (Baseβπ)(((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ , π¦)(abs β β )(π§ , π€)) < π)) |
51 | 50 | ralrimivva 3194 |
. . 3
β’ (π β βPreHil β
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)βπ β β+ βπ β β+
βπ§ β
(Baseβπ)βπ€ β (Baseβπ)(((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ , π¦)(abs β β )(π§ , π€)) < π)) |
52 | | cphngp 24560 |
. . . . . . 7
β’ (π β βPreHil β
π β
NrmGrp) |
53 | | ngpms 23979 |
. . . . . . 7
β’ (π β NrmGrp β π β MetSp) |
54 | 52, 53 | syl 17 |
. . . . . 6
β’ (π β βPreHil β
π β
MetSp) |
55 | | msxms 23830 |
. . . . . 6
β’ (π β MetSp β π β
βMetSp) |
56 | 54, 55 | syl 17 |
. . . . 5
β’ (π β βPreHil β
π β
βMetSp) |
57 | | eqid 2733 |
. . . . . 6
β’
((distβπ)
βΎ ((Baseβπ)
Γ (Baseβπ))) =
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) |
58 | 2, 57 | xmsxmet 23832 |
. . . . 5
β’ (π β βMetSp β
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) β
(βMetβ(Baseβπ))) |
59 | 56, 58 | syl 17 |
. . . 4
β’ (π β βPreHil β
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) β
(βMetβ(Baseβπ))) |
60 | | cnxmet 24159 |
. . . . 5
β’ (abs
β β ) β (βMetββ) |
61 | 60 | a1i 11 |
. . . 4
β’ (π β βPreHil β
(abs β β ) β (βMetββ)) |
62 | | eqid 2733 |
. . . . 5
β’
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) = (MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) |
63 | | ipcn.k |
. . . . . 6
β’ πΎ =
(TopOpenββfld) |
64 | 63 | cnfldtopn 24168 |
. . . . 5
β’ πΎ = (MetOpenβ(abs β
β )) |
65 | 62, 62, 64 | txmetcn 23927 |
. . . 4
β’
((((distβπ)
βΎ ((Baseβπ)
Γ (Baseβπ)))
β (βMetβ(Baseβπ)) β§ ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))) β
(βMetβ(Baseβπ)) β§ (abs β β ) β
(βMetββ)) β ( , β
(((MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) Cn πΎ) β ( , :((Baseβπ) Γ (Baseβπ))βΆβ β§
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)βπ β β+ βπ β β+
βπ§ β
(Baseβπ)βπ€ β (Baseβπ)(((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ , π¦)(abs β β )(π§ , π€)) < π)))) |
66 | 59, 59, 61, 65 | syl3anc 1372 |
. . 3
β’ (π β βPreHil β (
, β
(((MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) Cn πΎ) β ( , :((Baseβπ) Γ (Baseβπ))βΆβ β§
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)βπ β β+ βπ β β+
βπ§ β
(Baseβπ)βπ€ β (Baseβπ)(((π₯((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π§) < π β§ (π¦((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))π€) < π ) β ((π₯ , π¦)(abs β β )(π§ , π€)) < π)))) |
67 | 11, 51, 66 | mpbir2and 712 |
. 2
β’ (π β βPreHil β
, β
(((MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) Cn πΎ)) |
68 | | ipcn.j |
. . . . . 6
β’ π½ = (TopOpenβπ) |
69 | 68, 2, 57 | mstopn 23828 |
. . . . 5
β’ (π β MetSp β π½ =
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) |
70 | 54, 69 | syl 17 |
. . . 4
β’ (π β βPreHil β
π½ =
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) |
71 | 70, 70 | oveq12d 7379 |
. . 3
β’ (π β βPreHil β
(π½ Γt
π½) =
((MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))))) |
72 | 71 | oveq1d 7376 |
. 2
β’ (π β βPreHil β
((π½ Γt
π½) Cn πΎ) = (((MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ)))) Γt
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))) Cn πΎ)) |
73 | 67, 72 | eleqtrrd 2837 |
1
β’ (π β βPreHil β
, β
((π½ Γt
π½) Cn πΎ)) |