Metamath Proof Explorer

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

Ref Expression
Assertion adj2 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)$

Proof

Step Hyp Ref Expression
1 adj1 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={adj}_{h}\left({T}\right)\left({B}\right){\cdot }_{\mathrm{ih}}{A}$
2 simp2 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {B}\in ℋ$
3 dmadjop ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {T}:ℋ⟶ℋ$
4 3 ffvelrnda ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\to {T}\left({A}\right)\in ℋ$
5 4 3adant2 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {T}\left({A}\right)\in ℋ$
6 ax-his1 ${⊢}\left({B}\in ℋ\wedge {T}\left({A}\right)\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)=\stackrel{‾}{{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}}$
7 2 5 6 syl2anc ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)=\stackrel{‾}{{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}}$
8 adjcl ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({B}\right)\in ℋ$
9 8 3adant3 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({B}\right)\in ℋ$
10 simp3 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {A}\in ℋ$
11 ax-his1 ${⊢}\left({adj}_{h}\left({T}\right)\left({B}\right)\in ℋ\wedge {A}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({B}\right){\cdot }_{\mathrm{ih}}{A}=\stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)}$
12 9 10 11 syl2anc ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({B}\right){\cdot }_{\mathrm{ih}}{A}=\stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)}$
13 1 7 12 3eqtr3d ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to \stackrel{‾}{{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}}=\stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)}$
14 hicl ${⊢}\left({T}\left({A}\right)\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}\in ℂ$
15 5 2 14 syl2anc ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}\in ℂ$
16 hicl ${⊢}\left({A}\in ℋ\wedge {adj}_{h}\left({T}\right)\left({B}\right)\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)\in ℂ$
17 10 9 16 syl2anc ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)\in ℂ$
18 cj11 ${⊢}\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}\in ℂ\wedge {A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)\in ℂ\right)\to \left(\stackrel{‾}{{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}}=\stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)}↔{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)\right)$
19 15 17 18 syl2anc ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to \left(\stackrel{‾}{{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}}=\stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)}↔{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)\right)$
20 13 19 mpbid ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {B}\in ℋ\wedge {A}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)$
21 20 3com23 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({B}\right)$