Metamath Proof Explorer

Theorem adj2

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

Ref Expression
Assertion adj2 ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih B = A ⋅ ih adj h ⁡ T ⁡ B

Proof

Step Hyp Ref Expression
1 adj1 ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih T ⁡ A = adj h ⁡ T ⁡ B ⋅ ih A
2 simp2 ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → B ∈ ℋ
3 dmadjop ⊢ T ∈ dom ⁡ adj h → T : ℋ ⟶ ℋ
4 3 ffvelcdmda ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ → T ⁡ A ∈ ℋ
5 4 3adant2 ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → T ⁡ A ∈ ℋ
6 ax-his1 ⊢ B ∈ ℋ ∧ T ⁡ A ∈ ℋ → B ⋅ ih T ⁡ A = T ⁡ A ⋅ ih B ‾
7 2 5 6 syl2anc ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih T ⁡ A = T ⁡ A ⋅ ih B ‾
8 adjcl ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ → adj h ⁡ T ⁡ B ∈ ℋ
9 8 3adant3 ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → adj h ⁡ T ⁡ B ∈ ℋ
10 simp3 ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → A ∈ ℋ
11 ax-his1 ⊢ adj h ⁡ T ⁡ B ∈ ℋ ∧ A ∈ ℋ → adj h ⁡ T ⁡ B ⋅ ih A = A ⋅ ih adj h ⁡ T ⁡ B ‾
12 9 10 11 syl2anc ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → adj h ⁡ T ⁡ B ⋅ ih A = A ⋅ ih adj h ⁡ T ⁡ B ‾
13 1 7 12 3eqtr3d ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → T ⁡ A ⋅ ih B ‾ = A ⋅ ih adj h ⁡ T ⁡ B ‾
14 hicl ⊢ T ⁡ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih B ∈ ℂ
15 5 2 14 syl2anc ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → T ⁡ A ⋅ ih B ∈ ℂ
16 hicl ⊢ A ∈ ℋ ∧ adj h ⁡ T ⁡ B ∈ ℋ → A ⋅ ih adj h ⁡ T ⁡ B ∈ ℂ
17 10 9 16 syl2anc ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → A ⋅ ih adj h ⁡ T ⁡ B ∈ ℂ
18 cj11 ⊢ T ⁡ A ⋅ ih B ∈ ℂ ∧ A ⋅ ih adj h ⁡ T ⁡ B ∈ ℂ → T ⁡ A ⋅ ih B ‾ = A ⋅ ih adj h ⁡ T ⁡ B ‾ ↔ T ⁡ A ⋅ ih B = A ⋅ ih adj h ⁡ T ⁡ B
19 15 17 18 syl2anc ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → T ⁡ A ⋅ ih B ‾ = A ⋅ ih adj h ⁡ T ⁡ B ‾ ↔ T ⁡ A ⋅ ih B = A ⋅ ih adj h ⁡ T ⁡ B
20 13 19 mpbid ⊢ T ∈ dom ⁡ adj h ∧ B ∈ ℋ ∧ A ∈ ℋ → T ⁡ A ⋅ ih B = A ⋅ ih adj h ⁡ T ⁡ B
21 20 3com23 ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih B = A ⋅ ih adj h ⁡ T ⁡ B