Theorem htth

Description: Hellinger-Toeplitz Theorem: any self-adjoint linear operator defined on all of Hilbert space is bounded. Theorem 10.1-1 of Kreyszig p. 525. Discovered by E. Hellinger and O. Toeplitz in 1910, "it aroused both admiration and puzzlement since the theorem establishes a relation between properties of two different kinds, namely, the properties of being defined everywhere and being bounded." (Contributed by NM, 11-Jan-2008) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	htth.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	htth.2	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
	htth.3	$$⊢L=U\mathrm{LnOp}U$$
	htth.4	$$⊢B=U\mathrm{BLnOp}U$$
Assertion	htth	$$⊢\left(U\in {CHil}_{\mathrm{OLD}}\wedge T\in L\wedge \forall x\in X\forall y\in XxPT\left(y\right)=T\left(x\right)Py\right)\to T\in B$$

Proof

Step	Hyp	Ref	Expression
1		htth.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		htth.2	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
3		htth.3	$$⊢L=U\mathrm{LnOp}U$$
4		htth.4	$$⊢B=U\mathrm{BLnOp}U$$
5		oveq12	$$⊢\left(U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\wedge U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\to U\mathrm{LnOp}U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
6	5	anidms	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to U\mathrm{LnOp}U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
7	3 6	eqtrid	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to L=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
8	7	eleq2d	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(T\in L\leftrightarrow T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)$$
9		fveq2	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
10	1 9	eqtrid	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to X=\mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
11		fveq2	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to {\cdot }_{\mathrm{𝑖OLD}}\left(U\right)={\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
12	2 11	eqtrid	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to P={\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
13	12	oveqd	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to xPT\left(y\right)=x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)$$
14	12	oveqd	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to T\left(x\right)Py=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y$$
15	13 14	eqeq12d	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(xPT\left(y\right)=T\left(x\right)Py\leftrightarrow x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\right)$$
16	10 15	raleqbidv	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\forall y\in XxPT\left(y\right)=T\left(x\right)Py\leftrightarrow \forall y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\right)$$
17	10 16	raleqbidv	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\forall x\in X\forall y\in XxPT\left(y\right)=T\left(x\right)Py\leftrightarrow \forall x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\forall y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\right)$$
18	8 17	anbi12d	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\left(T\in L\wedge \forall x\in X\forall y\in XxPT\left(y\right)=T\left(x\right)Py\right)\leftrightarrow \left(T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge \forall x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\forall y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\right)\right)$$
19		oveq12	$$⊢\left(U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\wedge U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\to U\mathrm{BLnOp}U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{BLnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
20	19	anidms	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to U\mathrm{BLnOp}U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{BLnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
21	4 20	eqtrid	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to B=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{BLnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
22	21	eleq2d	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(T\in B\leftrightarrow T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{BLnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)$$
23	18 22	imbi12d	$$⊢U=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\left(\left(T\in L\wedge \forall x\in X\forall y\in XxPT\left(y\right)=T\left(x\right)Py\right)\to T\in B\right)\leftrightarrow \left(\left(T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge \forall x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\forall y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\right)\to T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{BLnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)\right)$$
24		eqid	$$⊢\mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)=\mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
25		eqid	$$⊢{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)={\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
26		eqid	$$⊢if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
27		eqid	$$⊢if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{BLnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)=if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{BLnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
28		eqid	$$⊢{norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)={norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
29		eqid	$$⊢⟨⟨+,\times ⟩,\mathrm{abs}⟩=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
30	29	cnchl	$$⊢⟨⟨+,\times ⟩,\mathrm{abs}⟩\in {CHil}_{\mathrm{OLD}}$$
31	30	elimel	$$⊢if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\in {CHil}_{\mathrm{OLD}}$$
32		simpl	$$⊢\left(T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge \forall x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\forall y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\right)\to T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
33		oveq1	$$⊢x=u\to x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=u{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)$$
34		fveq2	$$⊢x=u\to T\left(x\right)=T\left(u\right)$$
35	34	oveq1d	$$⊢x=u\to T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y=T\left(u\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y$$
36	33 35	eqeq12d	$$⊢x=u\to \left(x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\leftrightarrow u{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(u\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\right)$$
37		fveq2	$$⊢y=v\to T\left(y\right)=T\left(v\right)$$
38	37	oveq2d	$$⊢y=v\to u{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=u{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(v\right)$$
39		oveq2	$$⊢y=v\to T\left(u\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y=T\left(u\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)v$$
40	38 39	eqeq12d	$$⊢y=v\to \left(u{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(u\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\leftrightarrow u{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(v\right)=T\left(u\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)v\right)$$
41	36 40	cbvral2vw	$$⊢\forall x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\forall y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\leftrightarrow \forall u\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\forall v\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)u{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(v\right)=T\left(u\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)v$$
42	41	bilani	$$⊢\left(T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge \forall x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\forall y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\right)\to \forall u\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\forall v\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)u{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(v\right)=T\left(u\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)v$$
43		oveq1	$$⊢y=w\to y{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)=w{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)$$
44	43	cbvmptv	$$⊢\left(y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼y{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)\right)=\left(w\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼w{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)\right)$$
45		fveq2	$$⊢x=z\to T\left(x\right)=T\left(z\right)$$
46	45	oveq2d	$$⊢x=z\to w{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)=w{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(z\right)$$
47	46	mpteq2dv	$$⊢x=z\to \left(w\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼w{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)\right)=\left(w\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼w{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(z\right)\right)$$
48	44 47	eqtrid	$$⊢x=z\to \left(y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼y{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)\right)=\left(w\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼w{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(z\right)\right)$$
49	48	cbvmptv	$$⊢\left(x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼\left(y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼y{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)\right)\right)=\left(z\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼\left(w\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼w{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(z\right)\right)\right)$$
50		fveq2	$$⊢x=z\to {norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\left(x\right)={norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\left(z\right)$$
51	50	breq1d	$$⊢x=z\to \left({norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\left(x\right)\le 1\leftrightarrow {norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\left(z\right)\le 1\right)$$
52	51	cbvrabv	$$⊢\left\{x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)|{norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\left(x\right)\le 1\right\}=\left\{z\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)|{norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\left(z\right)\le 1\right\}$$
53	52	imaeq2i	$$⊢\left(x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼\left(y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼y{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)\right)\right)\left[\left\{x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)|{norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\left(x\right)\le 1\right\}\right]=\left(x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼\left(y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)⟼y{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(x\right)\right)\right)\left[\left\{z\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)|{norm}_{CV}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\left(z\right)\le 1\right\}\right]$$
54	24 25 26 27 28 31 29 32 42 49 53	htthlem	$$⊢\left(T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge \forall x\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\forall y\in \mathrm{BaseSet}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)x{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)y\right)\to T\in \left(if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{BLnOp}if\left(U\in {CHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
55	23 54	dedth	$$⊢U\in {CHil}_{\mathrm{OLD}}\to \left(\left(T\in L\wedge \forall x\in X\forall y\in XxPT\left(y\right)=T\left(x\right)Py\right)\to T\in B\right)$$
56	55	3impib	$$⊢\left(U\in {CHil}_{\mathrm{OLD}}\wedge T\in L\wedge \forall x\in X\forall y\in XxPT\left(y\right)=T\left(x\right)Py\right)\to T\in B$$