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$