# Metamath Proof Explorer

Description: Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adj0 ${⊢}{adj}_{h}\left({0}_{\mathrm{hop}}\right)={0}_{\mathrm{hop}}$

### Proof

Step Hyp Ref Expression
1 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
2 ho0val ${⊢}{x}\in ℋ\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
3 2 oveq1d ${⊢}{x}\in ℋ\to {0}_{\mathrm{hop}}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={0}_{ℎ}{\cdot }_{\mathrm{ih}}{y}$
4 hi01 ${⊢}{y}\in ℋ\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{y}=0$
5 3 4 sylan9eq ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {0}_{\mathrm{hop}}\left({x}\right){\cdot }_{\mathrm{ih}}{y}=0$
6 ho0val ${⊢}{y}\in ℋ\to {0}_{\mathrm{hop}}\left({y}\right)={0}_{ℎ}$
7 6 oveq2d ${⊢}{y}\in ℋ\to {x}{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{0}_{ℎ}$
8 hi02 ${⊢}{x}\in ℋ\to {x}{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0$
9 7 8 sylan9eqr ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left({y}\right)=0$
10 5 9 eqtr4d ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {0}_{\mathrm{hop}}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left({y}\right)$
11 10 rgen2 ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{0}_{\mathrm{hop}}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left({y}\right)$
12 adjeq ${⊢}\left({0}_{\mathrm{hop}}:ℋ⟶ℋ\wedge {0}_{\mathrm{hop}}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{0}_{\mathrm{hop}}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left({y}\right)\right)\to {adj}_{h}\left({0}_{\mathrm{hop}}\right)={0}_{\mathrm{hop}}$
13 1 1 11 12 mp3an ${⊢}{adj}_{h}\left({0}_{\mathrm{hop}}\right)={0}_{\mathrm{hop}}$