Metamath Proof Explorer

Theorem hspmbllem2

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspmbllem2.h 
|- H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) )
hspmbllem2.x 
|- ( ph -> X e. Fin )
hspmbllem2.k 
|- ( ph -> K e. X )
hspmbllem2.y 
|- ( ph -> Y e. RR )
hspmbllem2.e 
|- ( ph -> E e. RR+ )
hspmbllem2.c 
|- ( ph -> C : NN --> ( RR ^m X ) )
hspmbllem2.d 
|- ( ph -> D : NN --> ( RR ^m X ) )
hspmbllem2.a 
|- ( ph -> A C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
hspmbllem2.g 
|- ( ph -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + E ) )
hspmbllem2.r 
|- ( ph -> ( ( voln* ` X ) ` A ) e. RR )
hspmbllem2.i 
|- ( ph -> ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) e. RR )
hspmbllem2.f 
|- ( ph -> ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) e. RR )
hspmbllem2.l 
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
hspmbllem2.t 
|- T = ( y e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) )
hspmbllem2.s 
|- S = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h = K , if ( x <_ ( c ` h ) , ( c ` h ) , x ) , ( c ` h ) ) ) ) )
Assertion hspmbllem2 
|- ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + E ) )

Proof

Step Hyp Ref Expression
1 hspmbllem2.h 
 |-  H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) )
2 hspmbllem2.x 
 |-  ( ph -> X e. Fin )
3 hspmbllem2.k 
 |-  ( ph -> K e. X )
4 hspmbllem2.y 
 |-  ( ph -> Y e. RR )
5 hspmbllem2.e 
 |-  ( ph -> E e. RR+ )
6 hspmbllem2.c 
 |-  ( ph -> C : NN --> ( RR ^m X ) )
7 hspmbllem2.d 
 |-  ( ph -> D : NN --> ( RR ^m X ) )
8 hspmbllem2.a 
 |-  ( ph -> A C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
9 hspmbllem2.g 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + E ) )
10 hspmbllem2.r 
 |-  ( ph -> ( ( voln* ` X ) ` A ) e. RR )
11 hspmbllem2.i 
 |-  ( ph -> ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) e. RR )
12 hspmbllem2.f 
 |-  ( ph -> ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) e. RR )
13 hspmbllem2.l 
 |-  L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
14 hspmbllem2.t 
 |-  T = ( y e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) )
15 hspmbllem2.s 
 |-  S = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h = K , if ( x <_ ( c ` h ) , ( c ` h ) , x ) , ( c ` h ) ) ) ) )
16 11 12 readdcld 
 |-  ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) e. RR )
17 5 rpred 
 |-  ( ph -> E e. RR )
18 10 17 readdcld 
 |-  ( ph -> ( ( ( voln* ` X ) ` A ) + E ) e. RR )
19 nfv 
 |-  F/ j ph
20 nnex 
 |-  NN e. _V
21 20 a1i 
 |-  ( ph -> NN e. _V )
22 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
23 2 adantr 
 |-  ( ( ph /\ j e. NN ) -> X e. Fin )
24 6 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m X ) )
25 elmapi 
 |-  ( ( C ` j ) e. ( RR ^m X ) -> ( C ` j ) : X --> RR )
26 24 25 syl 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) : X --> RR )
27 7 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m X ) )
28 elmapi 
 |-  ( ( D ` j ) e. ( RR ^m X ) -> ( D ` j ) : X --> RR )
29 27 28 syl 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) : X --> RR )
30 13 23 26 29 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) e. ( 0 [,) +oo ) )
31 22 30 sseldi 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) e. ( 0 [,] +oo ) )
32 19 21 31 sge0clmpt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) e. ( 0 [,] +oo ) )
33 ne0i 
 |-  ( K e. X -> X =/= (/) )
34 3 33 syl 
 |-  ( ph -> X =/= (/) )
35 34 adantr 
 |-  ( ( ph /\ j e. NN ) -> X =/= (/) )
36 13 23 35 26 29 hoidmvn0val 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) = prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
37 36 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) )
38 37 fveq2d 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) ) ) )
39 38 9 eqbrtrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + E ) )
40 18 32 39 ge0lere 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) e. RR )
41 4 adantr 
 |-  ( ( ph /\ j e. NN ) -> Y e. RR )
42 14 41 23 29 hsphoif 
 |-  ( ( ph /\ j e. NN ) -> ( ( T ` Y ) ` ( D ` j ) ) : X --> RR )
43 13 23 26 42 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
44 22 43 sseldi 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
45 19 21 44 sge0clmpt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) )
46 oveq2 
 |-  ( x = y -> ( RR ^m x ) = ( RR ^m y ) )
47 eqeq1 
 |-  ( x = y -> ( x = (/) <-> y = (/) ) )
48 prodeq1 
 |-  ( x = y -> prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = prod_ k e. y ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) )
49 47 48 ifbieq2d 
 |-  ( x = y -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( y = (/) , 0 , prod_ k e. y ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) )
50 46 46 49 mpoeq123dv 
 |-  ( x = y -> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) = ( a e. ( RR ^m y ) , b e. ( RR ^m y ) |-> if ( y = (/) , 0 , prod_ k e. y ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
51 50 cbvmptv 
 |-  ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) ) = ( y e. Fin |-> ( a e. ( RR ^m y ) , b e. ( RR ^m y ) |-> if ( y = (/) , 0 , prod_ k e. y ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
52 13 51 eqtri 
 |-  L = ( y e. Fin |-> ( a e. ( RR ^m y ) , b e. ( RR ^m y ) |-> if ( y = (/) , 0 , prod_ k e. y ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
53 diffi 
 |-  ( X e. Fin -> ( X \ { K } ) e. Fin )
54 2 53 syl 
 |-  ( ph -> ( X \ { K } ) e. Fin )
55 snfi 
 |-  { K } e. Fin
56 55 a1i 
 |-  ( ph -> { K } e. Fin )
57 unfi 
 |-  ( ( ( X \ { K } ) e. Fin /\ { K } e. Fin ) -> ( ( X \ { K } ) u. { K } ) e. Fin )
58 54 56 57 syl2anc 
 |-  ( ph -> ( ( X \ { K } ) u. { K } ) e. Fin )
59 58 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( ( X \ { K } ) u. { K } ) e. Fin )
60 snidg 
 |-  ( K e. X -> K e. { K } )
61 3 60 syl 
 |-  ( ph -> K e. { K } )
62 elun2 
 |-  ( K e. { K } -> K e. ( ( X \ { K } ) u. { K } ) )
63 61 62 syl 
 |-  ( ph -> K e. ( ( X \ { K } ) u. { K } ) )
64 neldifsnd 
 |-  ( ph -> -. K e. ( X \ { K } ) )
65 63 64 eldifd 
 |-  ( ph -> K e. ( ( ( X \ { K } ) u. { K } ) \ ( X \ { K } ) ) )
66 65 adantr 
 |-  ( ( ph /\ j e. NN ) -> K e. ( ( ( X \ { K } ) u. { K } ) \ ( X \ { K } ) ) )
67 eqid 
 |-  ( ( X \ { K } ) u. { K } ) = ( ( X \ { K } ) u. { K } )
68 eqid 
 |-  ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) = ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) )
69 uncom 
 |-  ( ( X \ { K } ) u. { K } ) = ( { K } u. ( X \ { K } ) )
70 69 a1i 
 |-  ( ph -> ( ( X \ { K } ) u. { K } ) = ( { K } u. ( X \ { K } ) ) )
71 3 snssd 
 |-  ( ph -> { K } C_ X )
72 undif 
 |-  ( { K } C_ X <-> ( { K } u. ( X \ { K } ) ) = X )
73 71 72 sylib 
 |-  ( ph -> ( { K } u. ( X \ { K } ) ) = X )
74 70 73 eqtrd 
 |-  ( ph -> ( ( X \ { K } ) u. { K } ) = X )
75 74 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( ( X \ { K } ) u. { K } ) = X )
76 75 feq2d 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) : ( ( X \ { K } ) u. { K } ) --> RR <-> ( C ` j ) : X --> RR ) )
77 26 76 mpbird 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) : ( ( X \ { K } ) u. { K } ) --> RR )
78 75 feq2d 
 |-  ( ( ph /\ j e. NN ) -> ( ( D ` j ) : ( ( X \ { K } ) u. { K } ) --> RR <-> ( D ` j ) : X --> RR ) )
79 29 78 mpbird 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) : ( ( X \ { K } ) u. { K } ) --> RR )
80 52 59 66 67 41 68 77 79 hsphoidmvle 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` ( ( X \ { K } ) u. { K } ) ) ( ( ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) ` Y ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` ( ( X \ { K } ) u. { K } ) ) ( D ` j ) ) )
81 74 fveq2d 
 |-  ( ph -> ( L ` ( ( X \ { K } ) u. { K } ) ) = ( L ` X ) )
82 eqidd 
 |-  ( ph -> ( C ` j ) = ( C ` j ) )
83 14 a1i 
 |-  ( ph -> T = ( y e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) )
84 74 oveq2d 
 |-  ( ph -> ( RR ^m ( ( X \ { K } ) u. { K } ) ) = ( RR ^m X ) )
85 74 mpteq1d 
 |-  ( ph -> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) = ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) )
86 84 85 mpteq12dv 
 |-  ( ph -> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) = ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) )
87 86 eqcomd 
 |-  ( ph -> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) = ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) )
88 87 mpteq2dv 
 |-  ( ph -> ( y e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) = ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) )
89 83 88 eqtr2d 
 |-  ( ph -> ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) = T )
90 89 fveq1d 
 |-  ( ph -> ( ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) ` Y ) = ( T ` Y ) )
91 90 fveq1d 
 |-  ( ph -> ( ( ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) ` Y ) ` ( D ` j ) ) = ( ( T ` Y ) ` ( D ` j ) ) )
92 81 82 91 oveq123d 
 |-  ( ph -> ( ( C ` j ) ( L ` ( ( X \ { K } ) u. { K } ) ) ( ( ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) ` Y ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) )
93 92 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` ( ( X \ { K } ) u. { K } ) ) ( ( ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) ` Y ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) )
94 81 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( L ` ( ( X \ { K } ) u. { K } ) ) = ( L ` X ) )
95 94 oveqd 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` ( ( X \ { K } ) u. { K } ) ) ( D ` j ) ) = ( ( C ` j ) ( L ` X ) ( D ` j ) ) )
96 93 95 breq12d 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) ( L ` ( ( X \ { K } ) u. { K } ) ) ( ( ( y e. RR |-> ( c e. ( RR ^m ( ( X \ { K } ) u. { K } ) ) |-> ( h e. ( ( X \ { K } ) u. { K } ) |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) ` Y ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` ( ( X \ { K } ) u. { K } ) ) ( D ` j ) ) <-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) )
97 80 96 mpbid 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` X ) ( D ` j ) ) )
98 19 21 44 31 97 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
99 40 45 98 ge0lere 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) e. RR )
100 15 41 23 26 hoidifhspf 
 |-  ( ( ph /\ j e. NN ) -> ( ( S ` Y ) ` ( C ` j ) ) : X --> RR )
101 13 23 100 29 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) e. ( 0 [,) +oo ) )
102 101 fmpttd 
 |-  ( ph -> ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) : NN --> ( 0 [,) +oo ) )
103 22 a1i 
 |-  ( ph -> ( 0 [,) +oo ) C_ ( 0 [,] +oo ) )
104 102 103 fssd 
 |-  ( ph -> ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) : NN --> ( 0 [,] +oo ) )
105 21 104 sge0cl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) e. ( 0 [,] +oo ) )
106 22 101 sseldi 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) e. ( 0 [,] +oo ) )
107 3 adantr 
 |-  ( ( ph /\ j e. NN ) -> K e. X )
108 13 23 26 29 107 15 41 hoidifhspdmvle 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) <_ ( ( C ` j ) ( L ` X ) ( D ` j ) ) )
109 19 21 106 31 108 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
110 40 105 109 ge0lere 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) e. RR )
111 4 adantr 
 |-  ( ( ph /\ l e. NN ) -> Y e. RR )
112 2 adantr 
 |-  ( ( ph /\ l e. NN ) -> X e. Fin )
113 eleq1w 
 |-  ( j = l -> ( j e. NN <-> l e. NN ) )
114 113 anbi2d 
 |-  ( j = l -> ( ( ph /\ j e. NN ) <-> ( ph /\ l e. NN ) ) )
115 fveq2 
 |-  ( j = l -> ( D ` j ) = ( D ` l ) )
116 115 feq1d 
 |-  ( j = l -> ( ( D ` j ) : X --> RR <-> ( D ` l ) : X --> RR ) )
117 114 116 imbi12d 
 |-  ( j = l -> ( ( ( ph /\ j e. NN ) -> ( D ` j ) : X --> RR ) <-> ( ( ph /\ l e. NN ) -> ( D ` l ) : X --> RR ) ) )
118 117 29 chvarvv 
 |-  ( ( ph /\ l e. NN ) -> ( D ` l ) : X --> RR )
119 14 111 112 118 hsphoif 
 |-  ( ( ph /\ l e. NN ) -> ( ( T ` Y ) ` ( D ` l ) ) : X --> RR )
120 reex 
 |-  RR e. _V
121 120 a1i 
 |-  ( ph -> RR e. _V )
122 121 2 jca 
 |-  ( ph -> ( RR e. _V /\ X e. Fin ) )
123 122 adantr 
 |-  ( ( ph /\ l e. NN ) -> ( RR e. _V /\ X e. Fin ) )
124 elmapg 
 |-  ( ( RR e. _V /\ X e. Fin ) -> ( ( ( T ` Y ) ` ( D ` l ) ) e. ( RR ^m X ) <-> ( ( T ` Y ) ` ( D ` l ) ) : X --> RR ) )
125 123 124 syl 
 |-  ( ( ph /\ l e. NN ) -> ( ( ( T ` Y ) ` ( D ` l ) ) e. ( RR ^m X ) <-> ( ( T ` Y ) ` ( D ` l ) ) : X --> RR ) )
126 119 125 mpbird 
 |-  ( ( ph /\ l e. NN ) -> ( ( T ` Y ) ` ( D ` l ) ) e. ( RR ^m X ) )
127 126 fmpttd 
 |-  ( ph -> ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) : NN --> ( RR ^m X ) )
128 simpl 
 |-  ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) -> ph )
129 elinel1 
 |-  ( f e. ( A i^i ( K ( H ` X ) Y ) ) -> f e. A )
130 129 adantl 
 |-  ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) -> f e. A )
131 8 sselda 
 |-  ( ( ph /\ f e. A ) -> f e. U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
132 eliun 
 |-  ( f e. U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
133 131 132 sylib 
 |-  ( ( ph /\ f e. A ) -> E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
134 128 130 133 syl2anc 
 |-  ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) -> E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
135 simpll 
 |-  ( ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) /\ j e. NN ) -> ph )
136 elinel2 
 |-  ( f e. ( A i^i ( K ( H ` X ) Y ) ) -> f e. ( K ( H ` X ) Y ) )
137 136 adantl 
 |-  ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) -> f e. ( K ( H ` X ) Y ) )
138 137 adantr 
 |-  ( ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) /\ j e. NN ) -> f e. ( K ( H ` X ) Y ) )
139 simpr 
 |-  ( ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) /\ j e. NN ) -> j e. NN )
140 ixpfn 
 |-  ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> f Fn X )
141 140 adantl 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> f Fn X )
142 nfv 
 |-  F/ k ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN )
143 nfcv 
 |-  F/_ k f
144 nfixp1 
 |-  F/_ k X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) )
145 143 144 nfel 
 |-  F/ k f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) )
146 142 145 nfan 
 |-  F/ k ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
147 26 3adant3 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( C ` j ) : X --> RR )
148 simp3 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> k e. X )
149 147 148 ffvelrnd 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( C ` j ) ` k ) e. RR )
150 149 rexrd 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( C ` j ) ` k ) e. RR* )
151 150 ad5ant135 
 |-  ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( C ` j ) ` k ) e. RR* )
152 42 3adant3 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( T ` Y ) ` ( D ` j ) ) : X --> RR )
153 152 148 ffvelrnd 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) e. RR )
154 153 rexrd 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) e. RR* )
155 154 ad5ant135 
 |-  ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) e. RR* )
156 iftrue 
 |-  ( k = K -> if ( k = K , ( -oo (,) Y ) , RR ) = ( -oo (,) Y ) )
157 ioossre 
 |-  ( -oo (,) Y ) C_ RR
158 157 a1i 
 |-  ( k = K -> ( -oo (,) Y ) C_ RR )
159 156 158 eqsstrd 
 |-  ( k = K -> if ( k = K , ( -oo (,) Y ) , RR ) C_ RR )
160 iffalse 
 |-  ( -. k = K -> if ( k = K , ( -oo (,) Y ) , RR ) = RR )
161 ssid 
 |-  RR C_ RR
162 161 a1i 
 |-  ( -. k = K -> RR C_ RR )
163 160 162 eqsstrd 
 |-  ( -. k = K -> if ( k = K , ( -oo (,) Y ) , RR ) C_ RR )
164 159 163 pm2.61i 
 |-  if ( k = K , ( -oo (,) Y ) , RR ) C_ RR
165 simpr 
 |-  ( ( ph /\ f e. ( K ( H ` X ) Y ) ) -> f e. ( K ( H ` X ) Y ) )
166 1 2 3 4 hspval 
 |-  ( ph -> ( K ( H ` X ) Y ) = X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) )
167 166 adantr 
 |-  ( ( ph /\ f e. ( K ( H ` X ) Y ) ) -> ( K ( H ` X ) Y ) = X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) )
168 165 167 eleqtrd 
 |-  ( ( ph /\ f e. ( K ( H ` X ) Y ) ) -> f e. X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) )
169 168 adantr 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X ) -> f e. X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) )
170 simpr 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X ) -> k e. X )
171 vex 
 |-  f e. _V
172 171 elixp 
 |-  ( f e. X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) <-> ( f Fn X /\ A. k e. X ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) ) )
173 172 biimpi 
 |-  ( f e. X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) -> ( f Fn X /\ A. k e. X ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) ) )
174 173 simprd 
 |-  ( f e. X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) -> A. k e. X ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
175 174 adantr 
 |-  ( ( f e. X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) /\ k e. X ) -> A. k e. X ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
176 simpr 
 |-  ( ( f e. X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) /\ k e. X ) -> k e. X )
177 rspa 
 |-  ( ( A. k e. X ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) /\ k e. X ) -> ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
178 175 176 177 syl2anc 
 |-  ( ( f e. X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) /\ k e. X ) -> ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
179 169 170 178 syl2anc 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X ) -> ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
180 164 179 sseldi 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X ) -> ( f ` k ) e. RR )
181 180 rexrd 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X ) -> ( f ` k ) e. RR* )
182 181 ad4ant14 
 |-  ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) e. RR* )
183 150 ad4ant124 
 |-  ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( C ` j ) ` k ) e. RR* )
184 29 3adant3 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( D ` j ) : X --> RR )
185 184 148 ffvelrnd 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( D ` j ) ` k ) e. RR )
186 185 rexrd 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( D ` j ) ` k ) e. RR* )
187 186 ad4ant124 
 |-  ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( D ` j ) ` k ) e. RR* )
188 171 elixp 
 |-  ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> ( f Fn X /\ A. k e. X ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
189 188 biimpi 
 |-  ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> ( f Fn X /\ A. k e. X ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
190 189 simprd 
 |-  ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> A. k e. X ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
191 190 adantr 
 |-  ( ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. X ) -> A. k e. X ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
192 simpr 
 |-  ( ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. X ) -> k e. X )
193 rspa 
 |-  ( ( A. k e. X ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. X ) -> ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
194 191 192 193 syl2anc 
 |-  ( ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. X ) -> ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
195 194 adantll 
 |-  ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
196 icogelb 
 |-  ( ( ( ( C ` j ) ` k ) e. RR* /\ ( ( D ` j ) ` k ) e. RR* /\ ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( ( C ` j ) ` k ) <_ ( f ` k ) )
197 183 187 195 196 syl3anc 
 |-  ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( C ` j ) ` k ) <_ ( f ` k ) )
198 197 adantl3r 
 |-  ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( C ` j ) ` k ) <_ ( f ` k ) )
199 icoltub 
 |-  ( ( ( ( C ` j ) ` k ) e. RR* /\ ( ( D ` j ) ` k ) e. RR* /\ ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( f ` k ) < ( ( D ` j ) ` k ) )
200 183 187 195 199 syl3anc 
 |-  ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) < ( ( D ` j ) ` k ) )
201 200 adantl3r 
 |-  ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) < ( ( D ` j ) ` k ) )
202 201 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ ( ( D ` j ) ` k ) <_ Y ) -> ( f ` k ) < ( ( D ` j ) ` k ) )
203 simpll 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) -> ph )
204 simpr 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) -> j e. NN )
205 203 204 jca 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) -> ( ph /\ j e. NN ) )
206 205 3ad2ant1 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> ( ph /\ j e. NN ) )
207 simp2 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> k = K )
208 simp3 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> ( ( D ` j ) ` k ) <_ Y )
209 fveq2 
 |-  ( k = K -> ( ( D ` j ) ` k ) = ( ( D ` j ) ` K ) )
210 209 breq1d 
 |-  ( k = K -> ( ( ( D ` j ) ` k ) <_ Y <-> ( ( D ` j ) ` K ) <_ Y ) )
211 210 biimpa 
 |-  ( ( k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> ( ( D ` j ) ` K ) <_ Y )
212 211 iftrued 
 |-  ( ( k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = ( ( D ` j ) ` K ) )
213 209 eqcomd 
 |-  ( k = K -> ( ( D ` j ) ` K ) = ( ( D ` j ) ` k ) )
214 213 adantr 
 |-  ( ( k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> ( ( D ` j ) ` K ) = ( ( D ` j ) ` k ) )
215 212 214 eqtrd 
 |-  ( ( k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = ( ( D ` j ) ` k ) )
216 215 3adant1 
 |-  ( ( ( ph /\ j e. NN ) /\ k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = ( ( D ` j ) ` k ) )
217 breq2 
 |-  ( y = Y -> ( ( c ` h ) <_ y <-> ( c ` h ) <_ Y ) )
218 id 
 |-  ( y = Y -> y = Y )
219 217 218 ifbieq2d 
 |-  ( y = Y -> if ( ( c ` h ) <_ y , ( c ` h ) , y ) = if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) )
220 219 ifeq2d 
 |-  ( y = Y -> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) = if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) )
221 220 mpteq2dv 
 |-  ( y = Y -> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) = ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) ) )
222 221 mpteq2dv 
 |-  ( y = Y -> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) = ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) ) ) )
223 ovex 
 |-  ( RR ^m X ) e. _V
224 223 mptex 
 |-  ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) ) ) e. _V
225 224 a1i 
 |-  ( ph -> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) ) ) e. _V )
226 14 222 4 225 fvmptd3 
 |-  ( ph -> ( T ` Y ) = ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) ) ) )
227 226 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( T ` Y ) = ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) ) ) )
228 fveq1 
 |-  ( c = ( D ` j ) -> ( c ` h ) = ( ( D ` j ) ` h ) )
229 228 breq1d 
 |-  ( c = ( D ` j ) -> ( ( c ` h ) <_ Y <-> ( ( D ` j ) ` h ) <_ Y ) )
230 229 228 ifbieq1d 
 |-  ( c = ( D ` j ) -> if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) = if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) )
231 228 230 ifeq12d 
 |-  ( c = ( D ` j ) -> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) = if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) )
232 231 mpteq2dv 
 |-  ( c = ( D ` j ) -> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) ) = ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) )
233 232 adantl 
 |-  ( ( ( ph /\ j e. NN ) /\ c = ( D ` j ) ) -> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ Y , ( c ` h ) , Y ) ) ) = ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) )
234 mptexg 
 |-  ( X e. Fin -> ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) e. _V )
235 2 234 syl 
 |-  ( ph -> ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) e. _V )
236 235 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) e. _V )
237 227 233 27 236 fvmptd 
 |-  ( ( ph /\ j e. NN ) -> ( ( T ` Y ) ` ( D ` j ) ) = ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) )
238 237 fveq1d 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) = ( ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) ` k ) )
239 238 3adant3 
 |-  ( ( ph /\ j e. NN /\ k = K ) -> ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) = ( ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) ` k ) )
240 simpl 
 |-  ( ( ph /\ k = K ) -> ph )
241 simpr 
 |-  ( ( ph /\ k = K ) -> k = K )
242 240 3 syl 
 |-  ( ( ph /\ k = K ) -> K e. X )
243 241 242 eqeltrd 
 |-  ( ( ph /\ k = K ) -> k e. X )
244 eqidd 
 |-  ( ( ph /\ k e. X ) -> ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) = ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) )
245 eleq1w 
 |-  ( h = k -> ( h e. ( X \ { K } ) <-> k e. ( X \ { K } ) ) )
246 fveq2 
 |-  ( h = k -> ( ( D ` j ) ` h ) = ( ( D ` j ) ` k ) )
247 246 breq1d 
 |-  ( h = k -> ( ( ( D ` j ) ` h ) <_ Y <-> ( ( D ` j ) ` k ) <_ Y ) )
248 247 246 ifbieq1d 
 |-  ( h = k -> if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) = if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) )
249 245 246 248 ifbieq12d 
 |-  ( h = k -> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) = if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) )
250 249 adantl 
 |-  ( ( ( ph /\ k e. X ) /\ h = k ) -> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) = if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) )
251 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
252 fvexd 
 |-  ( ph -> ( ( D ` j ) ` k ) e. _V )
253 252 4 ifexd 
 |-  ( ph -> if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) e. _V )
254 252 253 ifexd 
 |-  ( ph -> if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) e. _V )
255 254 adantr 
 |-  ( ( ph /\ k e. X ) -> if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) e. _V )
256 244 250 251 255 fvmptd 
 |-  ( ( ph /\ k e. X ) -> ( ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) ` k ) = if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) )
257 240 243 256 syl2anc 
 |-  ( ( ph /\ k = K ) -> ( ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) ` k ) = if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) )
258 eleq1 
 |-  ( k = K -> ( k e. ( X \ { K } ) <-> K e. ( X \ { K } ) ) )
259 210 209 ifbieq1d 
 |-  ( k = K -> if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) = if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) )
260 258 209 259 ifbieq12d 
 |-  ( k = K -> if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) = if ( K e. ( X \ { K } ) , ( ( D ` j ) ` K ) , if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) ) )
261 260 adantl 
 |-  ( ( ph /\ k = K ) -> if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) = if ( K e. ( X \ { K } ) , ( ( D ` j ) ` K ) , if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) ) )
262 257 261 eqtrd 
 |-  ( ( ph /\ k = K ) -> ( ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) ` k ) = if ( K e. ( X \ { K } ) , ( ( D ` j ) ` K ) , if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) ) )
263 262 3adant2 
 |-  ( ( ph /\ j e. NN /\ k = K ) -> ( ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) ` k ) = if ( K e. ( X \ { K } ) , ( ( D ` j ) ` K ) , if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) ) )
264 neldifsnd 
 |-  ( k = K -> -. K e. ( X \ { K } ) )
265 264 iffalsed 
 |-  ( k = K -> if ( K e. ( X \ { K } ) , ( ( D ` j ) ` K ) , if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) ) = if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) )
266 265 3ad2ant3 
 |-  ( ( ph /\ j e. NN /\ k = K ) -> if ( K e. ( X \ { K } ) , ( ( D ` j ) ` K ) , if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) ) = if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) )
267 239 263 266 3eqtrrd 
 |-  ( ( ph /\ j e. NN /\ k = K ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
268 267 3expa 
 |-  ( ( ( ph /\ j e. NN ) /\ k = K ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
269 268 3adant3 
 |-  ( ( ( ph /\ j e. NN ) /\ k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
270 216 269 eqtr3d 
 |-  ( ( ( ph /\ j e. NN ) /\ k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> ( ( D ` j ) ` k ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
271 206 207 208 270 syl3anc 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k = K /\ ( ( D ` j ) ` k ) <_ Y ) -> ( ( D ` j ) ` k ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
272 271 ad5ant145 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ ( ( D ` j ) ` k ) <_ Y ) -> ( ( D ` j ) ` k ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
273 202 272 breqtrd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ ( ( D ` j ) ` k ) <_ Y ) -> ( f ` k ) < ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
274 mnfxr 
 |-  -oo e. RR*
275 274 a1i 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X /\ k = K ) -> -oo e. RR* )
276 4 rexrd 
 |-  ( ph -> Y e. RR* )
277 276 adantr 
 |-  ( ( ph /\ f e. ( K ( H ` X ) Y ) ) -> Y e. RR* )
278 277 3ad2ant1 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X /\ k = K ) -> Y e. RR* )
279 179 3adant3 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X /\ k = K ) -> ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
280 156 3ad2ant3 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X /\ k = K ) -> if ( k = K , ( -oo (,) Y ) , RR ) = ( -oo (,) Y ) )
281 279 280 eleqtrd 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X /\ k = K ) -> ( f ` k ) e. ( -oo (,) Y ) )
282 iooltub 
 |-  ( ( -oo e. RR* /\ Y e. RR* /\ ( f ` k ) e. ( -oo (,) Y ) ) -> ( f ` k ) < Y )
283 275 278 281 282 syl3anc 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ k e. X /\ k = K ) -> ( f ` k ) < Y )
284 283 3adant1r 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k e. X /\ k = K ) -> ( f ` k ) < Y )
285 284 ad4ant123 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k e. X ) /\ k = K ) /\ -. ( ( D ` j ) ` k ) <_ Y ) -> ( f ` k ) < Y )
286 simpr 
 |-  ( ( k = K /\ -. ( ( D ` j ) ` k ) <_ Y ) -> -. ( ( D ` j ) ` k ) <_ Y )
287 210 notbid 
 |-  ( k = K -> ( -. ( ( D ` j ) ` k ) <_ Y <-> -. ( ( D ` j ) ` K ) <_ Y ) )
288 287 adantr 
 |-  ( ( k = K /\ -. ( ( D ` j ) ` k ) <_ Y ) -> ( -. ( ( D ` j ) ` k ) <_ Y <-> -. ( ( D ` j ) ` K ) <_ Y ) )
289 286 288 mpbid 
 |-  ( ( k = K /\ -. ( ( D ` j ) ` k ) <_ Y ) -> -. ( ( D ` j ) ` K ) <_ Y )
290 289 iffalsed 
 |-  ( ( k = K /\ -. ( ( D ` j ) ` k ) <_ Y ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = Y )
291 eqidd 
 |-  ( ( k = K /\ -. ( ( D ` j ) ` k ) <_ Y ) -> Y = Y )
292 290 291 eqtr2d 
 |-  ( ( k = K /\ -. ( ( D ` j ) ` k ) <_ Y ) -> Y = if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) )
293 292 adantll 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k e. X ) /\ k = K ) /\ -. ( ( D ` j ) ` k ) <_ Y ) -> Y = if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) )
294 268 adantlr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. X ) /\ k = K ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
295 294 adantl3r 
 |-  ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k e. X ) /\ k = K ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
296 295 adantr 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k e. X ) /\ k = K ) /\ -. ( ( D ` j ) ` k ) <_ Y ) -> if ( ( ( D ` j ) ` K ) <_ Y , ( ( D ` j ) ` K ) , Y ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
297 293 296 eqtrd 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k e. X ) /\ k = K ) /\ -. ( ( D ` j ) ` k ) <_ Y ) -> Y = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
298 285 297 breqtrd 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k e. X ) /\ k = K ) /\ -. ( ( D ` j ) ` k ) <_ Y ) -> ( f ` k ) < ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
299 298 adantl3r 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ -. ( ( D ` j ) ` k ) <_ Y ) -> ( f ` k ) < ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
300 273 299 pm2.61dan 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) -> ( f ` k ) < ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
301 201 adantr 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> ( f ` k ) < ( ( D ` j ) ` k ) )
302 237 3adant3 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( T ` Y ) ` ( D ` j ) ) = ( h e. X |-> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) ) )
303 249 adantl 
 |-  ( ( ( ph /\ j e. NN /\ k e. X ) /\ h = k ) -> if ( h e. ( X \ { K } ) , ( ( D ` j ) ` h ) , if ( ( ( D ` j ) ` h ) <_ Y , ( ( D ` j ) ` h ) , Y ) ) = if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) )
304 255 3adant2 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) e. _V )
305 302 303 148 304 fvmptd 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) = if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) )
306 305 3expa 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) = if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) )
307 306 adantllr 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ k e. X ) -> ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) = if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) )
308 307 ad4ant13 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) = if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) )
309 simpl 
 |-  ( ( k e. X /\ -. k = K ) -> k e. X )
310 neqne 
 |-  ( -. k = K -> k =/= K )
311 nelsn 
 |-  ( k =/= K -> -. k e. { K } )
312 310 311 syl 
 |-  ( -. k = K -> -. k e. { K } )
313 312 adantl 
 |-  ( ( k e. X /\ -. k = K ) -> -. k e. { K } )
314 309 313 eldifd 
 |-  ( ( k e. X /\ -. k = K ) -> k e. ( X \ { K } ) )
315 314 iftrued 
 |-  ( ( k e. X /\ -. k = K ) -> if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) = ( ( D ` j ) ` k ) )
316 315 adantll 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> if ( k e. ( X \ { K } ) , ( ( D ` j ) ` k ) , if ( ( ( D ` j ) ` k ) <_ Y , ( ( D ` j ) ` k ) , Y ) ) = ( ( D ` j ) ` k ) )
317 308 316 eqtr2d 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> ( ( D ` j ) ` k ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
318 301 317 breqtrd 
 |-  ( ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> ( f ` k ) < ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
319 300 318 pm2.61dan 
 |-  ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) < ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
320 151 155 182 198 319 elicod 
 |-  ( ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
321 320 ex 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( k e. X -> ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) ) )
322 146 321 ralrimi 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> A. k e. X ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
323 141 322 jca 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( f Fn X /\ A. k e. X ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) ) )
324 171 elixp 
 |-  ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) <-> ( f Fn X /\ A. k e. X ( f ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) ) )
325 323 324 sylibr 
 |-  ( ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
326 325 ex 
 |-  ( ( ( ph /\ f e. ( K ( H ` X ) Y ) ) /\ j e. NN ) -> ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) ) )
327 135 138 139 326 syl21anc 
 |-  ( ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) /\ j e. NN ) -> ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) ) )
328 327 reximdva 
 |-  ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) -> ( E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) ) )
329 134 328 mpd 
 |-  ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) -> E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
330 eliun 
 |-  ( f e. U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) <-> E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
331 329 330 sylibr 
 |-  ( ( ph /\ f e. ( A i^i ( K ( H ` X ) Y ) ) ) -> f e. U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
332 331 ralrimiva 
 |-  ( ph -> A. f e. ( A i^i ( K ( H ` X ) Y ) ) f e. U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
333 dfss3 
 |-  ( ( A i^i ( K ( H ` X ) Y ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) <-> A. f e. ( A i^i ( K ( H ` X ) Y ) ) f e. U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
334 332 333 sylibr 
 |-  ( ph -> ( A i^i ( K ( H ` X ) Y ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
335 eqidd 
 |-  ( j e. NN -> ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) = ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) )
336 2fveq3 
 |-  ( l = j -> ( ( T ` Y ) ` ( D ` l ) ) = ( ( T ` Y ) ` ( D ` j ) ) )
337 336 adantl 
 |-  ( ( j e. NN /\ l = j ) -> ( ( T ` Y ) ` ( D ` l ) ) = ( ( T ` Y ) ` ( D ` j ) ) )
338 id 
 |-  ( j e. NN -> j e. NN )
339 fvexd 
 |-  ( j e. NN -> ( ( T ` Y ) ` ( D ` j ) ) e. _V )
340 335 337 338 339 fvmptd 
 |-  ( j e. NN -> ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) = ( ( T ` Y ) ` ( D ` j ) ) )
341 340 fveq1d 
 |-  ( j e. NN -> ( ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ` k ) = ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
342 341 oveq2d 
 |-  ( j e. NN -> ( ( ( C ` j ) ` k ) [,) ( ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
343 342 ixpeq2dv 
 |-  ( j e. NN -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) ) )
344 343 iuneq2i 
 |-  U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ` k ) ) = U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( T ` Y ) ` ( D ` j ) ) ` k ) )
345 334 344 sseqtrrdi 
 |-  ( ph -> ( A i^i ( K ( H ` X ) Y ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ` k ) ) )
346 2 6 127 345 13 ovnlecvr2 
 |-  ( ph -> ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ) ) ) )
347 340 oveq2d 
 |-  ( j e. NN -> ( ( C ` j ) ( L ` X ) ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ) = ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) )
348 347 mpteq2ia 
 |-  ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) )
349 348 fveq2i 
 |-  ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) )
350 349 a1i 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( l e. NN |-> ( ( T ` Y ) ` ( D ` l ) ) ) ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) )
351 346 350 breqtrd 
 |-  ( ph -> ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) )
352 6 ffvelrnda 
 |-  ( ( ph /\ l e. NN ) -> ( C ` l ) e. ( RR ^m X ) )
353 elmapi 
 |-  ( ( C ` l ) e. ( RR ^m X ) -> ( C ` l ) : X --> RR )
354 352 353 syl 
 |-  ( ( ph /\ l e. NN ) -> ( C ` l ) : X --> RR )
355 15 111 112 354 hoidifhspf 
 |-  ( ( ph /\ l e. NN ) -> ( ( S ` Y ) ` ( C ` l ) ) : X --> RR )
356 elmapg 
 |-  ( ( RR e. _V /\ X e. Fin ) -> ( ( ( S ` Y ) ` ( C ` l ) ) e. ( RR ^m X ) <-> ( ( S ` Y ) ` ( C ` l ) ) : X --> RR ) )
357 122 356 syl 
 |-  ( ph -> ( ( ( S ` Y ) ` ( C ` l ) ) e. ( RR ^m X ) <-> ( ( S ` Y ) ` ( C ` l ) ) : X --> RR ) )
358 357 adantr 
 |-  ( ( ph /\ l e. NN ) -> ( ( ( S ` Y ) ` ( C ` l ) ) e. ( RR ^m X ) <-> ( ( S ` Y ) ` ( C ` l ) ) : X --> RR ) )
359 355 358 mpbird 
 |-  ( ( ph /\ l e. NN ) -> ( ( S ` Y ) ` ( C ` l ) ) e. ( RR ^m X ) )
360 359 fmpttd 
 |-  ( ph -> ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) : NN --> ( RR ^m X ) )
361 simpl 
 |-  ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) -> ph )
362 eldifi 
 |-  ( f e. ( A \ ( K ( H ` X ) Y ) ) -> f e. A )
363 362 adantl 
 |-  ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) -> f e. A )
364 361 363 133 syl2anc 
 |-  ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) -> E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
365 140 adantl 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> f Fn X )
366 nfv 
 |-  F/ k ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN )
367 366 145 nfan 
 |-  F/ k ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
368 100 3adant3 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( S ` Y ) ` ( C ` j ) ) : X --> RR )
369 368 148 ffvelrnd 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) e. RR )
370 369 rexrd 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) e. RR* )
371 370 ad5ant135 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) e. RR* )
372 187 adantl3r 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( D ` j ) ` k ) e. RR* )
373 149 3expa 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( C ` j ) ` k ) e. RR )
374 186 3expa 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( D ` j ) ` k ) e. RR* )
375 icossre 
 |-  ( ( ( ( C ` j ) ` k ) e. RR /\ ( ( D ` j ) ` k ) e. RR* ) -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ RR )
376 373 374 375 syl2anc 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ RR )
377 376 adantlr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) C_ RR )
378 377 195 sseldd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) e. RR )
379 378 rexrd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) e. RR* )
380 379 adantl3r 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) e. RR* )
381 41 3adant3 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> Y e. RR )
382 23 3adant3 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> X e. Fin )
383 15 381 382 147 148 hoidifhspval3 
 |-  ( ( ph /\ j e. NN /\ k e. X ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) = if ( k = K , if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) , ( ( C ` j ) ` k ) ) )
384 383 ad5ant134 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ k e. X ) /\ k = K ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) = if ( k = K , if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) , ( ( C ` j ) ` k ) ) )
385 iftrue 
 |-  ( k = K -> if ( k = K , if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) , ( ( C ` j ) ` k ) ) = if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) )
386 385 adantl 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ k e. X ) /\ k = K ) -> if ( k = K , if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) , ( ( C ` j ) ` k ) ) = if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) )
387 384 386 eqtrd 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ k e. X ) /\ k = K ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) = if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) )
388 387 adantllr 
 |-  ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) = if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) )
389 iftrue 
 |-  ( Y <_ ( ( C ` j ) ` k ) -> if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) = ( ( C ` j ) ` k ) )
390 389 adantl 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ Y <_ ( ( C ` j ) ` k ) ) -> if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) = ( ( C ` j ) ` k ) )
391 197 adantl3r 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( C ` j ) ` k ) <_ ( f ` k ) )
392 391 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ Y <_ ( ( C ` j ) ` k ) ) -> ( ( C ` j ) ` k ) <_ ( f ` k ) )
393 390 392 eqbrtrd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ Y <_ ( ( C ` j ) ` k ) ) -> if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) <_ ( f ` k ) )
394 iffalse 
 |-  ( -. Y <_ ( ( C ` j ) ` k ) -> if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) = Y )
395 394 adantl 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ -. Y <_ ( ( C ` j ) ` k ) ) -> if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) = Y )
396 simpl1 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) )
397 simpr 
 |-  ( ( k = K /\ -. Y <_ ( f ` k ) ) -> -. Y <_ ( f ` k ) )
398 fveq2 
 |-  ( k = K -> ( f ` k ) = ( f ` K ) )
399 398 breq2d 
 |-  ( k = K -> ( Y <_ ( f ` k ) <-> Y <_ ( f ` K ) ) )
400 399 notbid 
 |-  ( k = K -> ( -. Y <_ ( f ` k ) <-> -. Y <_ ( f ` K ) ) )
401 400 adantr 
 |-  ( ( k = K /\ -. Y <_ ( f ` k ) ) -> ( -. Y <_ ( f ` k ) <-> -. Y <_ ( f ` K ) ) )
402 397 401 mpbid 
 |-  ( ( k = K /\ -. Y <_ ( f ` k ) ) -> -. Y <_ ( f ` K ) )
403 402 3ad2antl3 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> -. Y <_ ( f ` K ) )
404 398 eqcomd 
 |-  ( k = K -> ( f ` K ) = ( f ` k ) )
405 404 3ad2ant3 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) -> ( f ` K ) = ( f ` k ) )
406 364 adantr 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X ) -> E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
407 id 
 |-  ( ( ph /\ j e. NN ) -> ( ph /\ j e. NN ) )
408 407 ad4ant13 
 |-  ( ( ( ( ph /\ k e. X ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( ph /\ j e. NN ) )
409 simpr 
 |-  ( ( ( ( ph /\ k e. X ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
410 251 ad2antrr 
 |-  ( ( ( ( ph /\ k e. X ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> k e. X )
411 408 409 410 378 syl21anc 
 |-  ( ( ( ( ph /\ k e. X ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( f ` k ) e. RR )
412 411 rexlimdva2 
 |-  ( ( ph /\ k e. X ) -> ( E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> ( f ` k ) e. RR ) )
413 412 adantlr 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X ) -> ( E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> ( f ` k ) e. RR ) )
414 406 413 mpd 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X ) -> ( f ` k ) e. RR )
415 414 3adant3 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) -> ( f ` k ) e. RR )
416 405 415 eqeltrd 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) -> ( f ` K ) e. RR )
417 416 adantr 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> ( f ` K ) e. RR )
418 396 361 4 3syl 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> Y e. RR )
419 417 418 ltnled 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> ( ( f ` K ) < Y <-> -. Y <_ ( f ` K ) ) )
420 403 419 mpbird 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> ( f ` K ) < Y )
421 365 364 r19.29a 
 |-  ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) -> f Fn X )
422 421 adantr 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) -> f Fn X )
423 274 a1i 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ k = K ) -> -oo e. RR* )
424 276 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ k = K ) -> Y e. RR* )
425 414 ad4ant13 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ k = K ) -> ( f ` k ) e. RR )
426 425 mnfltd 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ k = K ) -> -oo < ( f ` k ) )
427 398 adantl 
 |-  ( ( ( f ` K ) < Y /\ k = K ) -> ( f ` k ) = ( f ` K ) )
428 simpl 
 |-  ( ( ( f ` K ) < Y /\ k = K ) -> ( f ` K ) < Y )
429 427 428 eqbrtrd 
 |-  ( ( ( f ` K ) < Y /\ k = K ) -> ( f ` k ) < Y )
430 429 ad4ant24 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ k = K ) -> ( f ` k ) < Y )
431 423 424 425 426 430 eliood 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ k = K ) -> ( f ` k ) e. ( -oo (,) Y ) )
432 156 eqcomd 
 |-  ( k = K -> ( -oo (,) Y ) = if ( k = K , ( -oo (,) Y ) , RR ) )
433 432 adantl 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ k = K ) -> ( -oo (,) Y ) = if ( k = K , ( -oo (,) Y ) , RR ) )
434 431 433 eleqtrd 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ k = K ) -> ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
435 414 ad4ant13 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ -. k = K ) -> ( f ` k ) e. RR )
436 160 eqcomd 
 |-  ( -. k = K -> RR = if ( k = K , ( -oo (,) Y ) , RR ) )
437 436 adantl 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ -. k = K ) -> RR = if ( k = K , ( -oo (,) Y ) , RR ) )
438 435 437 eleqtrd 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) /\ -. k = K ) -> ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
439 434 438 pm2.61dan 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) /\ k e. X ) -> ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
440 439 ralrimiva 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) -> A. k e. X ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) )
441 422 440 jca 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ ( f ` K ) < Y ) -> ( f Fn X /\ A. k e. X ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) ) )
442 396 420 441 syl2anc 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> ( f Fn X /\ A. k e. X ( f ` k ) e. if ( k = K , ( -oo (,) Y ) , RR ) ) )
443 442 172 sylibr 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> f e. X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) )
444 166 eqcomd 
 |-  ( ph -> X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) = ( K ( H ` X ) Y ) )
445 444 ad2antrr 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ -. Y <_ ( f ` k ) ) -> X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) = ( K ( H ` X ) Y ) )
446 445 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> X_ k e. X if ( k = K , ( -oo (,) Y ) , RR ) = ( K ( H ` X ) Y ) )
447 443 446 eleqtrd 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> f e. ( K ( H ` X ) Y ) )
448 eldifn 
 |-  ( f e. ( A \ ( K ( H ` X ) Y ) ) -> -. f e. ( K ( H ` X ) Y ) )
449 448 adantl 
 |-  ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) -> -. f e. ( K ( H ` X ) Y ) )
450 449 3ad2ant1 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) -> -. f e. ( K ( H ` X ) Y ) )
451 450 adantr 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) /\ -. Y <_ ( f ` k ) ) -> -. f e. ( K ( H ` X ) Y ) )
452 447 451 condan 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ k e. X /\ k = K ) -> Y <_ ( f ` k ) )
453 452 ad5ant145 
 |-  ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) -> Y <_ ( f ` k ) )
454 453 adantr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ -. Y <_ ( ( C ` j ) ` k ) ) -> Y <_ ( f ` k ) )
455 395 454 eqbrtrd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) /\ -. Y <_ ( ( C ` j ) ` k ) ) -> if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) <_ ( f ` k ) )
456 393 455 pm2.61dan 
 |-  ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) -> if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) <_ ( f ` k ) )
457 388 456 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ k = K ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) <_ ( f ` k ) )
458 383 ad5ant124 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) = if ( k = K , if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) , ( ( C ` j ) ` k ) ) )
459 iffalse 
 |-  ( -. k = K -> if ( k = K , if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) , ( ( C ` j ) ` k ) ) = ( ( C ` j ) ` k ) )
460 459 adantl 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> if ( k = K , if ( Y <_ ( ( C ` j ) ` k ) , ( ( C ` j ) ` k ) , Y ) , ( ( C ` j ) ` k ) ) = ( ( C ` j ) ` k ) )
461 458 460 eqtrd 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) = ( ( C ` j ) ` k ) )
462 197 adantr 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> ( ( C ` j ) ` k ) <_ ( f ` k ) )
463 461 462 eqbrtrd 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) <_ ( f ` k ) )
464 463 adantl4r 
 |-  ( ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) /\ -. k = K ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) <_ ( f ` k ) )
465 457 464 pm2.61dan 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) <_ ( f ` k ) )
466 200 adantl3r 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) < ( ( D ` j ) ` k ) )
467 371 372 380 465 466 elicod 
 |-  ( ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. X ) -> ( f ` k ) e. ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) )
468 467 ex 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( k e. X -> ( f ` k ) e. ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
469 367 468 ralrimi 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> A. k e. X ( f ` k ) e. ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) )
470 365 469 jca 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( f Fn X /\ A. k e. X ( f ` k ) e. ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
471 171 elixp 
 |-  ( f e. X_ k e. X ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> ( f Fn X /\ A. k e. X ( f ` k ) e. ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
472 470 471 sylibr 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> f e. X_ k e. X ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) )
473 eqidd 
 |-  ( j e. NN -> ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) = ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) )
474 2fveq3 
 |-  ( l = j -> ( ( S ` Y ) ` ( C ` l ) ) = ( ( S ` Y ) ` ( C ` j ) ) )
475 474 adantl 
 |-  ( ( j e. NN /\ l = j ) -> ( ( S ` Y ) ` ( C ` l ) ) = ( ( S ` Y ) ` ( C ` j ) ) )
476 fvexd 
 |-  ( j e. NN -> ( ( S ` Y ) ` ( C ` j ) ) e. _V )
477 473 475 338 476 fvmptd 
 |-  ( j e. NN -> ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) = ( ( S ` Y ) ` ( C ` j ) ) )
478 477 fveq1d 
 |-  ( j e. NN -> ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) = ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) )
479 478 oveq1d 
 |-  ( j e. NN -> ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) )
480 479 ixpeq2dv 
 |-  ( j e. NN -> X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = X_ k e. X ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) )
481 480 ad2antlr 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = X_ k e. X ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) )
482 481 eleq2d 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( f e. X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> f e. X_ k e. X ( ( ( ( S ` Y ) ` ( C ` j ) ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
483 472 482 mpbird 
 |-  ( ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) /\ f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> f e. X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
484 483 ex 
 |-  ( ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) /\ j e. NN ) -> ( f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> f e. X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
485 484 reximdva 
 |-  ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) -> ( E. j e. NN f e. X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> E. j e. NN f e. X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
486 364 485 mpd 
 |-  ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) -> E. j e. NN f e. X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
487 eliun 
 |-  ( f e. U_ j e. NN X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> E. j e. NN f e. X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
488 486 487 sylibr 
 |-  ( ( ph /\ f e. ( A \ ( K ( H ` X ) Y ) ) ) -> f e. U_ j e. NN X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
489 488 ralrimiva 
 |-  ( ph -> A. f e. ( A \ ( K ( H ` X ) Y ) ) f e. U_ j e. NN X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
490 dfss3 
 |-  ( ( A \ ( K ( H ` X ) Y ) ) C_ U_ j e. NN X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> A. f e. ( A \ ( K ( H ` X ) Y ) ) f e. U_ j e. NN X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
491 489 490 sylibr 
 |-  ( ph -> ( A \ ( K ( H ` X ) Y ) ) C_ U_ j e. NN X_ k e. X ( ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
492 2 360 7 491 13 ovnlecvr2 
 |-  ( ph -> ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ( L ` X ) ( D ` j ) ) ) ) )
493 477 oveq1d 
 |-  ( j e. NN -> ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ( L ` X ) ( D ` j ) ) = ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) )
494 493 mpteq2ia 
 |-  ( j e. NN |-> ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ( L ` X ) ( D ` j ) ) ) = ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) )
495 494 fveq2i 
 |-  ( sum^ ` ( j e. NN |-> ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) )
496 495 a1i 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( ( l e. NN |-> ( ( S ` Y ) ` ( C ` l ) ) ) ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) )
497 492 496 breqtrd 
 |-  ( ph -> ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) )
498 11 12 99 110 351 497 leadd12dd 
 |-  ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) ) )
499 23 107 41 26 29 13 14 15 hspmbllem1 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) = ( ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) +e ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) )
500 499 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) = ( j e. NN |-> ( ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) +e ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) )
501 500 fveq2d 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) +e ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) ) )
502 19 21 44 106 sge0xadd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) +e ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) ) = ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) +e ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) ) )
503 99 110 rexaddd 
 |-  ( ph -> ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) +e ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) ) = ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) ) )
504 501 502 503 3eqtrrd 
 |-  ( ph -> ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( ( T ` Y ) ` ( D ` j ) ) ) ) ) + ( sum^ ` ( j e. NN |-> ( ( ( S ` Y ) ` ( C ` j ) ) ( L ` X ) ( D ` j ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
505 498 504 breqtrd 
 |-  ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
506 16 40 18 505 39 letrd 
 |-  ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + E ) )