Step | Hyp | Ref
| Expression |
1 | | axhil.2 |
. . . . . 6
โข ๐ โ
CHilOLD |
2 | | simpl 484 |
. . . . . 6
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ ๐น โ
(Cauโ(IndMetโ๐))) |
3 | | eqid 2733 |
. . . . . . 7
โข
(IndMetโ๐) =
(IndMetโ๐) |
4 | | eqid 2733 |
. . . . . . 7
โข
(MetOpenโ(IndMetโ๐)) = (MetOpenโ(IndMetโ๐)) |
5 | 3, 4 | hlcompl 29906 |
. . . . . 6
โข ((๐ โ CHilOLD โง
๐น โ
(Cauโ(IndMetโ๐))) โ ๐น โ dom
(โ๐กโ(MetOpenโ(IndMetโ๐)))) |
6 | 1, 2, 5 | sylancr 588 |
. . . . 5
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ ๐น โ
dom (โ๐กโ(MetOpenโ(IndMetโ๐)))) |
7 | | eldm2g 5859 |
. . . . . 6
โข (๐น โ
(Cauโ(IndMetโ๐)) โ (๐น โ dom
(โ๐กโ(MetOpenโ(IndMetโ๐))) โ โ๐ฅโจ๐น, ๐ฅโฉ โ
(โ๐กโ(MetOpenโ(IndMetโ๐))))) |
8 | 7 | adantr 482 |
. . . . 5
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ (๐น โ
dom (โ๐กโ(MetOpenโ(IndMetโ๐))) โ โ๐ฅโจ๐น, ๐ฅโฉ โ
(โ๐กโ(MetOpenโ(IndMetโ๐))))) |
9 | 6, 8 | mpbid 231 |
. . . 4
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ โ๐ฅโจ๐น, ๐ฅโฉ โ
(โ๐กโ(MetOpenโ(IndMetโ๐)))) |
10 | | df-br 5110 |
. . . . . 6
โข (๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ
โ โจ๐น, ๐ฅโฉ โ
(โ๐กโ(MetOpenโ(IndMetโ๐)))) |
11 | 1 | hlnvi 29883 |
. . . . . . . . . 10
โข ๐ โ NrmCVec |
12 | | df-hba 29960 |
. . . . . . . . . . . 12
โข โ
= (BaseSetโโจโจ +โ ,
ยทโ โฉ,
normโโฉ) |
13 | | axhil.1 |
. . . . . . . . . . . . 13
โข ๐ = โจโจ
+โ , ยทโ โฉ,
normโโฉ |
14 | 13 | fveq2i 6849 |
. . . . . . . . . . . 12
โข
(BaseSetโ๐) =
(BaseSetโโจโจ +โ ,
ยทโ โฉ,
normโโฉ) |
15 | 12, 14 | eqtr4i 2764 |
. . . . . . . . . . 11
โข โ
= (BaseSetโ๐) |
16 | 15, 3 | imsxmet 29683 |
. . . . . . . . . 10
โข (๐ โ NrmCVec โ
(IndMetโ๐) โ
(โMetโ โ)) |
17 | 4 | mopntopon 23815 |
. . . . . . . . . 10
โข
((IndMetโ๐)
โ (โMetโ โ) โ (MetOpenโ(IndMetโ๐)) โ (TopOnโ
โ)) |
18 | 11, 16, 17 | mp2b 10 |
. . . . . . . . 9
โข
(MetOpenโ(IndMetโ๐)) โ (TopOnโ
โ) |
19 | | lmcl 22671 |
. . . . . . . . 9
โข
(((MetOpenโ(IndMetโ๐)) โ (TopOnโ โ) โง ๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ)
โ ๐ฅ โ โ) |
20 | 18, 19 | mpan 689 |
. . . . . . . 8
โข (๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ
โ ๐ฅ โ โ) |
21 | 20 | a1i 11 |
. . . . . . 7
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ (๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ
โ ๐ฅ โ โ)) |
22 | 13, 11, 15, 3, 4 | h2hlm 29971 |
. . . . . . . . . . . 12
โข
โ๐ฃ =
((โ๐กโ(MetOpenโ(IndMetโ๐))) โพ ( โ
โm โ)) |
23 | 22 | breqi 5115 |
. . . . . . . . . . 11
โข (๐น โ๐ฃ
๐ฅ โ ๐น((โ๐กโ(MetOpenโ(IndMetโ๐))) โพ ( โ โm โ))๐ฅ) |
24 | | brres 5948 |
. . . . . . . . . . . 12
โข (๐ฅ โ V โ (๐น((โ๐กโ(MetOpenโ(IndMetโ๐))) โพ ( โ โm โ))๐ฅ โ (๐น โ ( โ โm โ) โง ๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ))) |
25 | 24 | elv 3453 |
. . . . . . . . . . 11
โข (๐น((โ๐กโ(MetOpenโ(IndMetโ๐))) โพ ( โ โm โ))๐ฅ โ (๐น โ ( โ โm โ) โง ๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ)) |
26 | 23, 25 | bitri 275 |
. . . . . . . . . 10
โข (๐น โ๐ฃ
๐ฅ โ (๐น โ ( โ โm
โ) โง ๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ)) |
27 | 26 | baib 537 |
. . . . . . . . 9
โข (๐น โ ( โ
โm โ) โ (๐น โ๐ฃ ๐ฅ โ ๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ)) |
28 | 27 | adantl 483 |
. . . . . . . 8
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ (๐น
โ๐ฃ ๐ฅ โ ๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ)) |
29 | 28 | biimprd 248 |
. . . . . . 7
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ (๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ
โ ๐น โ๐ฃ ๐ฅ)) |
30 | 21, 29 | jcad 514 |
. . . . . 6
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ (๐น(โ๐กโ(MetOpenโ(IndMetโ๐)))๐ฅ
โ (๐ฅ โ โ โง ๐น โ๐ฃ ๐ฅ))) |
31 | 10, 30 | biimtrrid 242 |
. . . . 5
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ (โจ๐น,
๐ฅโฉ โ
(โ๐กโ(MetOpenโ(IndMetโ๐))) โ (๐ฅ โ โ โง ๐น โ๐ฃ ๐ฅ))) |
32 | 31 | eximdv 1921 |
. . . 4
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ (โ๐ฅโจ๐น, ๐ฅโฉ โ
(โ๐กโ(MetOpenโ(IndMetโ๐))) โ โ๐ฅ(๐ฅ โ โ โง ๐น โ๐ฃ ๐ฅ))) |
33 | 9, 32 | mpd 15 |
. . 3
โข ((๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ)) โ โ๐ฅ(๐ฅ โ โ โง ๐น โ๐ฃ ๐ฅ)) |
34 | | elin 3930 |
. . 3
โข (๐น โ
((Cauโ(IndMetโ๐)) โฉ ( โ โm
โ)) โ (๐น โ
(Cauโ(IndMetโ๐)) โง ๐น โ ( โ โm
โ))) |
35 | | df-rex 3071 |
. . 3
โข
(โ๐ฅ โ
โ ๐น
โ๐ฃ ๐ฅ โ โ๐ฅ(๐ฅ โ โ โง ๐น โ๐ฃ ๐ฅ)) |
36 | 33, 34, 35 | 3imtr4i 292 |
. 2
โข (๐น โ
((Cauโ(IndMetโ๐)) โฉ ( โ โm
โ)) โ โ๐ฅ
โ โ ๐น
โ๐ฃ ๐ฅ) |
37 | 13, 11, 15, 3 | h2hcau 29970 |
. 2
โข Cauchy =
((Cauโ(IndMetโ๐)) โฉ ( โ โm
โ)) |
38 | 36, 37 | eleq2s 2852 |
1
โข (๐น โ Cauchy โ
โ๐ฅ โ โ
๐น
โ๐ฃ ๐ฅ) |