Metamath Proof Explorer


Theorem helch

Description: The unit Hilbert lattice element (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