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⋅ihT⁡y=x⋅ihy

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⋅ihT⁡y=x⋅ihy→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⋅iht⁡y=T⁡x⋅ihT⁡y
11 10 eqeq1d ⊢t=T→t⁡x⋅iht⁡y=x⋅ihy↔T⁡x⋅ihT⁡y=x⋅ihy
12 11 2ralbidv ⊢t=T→∀x∈ℋ∀y∈ℋt⁡x⋅iht⁡y=x⋅ihy↔∀x∈ℋ∀y∈ℋT⁡x⋅ihT⁡y=x⋅ihy
13 7 12 anbi12d ⊢t=T→t:ℋ⟶ontoℋ∧∀x∈ℋ∀y∈ℋt⁡x⋅iht⁡y=x⋅ihy↔T:ℋ⟶ontoℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihT⁡y=x⋅ihy
14 df-unop ⊢UniOp=t|t:ℋ⟶ontoℋ∧∀x∈ℋ∀y∈ℋt⁡x⋅iht⁡y=x⋅ihy
15 13 14 elab2g ⊢T∈V→T∈UniOp↔T:ℋ⟶ontoℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihT⁡y=x⋅ihy
16 1 6 15 pm5.21nii ⊢T∈UniOp↔T:ℋ⟶ontoℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihT⁡y=x⋅ihy