This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem helch

Description: The Hilbert lattice one (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of Kalmbach p. 65. (Contributed by NM, 6-Sep-1999) (New usage is discouraged.)

Ref Expression
Assertion helch 
|- ~H e. CH

Proof

Step Hyp Ref Expression
1 ssid 
 |-  ~H C_ ~H
2 ax-hv0cl 
 |-  0h e. ~H
3 1 2 pm3.2i 
 |-  ( ~H C_ ~H /\ 0h e. ~H )
4 hvaddcl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) e. ~H )
5 4 rgen2 
 |-  A. x e. ~H A. y e. ~H ( x +h y ) e. ~H
6 hvmulcl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H )
7 6 rgen2 
 |-  A. x e. CC A. y e. ~H ( x .h y ) e. ~H
8 5 7 pm3.2i 
 |-  ( A. x e. ~H A. y e. ~H ( x +h y ) e. ~H /\ A. x e. CC A. y e. ~H ( x .h y ) e. ~H )
9 issh2 
 |-  ( ~H e. SH <-> ( ( ~H C_ ~H /\ 0h e. ~H ) /\ ( A. x e. ~H A. y e. ~H ( x +h y ) e. ~H /\ A. x e. CC A. y e. ~H ( x .h y ) e. ~H ) ) )
10 3 8 9 mpbir2an 
 |-  ~H e. SH
11 vex 
 |-  x e. _V
12 11 hlimveci 
 |-  ( f ~~>v x -> x e. ~H )
13 12 adantl 
 |-  ( ( f : NN --> ~H /\ f ~~>v x ) -> x e. ~H )
14 13 gen2 
 |-  A. f A. x ( ( f : NN --> ~H /\ f ~~>v x ) -> x e. ~H )
15 isch2 
 |-  ( ~H e. CH <-> ( ~H e. SH /\ A. f A. x ( ( f : NN --> ~H /\ f ~~>v x ) -> x e. ~H ) ) )
16 10 14 15 mpbir2an 
 |-  ~H e. CH