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	syl5eq	$$⊢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	syl5eq	$$⊢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	syl5eq	$$⊢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	syl5eq	$$⊢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		simpr	$$⊢\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 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$$
34		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)$$
35		fveq2	$$⊢x=u\to T\left(x\right)=T\left(u\right)$$
36	35	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$$
37	34 36	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)$$
38		fveq2	$$⊢y=v\to T\left(y\right)=T\left(v\right)$$
39	38	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)$$
40		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$$
41	39 40	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)$$
42	37 41	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$$
43	33 42	sylib	$$⊢\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$$
44		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)$$
45	44	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)$$
46		fveq2	$$⊢x=z\to T\left(x\right)=T\left(z\right)$$
47	46	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)$$
48	47	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)$$
49	45 48	syl5eq	$$⊢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)$$
50	49	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)$$
51		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)$$
52	51	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)$$
53	52	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\}$$
54	53	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]$$
55	24 25 26 27 28 31 29 32 43 50 54	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)$$
56	23 55	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)$$
57	56	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$$