# Metamath Proof Explorer

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