Theorem hhlnoi

Description: The linear operators of Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhlno.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	hhlno.2	$$⊢L=U\mathrm{LnOp}U$$
Assertion	hhlnoi	$$⊢\mathrm{LinOp}=L$$

Proof

Step	Hyp	Ref	Expression
1		hhlno.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		hhlno.2	$$⊢L=U\mathrm{LnOp}U$$
3		df-lnop	$$⊢\mathrm{LinOp}=\left\{t\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\forall x\in ℂ\forall y\in \mathscr{H}\forall z\in \mathscr{H}t\left(\left(x{\cdot }_{ℎ}y\right){+}_{ℎ}z\right)=\left(x{\cdot }_{ℎ}t\left(y\right)\right){+}_{ℎ}t\left(z\right)\right\}$$
4	1	hhnv	$$⊢U\in \mathrm{NrmCVec}$$
5	1	hhba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
6	1	hhva	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
7	1	hhsm	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
8	5 5 6 6 7 7 2	lnoval	$$⊢\left(U\in \mathrm{NrmCVec}\wedge U\in \mathrm{NrmCVec}\right)\to L=\left\{t\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\forall x\in ℂ\forall y\in \mathscr{H}\forall z\in \mathscr{H}t\left(\left(x{\cdot }_{ℎ}y\right){+}_{ℎ}z\right)=\left(x{\cdot }_{ℎ}t\left(y\right)\right){+}_{ℎ}t\left(z\right)\right\}$$
9	4 4 8	mp2an	$$⊢L=\left\{t\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\forall x\in ℂ\forall y\in \mathscr{H}\forall z\in \mathscr{H}t\left(\left(x{\cdot }_{ℎ}y\right){+}_{ℎ}z\right)=\left(x{\cdot }_{ℎ}t\left(y\right)\right){+}_{ℎ}t\left(z\right)\right\}$$
10	3 9	eqtr4i	$$⊢\mathrm{LinOp}=L$$