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 𝑦 ) ) }