Theorem adj0

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}}:\mathscr{H}⟶\mathscr{H}$$
2		ho0val	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
3	2	oveq1d	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}y=0_{ℎ}{\cdot }_{\mathrm{ih}}y$$
4		hi01	$$⊢y\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}y=0$$
5	3 4	sylan9eq	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to 0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}y=0$$
6		ho0val	$$⊢y\in \mathscr{H}\to 0_{\mathrm{hop}}\left(y\right)=0_{ℎ}$$
7	6	oveq2d	$$⊢y\in \mathscr{H}\to x{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left(y\right)=x{\cdot }_{\mathrm{ih}}{0}_{ℎ}$$
8		hi02	$$⊢x\in \mathscr{H}\to x{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0$$
9	7 8	sylan9eqr	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left(y\right)=0$$
10	5 9	eqtr4d	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\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 \mathscr{H}\forall y\in \mathscr{H}{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}}:\mathscr{H}⟶\mathscr{H}\wedge 0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}{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}}$$