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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	htth.2	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
	htth.3	⊢ 𝐿 = ( 𝑈 LnOp 𝑈 )
	htth.4	⊢ 𝐵 = ( 𝑈 BLnOp 𝑈 )
Assertion	htth	⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝑇 ∈ 𝐿 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) → 𝑇 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		htth.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		htth.2	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
3		htth.3	⊢ 𝐿 = ( 𝑈 LnOp 𝑈 )
4		htth.4	⊢ 𝐵 = ( 𝑈 BLnOp 𝑈 )
5		oveq12	⊢ ( ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∧ 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) → ( 𝑈 LnOp 𝑈 ) = ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
6	5	anidms	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑈 LnOp 𝑈 ) = ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
7	3 6	eqtrid	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝐿 = ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
8	7	eleq2d	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑇 ∈ 𝐿 ↔ 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
9		fveq2	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
10	1 9	eqtrid	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑋 = ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
11		fveq2	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ·𝑖OLD ‘ 𝑈 ) = ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
12	2 11	eqtrid	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑃 = ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
13	12	oveqd	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) )
14	12	oveqd	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) )
15	13 14	eqeq12d	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ↔ ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) )
16	10 15	raleqbidv	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ↔ ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) )
17	10 16	raleqbidv	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ↔ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) )
18	8 17	anbi12d	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝑇 ∈ 𝐿 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) ↔ ( 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) ) )
19		oveq12	⊢ ( ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∧ 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) → ( 𝑈 BLnOp 𝑈 ) = ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
20	19	anidms	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑈 BLnOp 𝑈 ) = ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
21	4 20	eqtrid	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝐵 = ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
22	21	eleq2d	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑇 ∈ 𝐵 ↔ 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
23	18 22	imbi12d	⊢ ( 𝑈 = if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( ( 𝑇 ∈ 𝐿 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) → 𝑇 ∈ 𝐵 ) ↔ ( ( 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) → 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) )
24		eqid	⊢ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
25		eqid	⊢ ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
26		eqid	⊢ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
27		eqid	⊢ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
28		eqid	⊢ ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
29		eqid	⊢ ⟨ ⟨ + , · ⟩ , abs ⟩ = ⟨ ⟨ + , · ⟩ , abs ⟩
30	29	cnchl	⊢ ⟨ ⟨ + , · ⟩ , abs ⟩ ∈ CHilOLD
31	30	elimel	⊢ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ CHilOLD
32		simpl	⊢ ( ( 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) → 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
33		simpr	⊢ ( ( 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) → ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) )
34		oveq1	⊢ ( 𝑥 = 𝑢 → ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( 𝑢 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) )
35		fveq2	⊢ ( 𝑥 = 𝑢 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑢 ) )
36	35	oveq1d	⊢ ( 𝑥 = 𝑢 → ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) = ( ( 𝑇 ‘ 𝑢 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) )
37	34 36	eqeq12d	⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ↔ ( 𝑢 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑢 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) )
38		fveq2	⊢ ( 𝑦 = 𝑣 → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑣 ) )
39	38	oveq2d	⊢ ( 𝑦 = 𝑣 → ( 𝑢 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( 𝑢 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑣 ) ) )
40		oveq2	⊢ ( 𝑦 = 𝑣 → ( ( 𝑇 ‘ 𝑢 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) = ( ( 𝑇 ‘ 𝑢 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑣 ) )
41	39 40	eqeq12d	⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑢 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ↔ ( 𝑢 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑣 ) ) = ( ( 𝑇 ‘ 𝑢 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑣 ) ) )
42	37 41	cbvral2vw	⊢ ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ↔ ∀ 𝑢 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑣 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑢 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑣 ) ) = ( ( 𝑇 ‘ 𝑢 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑣 ) )
43	33 42	sylib	⊢ ( ( 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) → ∀ 𝑢 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑣 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑢 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑣 ) ) = ( ( 𝑇 ‘ 𝑢 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑣 ) )
44		oveq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) = ( 𝑤 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) )
45	44	cbvmptv	⊢ ( 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑦 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑤 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑤 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) )
46		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑧 ) )
47	46	oveq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑤 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) = ( 𝑤 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑧 ) ) )
48	47	mpteq2dv	⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑤 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑤 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑤 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑧 ) ) ) )
49	45 48	eqtrid	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑦 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑤 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑤 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑧 ) ) ) )
50	49	cbvmptv	⊢ ( 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑦 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) ) ) = ( 𝑧 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑤 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑤 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑧 ) ) ) )
51		fveq2	⊢ ( 𝑥 = 𝑧 → ( ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑥 ) = ( ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑧 ) )
52	51	breq1d	⊢ ( 𝑥 = 𝑧 → ( ( ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑥 ) ≤ 1 ↔ ( ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑧 ) ≤ 1 ) )
53	52	cbvrabv	⊢ { 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∣ ( ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑥 ) ≤ 1 } = { 𝑧 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∣ ( ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑧 ) ≤ 1 }
54	53	imaeq2i	⊢ ( ( 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑦 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) ) ) “ { 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∣ ( ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑥 ) ≤ 1 } ) = ( ( 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ↦ ( 𝑦 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑥 ) ) ) ) “ { 𝑧 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∣ ( ( normCV ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑧 ) ≤ 1 } )
55	24 25 26 27 28 31 29 32 43 50 54	htthlem	⊢ ( ( 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) LnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∀ 𝑦 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑥 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝑦 ) ) → 𝑇 ∈ ( if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑈 ∈ CHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
56	23 55	dedth	⊢ ( 𝑈 ∈ CHilOLD → ( ( 𝑇 ∈ 𝐿 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) → 𝑇 ∈ 𝐵 ) )
57	56	3impib	⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝑇 ∈ 𝐿 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) → 𝑇 ∈ 𝐵 )