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