Definition df-unop 29878

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

Assertion

Ref	Expression
df-unop	⊢ UniOp = {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦))}

Distinct variable group:   𝑥,𝑡,𝑦

Detailed syntax breakdown of Definition df-unop

Step	Hyp	Ref	Expression
1		cuo 28984	. 2 class UniOp
2		chba 28954	. . . . 5 class ℋ
3		vt	. . . . . 6 setvar 𝑡
4	3	cv 1542	. . . . 5 class 𝑡
5	2, 2, 4	wfo 6356	. . . 4 wff 𝑡: ℋ–onto→ ℋ
6		vx	. . . . . . . . . 10 setvar 𝑥
7	6	cv 1542	. . . . . . . . 9 class 𝑥
8	7, 4	cfv 6358	. . . . . . . 8 class (𝑡‘𝑥)
9		vy	. . . . . . . . . 10 setvar 𝑦
10	9	cv 1542	. . . . . . . . 9 class 𝑦
11	10, 4	cfv 6358	. . . . . . . 8 class (𝑡‘𝑦)
12		csp 28957	. . . . . . . 8 class ·ih
13	8, 11, 12	co 7191	. . . . . . 7 class ((𝑡‘𝑥) ·ih (𝑡‘𝑦))
14	7, 10, 12	co 7191	. . . . . . 7 class (𝑥 ·ih 𝑦)
15	13, 14	wceq 1543	. . . . . 6 wff ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦)
16	15, 9, 2	wral 3051	. . . . 5 wff ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦)
17	16, 6, 2	wral 3051	. . . 4 wff ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦)
18	5, 17	wa 399	. . 3 wff (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦))
19	18, 3	cab 2714	. 2 class {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦))}
20	1, 19	wceq 1543	1 wff UniOp = {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦))}

This definition is referenced by:  elunop  29907