Definition df-oc 9400

Description: Define orthogonal complement of a subset (usually a subspace) of Hilbert space. The orthogonal complement is the set of all vectors orthogonal to all vectors in the subset. See ocval 9429 and chocvali 9447 for its value. Textbooks usually denote this unary operation with the symbol _|_ as a small superscript, although Mittelstaedt uses the symbol as a prefix operation. Here we define a function (prefix operation) _|_ rather than introducing a new syntactical form. This lets us take advantage of the theorems about functions that we already have proved under set theory. Definition of [Mittelstaedt] p. 9.

Assertion

Ref	Expression
df-oc	|- _|_ = {<.x, y>. | (x (_ H~ /\ y = {z e. H~ | A.w e. x (z .ih w) = 0})}

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Definition df-oc

Step	Hyp	Ref	Expression
1		cort 9074	. 2 class _|_
2		vx	. . . . . 6 set x
3	2	cv 991	. . . . 5 class x
4		chil 9063	. . . . 5 class H~
5	3, 4	wss 2099	. . . 4 wff x (_ H~
6		vy	. . . . . 6 set y
7	6	cv 991	. . . . 5 class y
8		vz	. . . . . . . . . 10 set z
9	8	cv 991	. . . . . . . . 9 class z
10		vw	. . . . . . . . . 10 set w
11	10	cv 991	. . . . . . . . 9 class w
12		csp 9068	. . . . . . . . 9 class .ih
13	9, 11, 12	co 4021	. . . . . . . 8 class (z .ih w)
14		cc0 5388	. . . . . . . 8 class 0
15	13, 14	wceq 992	. . . . . . 7 wff (z .ih w) = 0
16	15, 10, 3	wral 1691	. . . . . 6 wff A.w e. x (z .ih w) = 0
17	16, 8, 4	crab 1694	. . . . 5 class {z e. H~ | A.w e. x (z .ih w) = 0}
18	7, 17	wceq 992	. . . 4 wff y = {z e. H~ | A.w e. x (z .ih w) = 0}
19	5, 18	wa 221	. . 3 wff (x (_ H~ /\ y = {z e. H~ | A.w e. x (z .ih w) = 0})
20	19, 2, 6	copab 2740	. 2 class {<.x, y>. | (x (_ H~ /\ y = {z e. H~ | A.w e. x (z .ih w) = 0})}
21	1, 20	wceq 992	1 wff _|_ = {<.x, y>. | (x (_ H~ /\ y = {z e. H~ | A.w e. x (z .ih w) = 0})}

This definition is referenced by:  ocval 9429

Copyright terms: Public domain