Definition df-unop

Description: Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-unop	$$⊢\mathrm{UniOp}=\left\{t|\left(t:\mathscr{H}\underset{onto}{⟶}\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}t\left(x\right){\cdot }_{\mathrm{ih}}t\left(y\right)=x{\cdot }_{\mathrm{ih}}y\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuo	$$class\mathrm{UniOp}$$
1		vt	$$setvart$$
2	1	cv	$$setvart$$
3		chba	$$class\mathscr{H}$$
4	3 3 2	wfo	$$wfft:\mathscr{H}\underset{onto}{⟶}\mathscr{H}$$
5		vx	$$setvarx$$
6		vy	$$setvary$$
7	5	cv	$$setvarx$$
8	7 2	cfv	$$classt\left(x\right)$$
9		csp	$$class{\cdot }_{\mathrm{ih}}$$
10	6	cv	$$setvary$$
11	10 2	cfv	$$classt\left(y\right)$$
12	8 11 9	co	$$class\left(t\left(x\right){\cdot }_{\mathrm{ih}}t\left(y\right)\right)$$
13	7 10 9	co	$$class\left(x{\cdot }_{\mathrm{ih}}y\right)$$
14	12 13	wceq	$$wfft\left(x\right){\cdot }_{\mathrm{ih}}t\left(y\right)=x{\cdot }_{\mathrm{ih}}y$$
15	14 6 3	wral	$$wff\forall y\in \mathscr{H}t\left(x\right){\cdot }_{\mathrm{ih}}t\left(y\right)=x{\cdot }_{\mathrm{ih}}y$$
16	15 5 3	wral	$$wff\forall x\in \mathscr{H}\forall y\in \mathscr{H}t\left(x\right){\cdot }_{\mathrm{ih}}t\left(y\right)=x{\cdot }_{\mathrm{ih}}y$$
17	4 16	wa	$$wff\left(t:\mathscr{H}\underset{onto}{⟶}\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}t\left(x\right){\cdot }_{\mathrm{ih}}t\left(y\right)=x{\cdot }_{\mathrm{ih}}y\right)$$
18	17 1	cab	$$class\left\{t|\left(t:\mathscr{H}\underset{onto}{⟶}\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}t\left(x\right){\cdot }_{\mathrm{ih}}t\left(y\right)=x{\cdot }_{\mathrm{ih}}y\right)\right\}$$
19	0 18	wceq	$$wff\mathrm{UniOp}=\left\{t|\left(t:\mathscr{H}\underset{onto}{⟶}\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}t\left(x\right){\cdot }_{\mathrm{ih}}t\left(y\right)=x{\cdot }_{\mathrm{ih}}y\right)\right\}$$