Definition df-sh 28064

Description: Define the set of subspaces of a Hilbert space. See issh 28065 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.)

Assertion

Ref	Expression
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 of Definition df-sh

Step	Hyp	Ref	Expression
1		csh 27785	. 2 class SH
2		c0v 27781	. . . . 5 class 0h
3		vh	. . . . . 6 setvar h
4	3	cv 1482	. . . . 5 class h
5	2, 4	wcel 1990	. . . 4 wff 0h e. h
6		cva 27777	. . . . . 6 class +h
7	4, 4	cxp 5112	. . . . . 6 class ( h X. h )
8	6, 7	cima 5117	. . . . 5 class ( +h " ( h X. h ) )
9	8, 4	wss 3574	. . . 4 wff ( +h " ( h X. h ) ) C_ h
10		csm 27778	. . . . . 6 class .h
11		cc 9934	. . . . . . 7 class CC
12	11, 4	cxp 5112	. . . . . 6 class ( CC X. h )
13	10, 12	cima 5117	. . . . 5 class ( .h " ( CC X. h ) )
14	13, 4	wss 3574	. . . 4 wff ( .h " ( CC X. h ) ) C_ h
15	5, 9, 14	w3a 1037	. . 3 wff ( 0h e. h /\ ( +h " ( h X. h ) ) C_ h /\ ( .h " ( CC X. h ) ) C_ h )
16		chil 27776	. . . 4 class ~H
17	16	cpw 4158	. . 3 class ~P ~H
18	15, 3, 17	crab 2916	. 2 class { h e. ~P ~H | ( 0h e. h /\ ( +h " ( h X. h ) ) C_ h /\ ( .h " ( CC X. h ) ) C_ h ) }
19	1, 18	wceq 1483	1 wff SH = { h e. ~P ~H | ( 0h e. h /\ ( +h " ( h X. h ) ) C_ h /\ ( .h " ( CC X. h ) ) C_ h ) }

This definition is referenced by:  issh  28065