Metamath Proof Explorer

Theorem adjeq

Description: A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjeq ⊢T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y→adjh⁡T=S

Proof

Step Hyp Ref Expression
1 funadj ⊢Fun⁡adjh
2 df-adjh ⊢adjh=zw|z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋz⁡x⋅ihy=x⋅ihw⁡y
3 2 eleq2i ⊢TS∈adjh↔TS∈zw|z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋz⁡x⋅ihy=x⋅ihw⁡y
4 ax-hilex ⊢ℋ∈V
5 fex ⊢T:ℋ⟶ℋ∧ℋ∈V→T∈V
6 4 5 mpan2 ⊢T:ℋ⟶ℋ→T∈V
7 fex ⊢S:ℋ⟶ℋ∧ℋ∈V→S∈V
8 4 7 mpan2 ⊢S:ℋ⟶ℋ→S∈V
9 feq1 ⊢z=T→z:ℋ⟶ℋ↔T:ℋ⟶ℋ
10 fveq1 ⊢z=T→z⁡x=T⁡x
11 10 oveq1d ⊢z=T→z⁡x⋅ihy=T⁡x⋅ihy
12 11 eqeq1d ⊢z=T→z⁡x⋅ihy=x⋅ihw⁡y↔T⁡x⋅ihy=x⋅ihw⁡y
13 12 2ralbidv ⊢z=T→∀x∈ℋ∀y∈ℋz⁡x⋅ihy=x⋅ihw⁡y↔∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihw⁡y
14 9 13 3anbi13d ⊢z=T→z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋz⁡x⋅ihy=x⋅ihw⁡y↔T:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihw⁡y
15 feq1 ⊢w=S→w:ℋ⟶ℋ↔S:ℋ⟶ℋ
16 fveq1 ⊢w=S→w⁡y=S⁡y
17 16 oveq2d ⊢w=S→x⋅ihw⁡y=x⋅ihS⁡y
18 17 eqeq2d ⊢w=S→T⁡x⋅ihy=x⋅ihw⁡y↔T⁡x⋅ihy=x⋅ihS⁡y
19 18 2ralbidv ⊢w=S→∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihw⁡y↔∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y
20 15 19 3anbi23d ⊢w=S→T:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihw⁡y↔T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y
21 14 20 opelopabg ⊢T∈V∧S∈V→TS∈zw|z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋz⁡x⋅ihy=x⋅ihw⁡y↔T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y
22 6 8 21 syl2an ⊢T:ℋ⟶ℋ∧S:ℋ⟶ℋ→TS∈zw|z:ℋ⟶ℋ∧w:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋz⁡x⋅ihy=x⋅ihw⁡y↔T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y
23 3 22 syl5bb ⊢T:ℋ⟶ℋ∧S:ℋ⟶ℋ→TS∈adjh↔T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y
24 df-3an ⊢T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y↔T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y
25 24 baibr ⊢T:ℋ⟶ℋ∧S:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y↔T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y
26 23 25 bitr4d ⊢T:ℋ⟶ℋ∧S:ℋ⟶ℋ→TS∈adjh↔∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y
27 26 biimp3ar ⊢T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y→TS∈adjh
28 funopfv ⊢Fun⁡adjh→TS∈adjh→adjh⁡T=S
29 1 27 28 mpsyl ⊢T:ℋ⟶ℋ∧S:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihS⁡y→adjh⁡T=S