Metamath Proof Explorer

Description: The domain of the adjoint function is a subset of the maps from ~H to ~H . (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion dmadjss ${⊢}\mathrm{dom}{adj}_{h}\subseteq {ℋ}^{ℋ}$

Proof

Step Hyp Ref Expression
1 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\}$
2 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)$
3 ax-hilex ${⊢}ℋ\in \mathrm{V}$
4 3 3 elmap ${⊢}{t}\in \left({ℋ}^{ℋ}\right)↔{t}:ℋ⟶ℋ$
5 4 anbi1i ${⊢}\left({t}\in \left({ℋ}^{ℋ}\right)\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)↔\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)$
6 2 5 bitr4i ${⊢}\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}\in \left({ℋ}^{ℋ}\right)\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 6 opabbii ${⊢}\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\}=\left\{⟨{t},{u}⟩|\left({t}\in \left({ℋ}^{ℋ}\right)\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\}$
8 1 7 eqtri ${⊢}{adj}_{h}=\left\{⟨{t},{u}⟩|\left({t}\in \left({ℋ}^{ℋ}\right)\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\}$
9 8 dmeqi ${⊢}\mathrm{dom}{adj}_{h}=\mathrm{dom}\left\{⟨{t},{u}⟩|\left({t}\in \left({ℋ}^{ℋ}\right)\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\}$
10 dmopabss ${⊢}\mathrm{dom}\left\{⟨{t},{u}⟩|\left({t}\in \left({ℋ}^{ℋ}\right)\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\}\subseteq {ℋ}^{ℋ}$
11 9 10 eqsstri ${⊢}\mathrm{dom}{adj}_{h}\subseteq {ℋ}^{ℋ}$