Definition df-sh

Description: Define the set of subspaces of a Hilbert space. See issh for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of Beran p. 95. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	df-sh	|- SH = { h e. ~P ~H | ( 0h e. h /\ ( +h " ( h X. h ) ) C_ h /\ ( .h " ( CC X. h ) ) C_ h ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csh	|- SH
1		vh	|- h
2		chba	|- ~H
3	2	cpw	|- ~P ~H
4		c0v	|- 0h
5	1	cv	|- h
6	4 5	wcel	|- 0h e. h
7		cva	|- +h
8	5 5	cxp	|- ( h X. h )
9	7 8	cima	|- ( +h " ( h X. h ) )
10	9 5	wss	|- ( +h " ( h X. h ) ) C_ h
11		csm	|- .h
12		cc	|- CC
13	12 5	cxp	|- ( CC X. h )
14	11 13	cima	|- ( .h " ( CC X. h ) )
15	14 5	wss	|- ( .h " ( CC X. h ) ) C_ h
16	6 10 15	w3a	|- ( 0h e. h /\ ( +h " ( h X. h ) ) C_ h /\ ( .h " ( CC X. h ) ) C_ h )
17	16 1 3	crab	|- { h e. ~P ~H | ( 0h e. h /\ ( +h " ( h X. h ) ) C_ h /\ ( .h " ( CC X. h ) ) C_ h ) }
18	0 17	wceq	|- SH = { h e. ~P ~H | ( 0h e. h /\ ( +h " ( h X. h ) ) C_ h /\ ( .h " ( CC X. h ) ) C_ h ) }