Theorem 0hmop

Description: The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	0hmop	$$⊢0_{\mathrm{hop}}\in \mathrm{HrmOp}$$

Proof

Step	Hyp	Ref	Expression
1		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
2		ho0val	$$⊢y\in \mathscr{H}\to 0_{\mathrm{hop}}\left(y\right)=0_{ℎ}$$
3	2	oveq2d	$$⊢y\in \mathscr{H}\to x{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left(y\right)=x{\cdot }_{\mathrm{ih}}{0}_{ℎ}$$
4		hi02	$$⊢x\in \mathscr{H}\to x{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0$$
5	3 4	sylan9eqr	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left(y\right)=0$$
6		ho0val	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
7	6	oveq1d	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}y=0_{ℎ}{\cdot }_{\mathrm{ih}}y$$
8		hi01	$$⊢y\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}y=0$$
9	7 8	sylan9eq	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to 0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}y=0$$
10	5 9	eqtr4d	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left(y\right)=0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}y$$
11	10	rgen2	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left(y\right)=0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}y$$
12		elhmop	$$⊢0_{\mathrm{hop}}\in \mathrm{HrmOp}\leftrightarrow \left(0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}{0}_{\mathrm{hop}}\left(y\right)=0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
13	1 11 12	mpbir2an	$$⊢0_{\mathrm{hop}}\in \mathrm{HrmOp}$$