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