# Metamath Proof Explorer

## Theorem adjval2

Description: Value of the adjoint function. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjval2 ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)=\left(\iota {u}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 adjval ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)=\left(\iota {u}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
2 dmadjop ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {T}:ℋ⟶ℋ$
3 elmapi ${⊢}{u}\in \left({ℋ}^{ℋ}\right)\to {u}:ℋ⟶ℋ$
4 adjsym ${⊢}\left({T}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
5 eqcom ${⊢}{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)$
6 5 2ralbii ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)$
7 4 6 syl6bb ${⊢}\left({T}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)\right)$
8 2 3 7 syl2an ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {u}\in \left({ℋ}^{ℋ}\right)\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)\right)$
9 8 riotabidva ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \left(\iota {u}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)=\left(\iota {u}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)\right)$
10 1 9 eqtrd ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)=\left(\iota {u}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)\right)$