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

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