Theorem elunop

Description: Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	elunop	⊢ ( 𝑇 ∈ UniOp ↔ ( 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑇 ∈ UniOp → 𝑇 ∈ V )
2		fof	⊢ ( 𝑇 : ℋ –onto→ ℋ → 𝑇 : ℋ ⟶ ℋ )
3		ax-hilex	⊢ ℋ ∈ V
4		fex	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ℋ ∈ V ) → 𝑇 ∈ V )
5	2 3 4	sylancl	⊢ ( 𝑇 : ℋ –onto→ ℋ → 𝑇 ∈ V )
6	5	adantr	⊢ ( ( 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) → 𝑇 ∈ V )
7		foeq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 : ℋ –onto→ ℋ ↔ 𝑇 : ℋ –onto→ ℋ ) )
8		fveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
9		fveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) )
10	8 9	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
11	10	eqeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) )
12	11	2ralbidv	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) )
13	7 12	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) ↔ ( 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) ) )
14		df-unop	⊢ UniOp = { 𝑡 ∣ ( 𝑡 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑡 ‘ 𝑥 ) ·ih ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) }
15	13 14	elab2g	⊢ ( 𝑇 ∈ V → ( 𝑇 ∈ UniOp ↔ ( 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) ) )
16	1 6 15	pm5.21nii	⊢ ( 𝑇 ∈ UniOp ↔ ( 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) )