Metamath Proof Explorer

Theorem adj1

Description: Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adj1 ⊢T∈dom⁡adjh∧A∈ℋ∧B∈ℋ→A⋅ihT⁡B=adjh⁡T⁡A⋅ihB

Proof

Step Hyp Ref Expression
1 funadj ⊢Fun⁡adjh
2 funfvop ⊢Fun⁡adjh∧T∈dom⁡adjh→Tadjh⁡T∈adjh
3 1 2 mpan ⊢T∈dom⁡adjh→Tadjh⁡T∈adjh
4 dfadj2 ⊢adjh=zw|z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihz⁡y=w⁡x⋅ihy
5 3 4 eleqtrdi ⊢T∈dom⁡adjh→Tadjh⁡T∈zw|z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihz⁡y=w⁡x⋅ihy
6 fvex ⊢adjh⁡T∈V
7 feq1 ⊢z=T→z:ℋ⟶ℋ↔T:ℋ⟶ℋ
8 fveq1 ⊢z=T→z⁡y=T⁡y
9 8 oveq2d ⊢z=T→x⋅ihz⁡y=x⋅ihT⁡y
10 9 eqeq1d ⊢z=T→x⋅ihz⁡y=w⁡x⋅ihy↔x⋅ihT⁡y=w⁡x⋅ihy
11 10 2ralbidv ⊢z=T→∀x∈ℋ∀y∈ℋx⋅ihz⁡y=w⁡x⋅ihy↔∀x∈ℋ∀y∈ℋx⋅ihT⁡y=w⁡x⋅ihy
12 7 11 3anbi13d ⊢z=T→z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihz⁡y=w⁡x⋅ihy↔T:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=w⁡x⋅ihy
13 feq1 ⊢w=adjh⁡T→w:ℋ⟶ℋ↔adjh⁡T:ℋ⟶ℋ
14 fveq1 ⊢w=adjh⁡T→w⁡x=adjh⁡T⁡x
15 14 oveq1d ⊢w=adjh⁡T→w⁡x⋅ihy=adjh⁡T⁡x⋅ihy
16 15 eqeq2d ⊢w=adjh⁡T→x⋅ihT⁡y=w⁡x⋅ihy↔x⋅ihT⁡y=adjh⁡T⁡x⋅ihy
17 16 2ralbidv ⊢w=adjh⁡T→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=w⁡x⋅ihy↔∀x∈ℋ∀y∈ℋx⋅ihT⁡y=adjh⁡T⁡x⋅ihy
18 13 17 3anbi23d ⊢w=adjh⁡T→T:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=w⁡x⋅ihy↔T:ℋ⟶ℋ∧adjh⁡T:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=adjh⁡T⁡x⋅ihy
19 12 18 opelopabg ⊢T∈dom⁡adjh∧adjh⁡T∈V→Tadjh⁡T∈zw|z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihz⁡y=w⁡x⋅ihy↔T:ℋ⟶ℋ∧adjh⁡T:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=adjh⁡T⁡x⋅ihy
20 6 19 mpan2 ⊢T∈dom⁡adjh→Tadjh⁡T∈zw|z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihz⁡y=w⁡x⋅ihy↔T:ℋ⟶ℋ∧adjh⁡T:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=adjh⁡T⁡x⋅ihy
21 5 20 mpbid ⊢T∈dom⁡adjh→T:ℋ⟶ℋ∧adjh⁡T:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=adjh⁡T⁡x⋅ihy
22 21 simp3d ⊢T∈dom⁡adjh→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=adjh⁡T⁡x⋅ihy
23 oveq1 ⊢x=A→x⋅ihT⁡y=A⋅ihT⁡y
24 fveq2 ⊢x=A→adjh⁡T⁡x=adjh⁡T⁡A
25 24 oveq1d ⊢x=A→adjh⁡T⁡x⋅ihy=adjh⁡T⁡A⋅ihy
26 23 25 eqeq12d ⊢x=A→x⋅ihT⁡y=adjh⁡T⁡x⋅ihy↔A⋅ihT⁡y=adjh⁡T⁡A⋅ihy
27 fveq2 ⊢y=B→T⁡y=T⁡B
28 27 oveq2d ⊢y=B→A⋅ihT⁡y=A⋅ihT⁡B
29 oveq2 ⊢y=B→adjh⁡T⁡A⋅ihy=adjh⁡T⁡A⋅ihB
30 28 29 eqeq12d ⊢y=B→A⋅ihT⁡y=adjh⁡T⁡A⋅ihy↔A⋅ihT⁡B=adjh⁡T⁡A⋅ihB
31 26 30 rspc2v ⊢A∈ℋ∧B∈ℋ→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=adjh⁡T⁡x⋅ihy→A⋅ihT⁡B=adjh⁡T⁡A⋅ihB
32 22 31 syl5com ⊢T∈dom⁡adjh→A∈ℋ∧B∈ℋ→A⋅ihT⁡B=adjh⁡T⁡A⋅ihB
33 32 3impib ⊢T∈dom⁡adjh∧A∈ℋ∧B∈ℋ→A⋅ihT⁡B=adjh⁡T⁡A⋅ihB