# Metamath Proof Explorer

Description: Value of the adjoint function for T in the domain of adjh . (Contributed by NM, 19-Feb-2006) (Revised by Mario Carneiro, 24-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 dmadjop ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {T}:ℋ⟶ℋ$
2 1 biantrurd ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \left(\left({u}:ℋ⟶ℋ\wedge \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({T}:ℋ⟶ℋ\wedge \left({u}:ℋ⟶ℋ\wedge \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)\right)\right)$
3 ax-hilex ${⊢}ℋ\in \mathrm{V}$
4 3 3 elmap ${⊢}{u}\in \left({ℋ}^{ℋ}\right)↔{u}:ℋ⟶ℋ$
5 4 anbi1i ${⊢}\left({u}\in \left({ℋ}^{ℋ}\right)\wedge \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({u}:ℋ⟶ℋ\wedge \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)$
6 3anass ${⊢}\left({T}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \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({T}:ℋ⟶ℋ\wedge \left({u}:ℋ⟶ℋ\wedge \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)\right)$
7 2 5 6 3bitr4g ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \left(\left({u}\in \left({ℋ}^{ℋ}\right)\wedge \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({T}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \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)\right)$
8 7 iotabidv ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \left(\iota {u}|\left({u}\in \left({ℋ}^{ℋ}\right)\wedge \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)\right)=\left(\iota {u}|\left({T}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \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)\right)$
9 df-riota ${⊢}\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}|\left({u}\in \left({ℋ}^{ℋ}\right)\wedge \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)\right)$
10 9 a1i ${⊢}{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}|\left({u}\in \left({ℋ}^{ℋ}\right)\wedge \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)\right)$
11 dfadj2 ${⊢}{adj}_{h}=\left\{⟨{t},{u}⟩|\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \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)\right\}$
12 feq1 ${⊢}{t}={T}\to \left({t}:ℋ⟶ℋ↔{T}:ℋ⟶ℋ\right)$
13 fveq1 ${⊢}{t}={T}\to {t}\left({y}\right)={T}\left({y}\right)$
14 13 oveq2d ${⊢}{t}={T}\to {x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)$
15 14 eqeq1d ${⊢}{t}={T}\to \left({x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
16 15 2ralbidv ${⊢}{t}={T}\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}}{T}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
17 12 16 3anbi13d ${⊢}{t}={T}\to \left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \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({T}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \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)\right)$
18 11 17 fvopab5 ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)=\left(\iota {u}|\left({T}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \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)\right)$
19 8 10 18 3eqtr4rd ${⊢}{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)$