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 ⁡ adj h ∧ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih T ⁡ B = adj h ⁡ T ⁡ A ⋅ ih B

Proof

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