# Metamath Proof Explorer

Description: The adjoint of the scalar product of an operator. Theorem 3.11(ii) of Beran p. 106. (Contributed by NM, 21-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjmul ${⊢}\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to {adj}_{h}\left({A}{·}_{\mathrm{op}}{T}\right)=\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 dmadjop ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {T}:ℋ⟶ℋ$
2 homulcl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
3 1 2 sylan2 ${⊢}\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
4 cjcl ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}\in ℂ$
5 dmadjrn ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}$
6 dmadjop ${⊢}{adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right):ℋ⟶ℋ$
7 5 6 syl ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right):ℋ⟶ℋ$
8 homulcl ${⊢}\left(\stackrel{‾}{{A}}\in ℂ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\right)\to \left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right):ℋ⟶ℋ$
9 4 7 8 syl2an ${⊢}\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to \left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right):ℋ⟶ℋ$
10 adj2 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)$
11 10 3expb ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)$
12 11 adantll ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)$
13 12 oveq2d ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)={A}\left({x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)\right)$
14 1 ffvelrnda ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
15 ax-his3 ${⊢}\left({A}\in ℂ\wedge {T}\left({x}\right)\in ℋ\wedge {y}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
16 14 15 syl3an2 ${⊢}\left({A}\in ℂ\wedge \left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\right)\wedge {y}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
17 16 3exp ${⊢}{A}\in ℂ\to \left(\left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\right)\to \left({y}\in ℋ\to \left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right)\right)$
18 17 expd ${⊢}{A}\in ℂ\to \left({T}\in \mathrm{dom}{adj}_{h}\to \left({x}\in ℋ\to \left({y}\in ℋ\to \left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right)\right)\right)$
19 18 imp43 ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
20 simpll ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {A}\in ℂ$
21 simprl ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}\in ℋ$
22 adjcl ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {y}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({y}\right)\in ℋ$
23 22 ad2ant2l ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {adj}_{h}\left({T}\right)\left({y}\right)\in ℋ$
24 his52 ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\wedge {adj}_{h}\left({T}\right)\left({y}\right)\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)\right)={A}\left({x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)\right)$
25 20 21 23 24 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)\right)={A}\left({x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)\right)$
26 13 19 25 3eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)\right)$
27 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
28 1 27 syl3an2 ${⊢}\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
29 28 3expa ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
30 29 adantrr ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
31 30 oveq1d ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}=\left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}$
32 id ${⊢}{y}\in ℋ\to {y}\in ℋ$
33 homval ${⊢}\left(\stackrel{‾}{{A}}\in ℂ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\wedge {y}\in ℋ\right)\to \left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)=\stackrel{‾}{{A}}{\cdot }_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)$
34 4 7 32 33 syl3an ${⊢}\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\wedge {y}\in ℋ\right)\to \left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)=\stackrel{‾}{{A}}{\cdot }_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)$
35 34 3expa ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge {y}\in ℋ\right)\to \left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)=\stackrel{‾}{{A}}{\cdot }_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)$
36 35 adantrl ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)=\stackrel{‾}{{A}}{\cdot }_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)$
37 36 oveq2d ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)\right)$
38 26 31 37 3eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)$
39 38 ralrimivva ${⊢}\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)$
40 adjeq ${⊢}\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right):ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)\right)\to {adj}_{h}\left({A}{·}_{\mathrm{op}}{T}\right)=\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)$
41 3 9 39 40 syl3anc ${⊢}\left({A}\in ℂ\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to {adj}_{h}\left({A}{·}_{\mathrm{op}}{T}\right)=\stackrel{‾}{{A}}{·}_{\mathrm{op}}{adj}_{h}\left({T}\right)$