This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑇 ∈ 𝐿 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) → 𝑇 ∈ 𝐵 )