This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { 𝑡 ∣ ( 𝑡 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuo ⊢ UniOp
1 vt ⊢ 𝑡
2 1 cv ⊢ 𝑡
3 chba ⊢ ℋ
4 3 3 2 wfo ⊢ 𝑡 : ℋ –onto→ ℋ
5 vx ⊢ 𝑥
6 vy ⊢ 𝑦
7 5 cv ⊢ 𝑥
8 7 2 cfv ⊢ ( 𝑡 ‘ 𝑥 )
9 csp ⊢ ·ih
10 6 cv ⊢ 𝑦
11 10 2 cfv ⊢ ( 𝑡 ‘ 𝑦 )
12 8 11 9 co ⊢ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) )
13 7 10 9 co ⊢ ( 𝑥 ·ih 𝑦 )
14 12 13 wceq ⊢ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 )
15 14 6 3 wral ⊢ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 )
16 15 5 3 wral ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 )
17 4 16 wa ⊢ ( 𝑡 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
18 17 1 cab ⊢ { 𝑡 ∣ ( 𝑡 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) }
19 0 18 wceq ⊢ UniOp = { 𝑡 ∣ ( 𝑡 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) }