HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-unop Structured version   Visualization version   GIF version

Definition df-unop 29395
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
StepHypRef Expression
1 cuo 28499 . 2 class UniOp
2 chba 28469 . . . . 5 class
3 vt . . . . . 6 setvar 𝑡
43cv 1506 . . . . 5 class 𝑡
52, 2, 4wfo 6180 . . . 4 wff 𝑡: ℋ–onto→ ℋ
6 vx . . . . . . . . . 10 setvar 𝑥
76cv 1506 . . . . . . . . 9 class 𝑥
87, 4cfv 6182 . . . . . . . 8 class (𝑡𝑥)
9 vy . . . . . . . . . 10 setvar 𝑦
109cv 1506 . . . . . . . . 9 class 𝑦
1110, 4cfv 6182 . . . . . . . 8 class (𝑡𝑦)
12 csp 28472 . . . . . . . 8 class ·ih
138, 11, 12co 6970 . . . . . . 7 class ((𝑡𝑥) ·ih (𝑡𝑦))
147, 10, 12co 6970 . . . . . . 7 class (𝑥 ·ih 𝑦)
1513, 14wceq 1507 . . . . . 6 wff ((𝑡𝑥) ·ih (𝑡𝑦)) = (𝑥 ·ih 𝑦)
1615, 9, 2wral 3082 . . . . 5 wff 𝑦 ∈ ℋ ((𝑡𝑥) ·ih (𝑡𝑦)) = (𝑥 ·ih 𝑦)
1716, 6, 2wral 3082 . . . 4 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih (𝑡𝑦)) = (𝑥 ·ih 𝑦)
185, 17wa 387 . . 3 wff (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih (𝑡𝑦)) = (𝑥 ·ih 𝑦))
1918, 3cab 2752 . 2 class {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih (𝑡𝑦)) = (𝑥 ·ih 𝑦))}
201, 19wceq 1507 1 wff UniOp = {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih (𝑡𝑦)) = (𝑥 ·ih 𝑦))}
Colors of variables: wff setvar class
This definition is referenced by:  elunop  29424
  Copyright terms: Public domain W3C validator