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 
|- X = ( BaseSet ` U )
htth.2 
|- P = ( .iOLD ` U )
htth.3 
|- L = ( U LnOp U )
htth.4 
|- B = ( U BLnOp U )
Assertion htth 
|- ( ( U e. CHilOLD /\ T e. L /\ A. x e. X A. y e. X ( x P ( T ` y ) ) = ( ( T ` x ) P y ) ) -> T e. B )

Proof

Step Hyp Ref Expression
1 htth.1 
 |-  X = ( BaseSet ` U )
2 htth.2 
 |-  P = ( .iOLD ` U )
3 htth.3 
 |-  L = ( U LnOp U )
4 htth.4 
 |-  B = ( U BLnOp U )
5 oveq12 
 |-  ( ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) /\ U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) -> ( U LnOp U ) = ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
6 5 anidms 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( U LnOp U ) = ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
7 3 6 syl5eq 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> L = ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
8 7 eleq2d 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( T e. L <-> T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ) )
9 fveq2 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( BaseSet ` U ) = ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
10 1 9 syl5eq 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> X = ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
11 fveq2 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( .iOLD ` U ) = ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
12 2 11 syl5eq 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> P = ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
13 12 oveqd 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( x P ( T ` y ) ) = ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) )
14 12 oveqd 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( T ` x ) P y ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) )
15 13 14 eqeq12d 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( x P ( T ` y ) ) = ( ( T ` x ) P y ) <-> ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) )
16 10 15 raleqbidv 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( A. y e. X ( x P ( T ` y ) ) = ( ( T ` x ) P y ) <-> A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) )
17 10 16 raleqbidv 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( A. x e. X A. y e. X ( x P ( T ` y ) ) = ( ( T ` x ) P y ) <-> A. x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) )
18 8 17 anbi12d 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( T e. L /\ A. x e. X A. y e. X ( x P ( T ` y ) ) = ( ( T ` x ) P y ) ) <-> ( T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ A. x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) ) )
19 oveq12 
 |-  ( ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) /\ U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) -> ( U BLnOp U ) = ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) BLnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
20 19 anidms 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( U BLnOp U ) = ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) BLnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
21 4 20 syl5eq 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> B = ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) BLnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
22 21 eleq2d 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( T e. B <-> T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) BLnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ) )
23 18 22 imbi12d 
 |-  ( U = if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( ( T e. L /\ A. x e. X A. y e. X ( x P ( T ` y ) ) = ( ( T ` x ) P y ) ) -> T e. B ) <-> ( ( T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ A. x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) -> T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) BLnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ) ) )
24 eqid 
 |-  ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) = ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) )
25 eqid 
 |-  ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) = ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) )
26 eqid 
 |-  ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) = ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) )
27 eqid 
 |-  ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) BLnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) = ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) BLnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) )
28 eqid 
 |-  ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) = ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) )
29 eqid 
 |-  <. <. + , x. >. , abs >. = <. <. + , x. >. , abs >.
30 29 cnchl 
 |-  <. <. + , x. >. , abs >. e. CHilOLD
31 30 elimel 
 |-  if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) e. CHilOLD
32 simpl 
 |-  ( ( T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ A. x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) -> T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
33 simpr 
 |-  ( ( T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ A. x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) -> A. x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) )
34 oveq1 
 |-  ( x = u -> ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( u ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) )
35 fveq2 
 |-  ( x = u -> ( T ` x ) = ( T ` u ) )
36 35 oveq1d 
 |-  ( x = u -> ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) = ( ( T ` u ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) )
37 34 36 eqeq12d 
 |-  ( x = u -> ( ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) <-> ( u ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` u ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) )
38 fveq2 
 |-  ( y = v -> ( T ` y ) = ( T ` v ) )
39 38 oveq2d 
 |-  ( y = v -> ( u ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( u ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` v ) ) )
40 oveq2 
 |-  ( y = v -> ( ( T ` u ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) = ( ( T ` u ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) v ) )
41 39 40 eqeq12d 
 |-  ( y = v -> ( ( u ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` u ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) <-> ( u ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` v ) ) = ( ( T ` u ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) v ) ) )
42 37 41 cbvral2vw 
 |-  ( A. x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) <-> A. u e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. v e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( u ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` v ) ) = ( ( T ` u ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) v ) )
43 33 42 sylib 
 |-  ( ( T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ A. x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) -> A. u e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. v e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( u ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` v ) ) = ( ( T ` u ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) v ) )
44 oveq1 
 |-  ( y = w -> ( y ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) = ( w ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) )
45 44 cbvmptv 
 |-  ( y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( y ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) ) = ( w e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( w ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) )
46 fveq2 
 |-  ( x = z -> ( T ` x ) = ( T ` z ) )
47 46 oveq2d 
 |-  ( x = z -> ( w ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) = ( w ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` z ) ) )
48 47 mpteq2dv 
 |-  ( x = z -> ( w e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( w ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) ) = ( w e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( w ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` z ) ) ) )
49 45 48 syl5eq 
 |-  ( x = z -> ( y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( y ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) ) = ( w e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( w ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` z ) ) ) )
50 49 cbvmptv 
 |-  ( x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( y ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) ) ) = ( z e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( w e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( w ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` z ) ) ) )
51 fveq2 
 |-  ( x = z -> ( ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ` x ) = ( ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ` z ) )
52 51 breq1d 
 |-  ( x = z -> ( ( ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ` x ) <_ 1 <-> ( ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ` z ) <_ 1 ) )
53 52 cbvrabv 
 |-  { x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) | ( ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ` x ) <_ 1 } = { z e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) | ( ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ` z ) <_ 1 }
54 53 imaeq2i 
 |-  ( ( x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( y ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) ) ) " { x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) | ( ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ` x ) <_ 1 } ) = ( ( x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) |-> ( y ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` x ) ) ) ) " { z e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) | ( ( normCV ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ` z ) <_ 1 } )
55 24 25 26 27 28 31 29 32 43 50 54 htthlem 
 |-  ( ( T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) LnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ A. x e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) A. y e. ( BaseSet ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( x ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) ( T ` y ) ) = ( ( T ` x ) ( .iOLD ` if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) y ) ) -> T e. ( if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) BLnOp if ( U e. CHilOLD , U , <. <. + , x. >. , abs >. ) ) )
56 23 55 dedth 
 |-  ( U e. CHilOLD -> ( ( T e. L /\ A. x e. X A. y e. X ( x P ( T ` y ) ) = ( ( T ` x ) P y ) ) -> T e. B ) )
57 56 3impib 
 |-  ( ( U e. CHilOLD /\ T e. L /\ A. x e. X A. y e. X ( x P ( T ` y ) ) = ( ( T ` x ) P y ) ) -> T e. B )