Metamath Proof Explorer

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 ⊢ UniOp = t | t : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuo class UniOp
1 vt setvar t
2 1 cv setvar t
3 chba class ℋ
4 3 3 2 wfo wff t : ℋ ⟶ onto ℋ
5 vx setvar x
6 vy setvar y
7 5 cv setvar x
8 7 2 cfv class t ⁡ x
9 csp class ⋅ ih
10 6 cv setvar y
11 10 2 cfv class t ⁡ y
12 8 11 9 co class t ⁡ x ⋅ ih t ⁡ y
13 7 10 9 co class x ⋅ ih y
14 12 13 wceq wff t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y
15 14 6 3 wral wff ∀ y ∈ ℋ t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y
16 15 5 3 wral wff ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y
17 4 16 wa wff t : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y
18 17 1 cab class t | t : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y
19 0 18 wceq wff UniOp = t | t : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y