Metamath Proof Explorer


Theorem hsn0elch

Description: The zero subspace belongs to the set of closed subspaces of Hilbert space. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hsn0elch
|- { 0h } e. CH

Proof

Step Hyp Ref Expression
1 ax-hv0cl
 |-  0h e. ~H
2 snssi
 |-  ( 0h e. ~H -> { 0h } C_ ~H )
3 1 2 ax-mp
 |-  { 0h } C_ ~H
4 1 elexi
 |-  0h e. _V
5 4 snid
 |-  0h e. { 0h }
6 3 5 pm3.2i
 |-  ( { 0h } C_ ~H /\ 0h e. { 0h } )
7 velsn
 |-  ( x e. { 0h } <-> x = 0h )
8 velsn
 |-  ( y e. { 0h } <-> y = 0h )
9 oveq12
 |-  ( ( x = 0h /\ y = 0h ) -> ( x +h y ) = ( 0h +h 0h ) )
10 1 hvaddid2i
 |-  ( 0h +h 0h ) = 0h
11 9 10 eqtrdi
 |-  ( ( x = 0h /\ y = 0h ) -> ( x +h y ) = 0h )
12 ovex
 |-  ( x +h y ) e. _V
13 12 elsn
 |-  ( ( x +h y ) e. { 0h } <-> ( x +h y ) = 0h )
14 11 13 sylibr
 |-  ( ( x = 0h /\ y = 0h ) -> ( x +h y ) e. { 0h } )
15 7 8 14 syl2anb
 |-  ( ( x e. { 0h } /\ y e. { 0h } ) -> ( x +h y ) e. { 0h } )
16 15 rgen2
 |-  A. x e. { 0h } A. y e. { 0h } ( x +h y ) e. { 0h }
17 oveq2
 |-  ( y = 0h -> ( x .h y ) = ( x .h 0h ) )
18 hvmul0
 |-  ( x e. CC -> ( x .h 0h ) = 0h )
19 17 18 sylan9eqr
 |-  ( ( x e. CC /\ y = 0h ) -> ( x .h y ) = 0h )
20 ovex
 |-  ( x .h y ) e. _V
21 20 elsn
 |-  ( ( x .h y ) e. { 0h } <-> ( x .h y ) = 0h )
22 19 21 sylibr
 |-  ( ( x e. CC /\ y = 0h ) -> ( x .h y ) e. { 0h } )
23 8 22 sylan2b
 |-  ( ( x e. CC /\ y e. { 0h } ) -> ( x .h y ) e. { 0h } )
24 23 rgen2
 |-  A. x e. CC A. y e. { 0h } ( x .h y ) e. { 0h }
25 16 24 pm3.2i
 |-  ( A. x e. { 0h } A. y e. { 0h } ( x +h y ) e. { 0h } /\ A. x e. CC A. y e. { 0h } ( x .h y ) e. { 0h } )
26 issh2
 |-  ( { 0h } e. SH <-> ( ( { 0h } C_ ~H /\ 0h e. { 0h } ) /\ ( A. x e. { 0h } A. y e. { 0h } ( x +h y ) e. { 0h } /\ A. x e. CC A. y e. { 0h } ( x .h y ) e. { 0h } ) ) )
27 6 25 26 mpbir2an
 |-  { 0h } e. SH
28 4 fconst2
 |-  ( f : NN --> { 0h } <-> f = ( NN X. { 0h } ) )
29 hlim0
 |-  ( NN X. { 0h } ) ~~>v 0h
30 breq1
 |-  ( f = ( NN X. { 0h } ) -> ( f ~~>v 0h <-> ( NN X. { 0h } ) ~~>v 0h ) )
31 29 30 mpbiri
 |-  ( f = ( NN X. { 0h } ) -> f ~~>v 0h )
32 28 31 sylbi
 |-  ( f : NN --> { 0h } -> f ~~>v 0h )
33 hlimuni
 |-  ( ( f ~~>v 0h /\ f ~~>v x ) -> 0h = x )
34 33 eleq1d
 |-  ( ( f ~~>v 0h /\ f ~~>v x ) -> ( 0h e. { 0h } <-> x e. { 0h } ) )
35 32 34 sylan
 |-  ( ( f : NN --> { 0h } /\ f ~~>v x ) -> ( 0h e. { 0h } <-> x e. { 0h } ) )
36 5 35 mpbii
 |-  ( ( f : NN --> { 0h } /\ f ~~>v x ) -> x e. { 0h } )
37 36 gen2
 |-  A. f A. x ( ( f : NN --> { 0h } /\ f ~~>v x ) -> x e. { 0h } )
38 isch2
 |-  ( { 0h } e. CH <-> ( { 0h } e. SH /\ A. f A. x ( ( f : NN --> { 0h } /\ f ~~>v x ) -> x e. { 0h } ) ) )
39 27 37 38 mpbir2an
 |-  { 0h } e. CH