Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  adj2 Structured version   Visualization version   GIF version

 Description: Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
adj2 ((𝑇 ∈ dom adj𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇𝐴) ·ih 𝐵) = (𝐴 ·ih ((adj𝑇)‘𝐵)))

StepHypRef Expression
1 adj1 29726 . . . 4 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐵 ·ih (𝑇𝐴)) = (((adj𝑇)‘𝐵) ·ih 𝐴))
2 simp2 1134 . . . . 5 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → 𝐵 ∈ ℋ)
3 dmadjop 29681 . . . . . . 7 (𝑇 ∈ dom adj𝑇: ℋ⟶ ℋ)
43ffvelrnda 6829 . . . . . 6 ((𝑇 ∈ dom adj𝐴 ∈ ℋ) → (𝑇𝐴) ∈ ℋ)
543adant2 1128 . . . . 5 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝑇𝐴) ∈ ℋ)
6 ax-his1 28875 . . . . 5 ((𝐵 ∈ ℋ ∧ (𝑇𝐴) ∈ ℋ) → (𝐵 ·ih (𝑇𝐴)) = (∗‘((𝑇𝐴) ·ih 𝐵)))
72, 5, 6syl2anc 587 . . . 4 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐵 ·ih (𝑇𝐴)) = (∗‘((𝑇𝐴) ·ih 𝐵)))
8 adjcl 29725 . . . . . 6 ((𝑇 ∈ dom adj𝐵 ∈ ℋ) → ((adj𝑇)‘𝐵) ∈ ℋ)
983adant3 1129 . . . . 5 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → ((adj𝑇)‘𝐵) ∈ ℋ)
10 simp3 1135 . . . . 5 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → 𝐴 ∈ ℋ)
11 ax-his1 28875 . . . . 5 ((((adj𝑇)‘𝐵) ∈ ℋ ∧ 𝐴 ∈ ℋ) → (((adj𝑇)‘𝐵) ·ih 𝐴) = (∗‘(𝐴 ·ih ((adj𝑇)‘𝐵))))
129, 10, 11syl2anc 587 . . . 4 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (((adj𝑇)‘𝐵) ·ih 𝐴) = (∗‘(𝐴 ·ih ((adj𝑇)‘𝐵))))
131, 7, 123eqtr3d 2841 . . 3 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (∗‘((𝑇𝐴) ·ih 𝐵)) = (∗‘(𝐴 ·ih ((adj𝑇)‘𝐵))))
14 hicl 28873 . . . . 5 (((𝑇𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇𝐴) ·ih 𝐵) ∈ ℂ)
155, 2, 14syl2anc 587 . . . 4 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → ((𝑇𝐴) ·ih 𝐵) ∈ ℂ)
16 hicl 28873 . . . . 5 ((𝐴 ∈ ℋ ∧ ((adj𝑇)‘𝐵) ∈ ℋ) → (𝐴 ·ih ((adj𝑇)‘𝐵)) ∈ ℂ)
1710, 9, 16syl2anc 587 . . . 4 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ·ih ((adj𝑇)‘𝐵)) ∈ ℂ)
18 cj11 14516 . . . 4 ((((𝑇𝐴) ·ih 𝐵) ∈ ℂ ∧ (𝐴 ·ih ((adj𝑇)‘𝐵)) ∈ ℂ) → ((∗‘((𝑇𝐴) ·ih 𝐵)) = (∗‘(𝐴 ·ih ((adj𝑇)‘𝐵))) ↔ ((𝑇𝐴) ·ih 𝐵) = (𝐴 ·ih ((adj𝑇)‘𝐵))))
1915, 17, 18syl2anc 587 . . 3 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → ((∗‘((𝑇𝐴) ·ih 𝐵)) = (∗‘(𝐴 ·ih ((adj𝑇)‘𝐵))) ↔ ((𝑇𝐴) ·ih 𝐵) = (𝐴 ·ih ((adj𝑇)‘𝐵))))
2013, 19mpbid 235 . 2 ((𝑇 ∈ dom adj𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → ((𝑇𝐴) ·ih 𝐵) = (𝐴 ·ih ((adj𝑇)‘𝐵)))
21203com23 1123 1 ((𝑇 ∈ dom adj𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇𝐴) ·ih 𝐵) = (𝐴 ·ih ((adj𝑇)‘𝐵)))