# 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 $⊢ T ∈ UniOp ↔ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y$

### Proof

Step Hyp Ref Expression
1 elex $⊢ T ∈ UniOp → T ∈ V$
2 fof $⊢ T : ℋ ⟶ onto ℋ → T : ℋ ⟶ ℋ$
3 ax-hilex $⊢ ℋ ∈ V$
4 fex $⊢ T : ℋ ⟶ ℋ ∧ ℋ ∈ V → T ∈ V$
5 2 3 4 sylancl $⊢ T : ℋ ⟶ onto ℋ → T ∈ V$
6 5 adantr $⊢ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y → T ∈ V$
7 foeq1 $⊢ t = T → t : ℋ ⟶ onto ℋ ↔ T : ℋ ⟶ onto ℋ$
8 fveq1 $⊢ t = T → t ⁡ x = T ⁡ x$
9 fveq1 $⊢ t = T → t ⁡ y = T ⁡ y$
10 8 9 oveq12d $⊢ t = T → t ⁡ x ⋅ ih t ⁡ y = T ⁡ x ⋅ ih T ⁡ y$
11 10 eqeq1d $⊢ t = T → t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y ↔ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y$
12 11 2ralbidv $⊢ t = T → ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y$
13 7 12 anbi12d $⊢ t = T → t : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y ↔ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y$
14 df-unop $⊢ UniOp = t | t : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih t ⁡ y = x ⋅ ih y$
15 13 14 elab2g $⊢ T ∈ V → T ∈ UniOp ↔ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y$
16 1 6 15 pm5.21nii $⊢ T ∈ UniOp ↔ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y$