Metamath Proof Explorer


Theorem axhcompl-zf

Description: Derive Axiom ax-hcompl from Hilbert space under ZF set theory. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022) (New usage is discouraged.)

Ref Expression
Hypotheses axhil.1 U = + norm
axhil.2 U CHil OLD
Assertion axhcompl-zf F Cauchy x F v x

Proof

Step Hyp Ref Expression
1 axhil.1 U = + norm
2 axhil.2 U CHil OLD
3 simpl F Cau IndMet U F F Cau IndMet U
4 eqid IndMet U = IndMet U
5 eqid MetOpen IndMet U = MetOpen IndMet U
6 4 5 hlcompl U CHil OLD F Cau IndMet U F dom t MetOpen IndMet U
7 2 3 6 sylancr F Cau IndMet U F F dom t MetOpen IndMet U
8 eldm2g F Cau IndMet U F dom t MetOpen IndMet U x F x t MetOpen IndMet U
9 8 adantr F Cau IndMet U F F dom t MetOpen IndMet U x F x t MetOpen IndMet U
10 7 9 mpbid F Cau IndMet U F x F x t MetOpen IndMet U
11 df-br F t MetOpen IndMet U x F x t MetOpen IndMet U
12 2 hlnvi U NrmCVec
13 df-hba = BaseSet + norm
14 1 fveq2i BaseSet U = BaseSet + norm
15 13 14 eqtr4i = BaseSet U
16 15 4 imsxmet U NrmCVec IndMet U ∞Met
17 5 mopntopon IndMet U ∞Met MetOpen IndMet U TopOn
18 12 16 17 mp2b MetOpen IndMet U TopOn
19 lmcl MetOpen IndMet U TopOn F t MetOpen IndMet U x x
20 18 19 mpan F t MetOpen IndMet U x x
21 20 a1i F Cau IndMet U F F t MetOpen IndMet U x x
22 1 12 15 4 5 h2hlm v = t MetOpen IndMet U
23 22 breqi F v x F t MetOpen IndMet U x
24 brres x V F t MetOpen IndMet U x F F t MetOpen IndMet U x
25 24 elv F t MetOpen IndMet U x F F t MetOpen IndMet U x
26 23 25 bitri F v x F F t MetOpen IndMet U x
27 26 baib F F v x F t MetOpen IndMet U x
28 27 adantl F Cau IndMet U F F v x F t MetOpen IndMet U x
29 28 biimprd F Cau IndMet U F F t MetOpen IndMet U x F v x
30 21 29 jcad F Cau IndMet U F F t MetOpen IndMet U x x F v x
31 11 30 syl5bir F Cau IndMet U F F x t MetOpen IndMet U x F v x
32 31 eximdv F Cau IndMet U F x F x t MetOpen IndMet U x x F v x
33 10 32 mpd F Cau IndMet U F x x F v x
34 elin F Cau IndMet U F Cau IndMet U F
35 df-rex x F v x x x F v x
36 33 34 35 3imtr4i F Cau IndMet U x F v x
37 1 12 15 4 h2hcau Cauchy = Cau IndMet U
38 36 37 eleq2s F Cauchy x F v x