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