:: BHSP_7 semantic presentation
E1:
for b1, b2, b3, b4 being Real holds
not ( abs (b1 - b2) < b4 / 2 & abs (b2 - b3) < b4 / 2 & not abs (b1 - b3) < b4 )
E2:
for b1 being real number holds
not ( b1 > 0 & for b2 being Nat holds not 1 / (b2 + 1) < b1 )
E3:
for b1 being real number
for b2 being Nat holds
not ( b1 > 0 & for b3 being Nat holds
not ( 1 / (b3 + 1) < b1 & b3 >= b2 ) )
theorem E4: :: BHSP_7:1
proof
let c
1 be
RealUnitarySpace;
let c
2 be
Subset of c
1;
let c
3 be
Functional of c
1;
thus
( c
2 is_summable_set_by c
3 implies for b
1 being
Real holds
not ( 0
< b
1 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( not b
3 is
empty & b
3 c= c
2 & b
2 misses b
3 & not
abs (setopfunc b3,the carrier of c1,REAL ,c3,addreal ) < b
1 ) ) ) )
proof
assume
c
2 is_summable_set_by c
3
;
then consider c
4 being
Real such that
E5:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( b
2 c= b
3 & b
3 c= c
2 & not
abs (c4 - (setopfunc b3,the carrier of c1,REAL ,c3,addreal )) < b
1 ) ) )
by BHSP_6:def 6;
for b
1 being
Real holds
not ( 0
< b
1 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( not b
3 is
empty & b
3 c= c
2 & b
2 misses b
3 & not
abs (setopfunc b3,the carrier of c1,REAL ,c3,addreal ) < b
1 ) ) )
proof
let c
5 be
Real;
assume E6:
0
< c
5
;
0
< c
5 / 2
by E6, XREAL_1:141;
then consider c
6 being
finite Subset of c
1 such that
E7:
( not c
6 is
empty & c
6 c= c
2 & for b
1 being
finite Subset of c
1 holds
not ( c
6 c= b
1 & b
1 c= c
2 & not
abs (c4 - (setopfunc b1,the carrier of c1,REAL ,c3,addreal )) < c
5 / 2 ) )
by E5;
for b
1 being
finite Subset of c
1 holds
not ( not b
1 is
empty & b
1 c= c
2 & c
6 misses b
1 & not
abs (setopfunc b1,the carrier of c1,REAL ,c3,addreal ) < c
5 )
proof
let c
7 be
finite Subset of c
1;
assume E8:
( not c
7 is
empty & c
7 c= c
2 & c
6 misses c
7 )
;
set c
8 = c
6 \/ c
7;
( c
6 \/ c
7 = c
6 \/ c
7 & c
6 c= c
6 \/ c
7 & c
6 \/ c
7 c= c
2 & c
6 \/ c
7 is
finite Subset of c
1 )
by E7, E8, XBOOLE_1:7, XBOOLE_1:8;
then
abs (c4 - (setopfunc (c6 \/ c7),the carrier of c1,REAL ,c3,addreal )) < c
5 / 2
by E7;
then E9:
abs ((setopfunc (c6 \/ c7),the carrier of c1,REAL ,c3,addreal ) - c4) < c
5 / 2
by UNIFORM1:13;
E10:
abs (c4 - (setopfunc c6,the carrier of c1,REAL ,c3,addreal )) < c
5 / 2
by E7;
dom c
3 = the
carrier of c
1
by FUNCT_2:def 1;
then setopfunc (c6 \/ c7),the
carrier of c
1,
REAL ,c
3,
addreal =
addreal . (setopfunc c6,the carrier of c1,REAL ,c3,addreal ),
(setopfunc c7,the carrier of c1,REAL ,c3,addreal )
by E8, BHSP_5:14
.=
(setopfunc c6,the carrier of c1,REAL ,c3,addreal ) + (setopfunc c7,the carrier of c1,REAL ,c3,addreal )
by BINOP_2:def 9
;
then
setopfunc c
7,the
carrier of c
1,
REAL ,c
3,
addreal = (setopfunc (c6 \/ c7),the carrier of c1,REAL ,c3,addreal ) - (setopfunc c6,the carrier of c1,REAL ,c3,addreal )
;
hence
abs (setopfunc c7,the carrier of c1,REAL ,c3,addreal ) < c
5
by E9, E10, E1;
end;
hence
ex b
1 being
finite Subset of c
1 st
( not b
1 is
empty & b
1 c= c
2 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & b
1 misses b
2 & not
abs (setopfunc b2,the carrier of c1,REAL ,c3,addreal ) < c
5 ) )
by E7;
end;
hence
for b
1 being
Real holds
not ( 0
< b
1 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( not b
3 is
empty & b
3 c= c
2 & b
2 misses b
3 & not
abs (setopfunc b3,the carrier of c1,REAL ,c3,addreal ) < b
1 ) ) )
;
end;
assume E5:
for b
1 being
Real holds
not ( 0
< b
1 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( not b
3 is
empty & b
3 c= c
2 & b
2 misses b
3 & not
abs (setopfunc b3,the carrier of c1,REAL ,c3,addreal ) < b
1 ) ) )
;
ex b
1 being
Real st
for b
2 being
Real holds
not ( 0
< b
2 & for b
3 being
finite Subset of c
1 holds
not ( not b
3 is
empty & b
3 c= c
2 & for b
4 being
finite Subset of c
1 holds
not ( b
3 c= b
4 & b
4 c= c
2 & not
abs (b1 - (setopfunc b4,the carrier of c1,REAL ,c3,addreal )) < b
2 ) ) )
proof
defpred S
1[
set ,
set ] means ( a
2 is
finite Subset of c
1 & not a
2 is
empty & a
2 c= c
2 & for b
1 being
Real holds
( b
1 = a
1 implies for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & a
2 misses b
2 & not
abs (setopfunc b2,the carrier of c1,REAL ,c3,addreal ) < 1
/ (b1 + 1) ) ) );
E6:
ex b
1 being
Function of
NAT ,
bool c
2 st
for b
2 being
set holds
( b
2 in NAT implies S
1[b
2,b
1 . b
2] )
proof
now
let c
4 be
set ;
assume E7:
c
4 in NAT
;
reconsider c
5 = c
4 as
Nat by E7;
reconsider c
6 = 1
/ (c5 + 1) as
Real ;
0
<= c
5
by NAT_1:18;
then
0
< c
5 + 1
by NAT_1:38;
then
0
/ (c5 + 1) < 1
/ (c5 + 1)
by REAL_1:73;
then consider c
7 being
finite Subset of c
1 such that
E8:
( not c
7 is
empty & c
7 c= c
2 & for b
1 being
finite Subset of c
1 holds
not ( not b
1 is
empty & b
1 c= c
2 & c
7 misses b
1 & not
abs (setopfunc b1,the carrier of c1,REAL ,c3,addreal ) < c
6 ) )
by E5;
E9:
c
7 in bool c
2
by E8, ZFMISC_1:def 1;
for b
1 being
Real holds
( b
1 = c
4 implies for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & c
7 misses b
2 & not
abs (setopfunc b2,the carrier of c1,REAL ,c3,addreal ) < 1
/ (b1 + 1) ) )
by E8;
hence
ex b
1 being
set st
( b
1 in bool c
2 & b
1 is
finite Subset of c
1 & not b
1 is
empty & b
1 c= c
2 & for b
2 being
Real holds
( b
2 = c
4 implies for b
3 being
finite Subset of c
1 holds
not ( not b
3 is
empty & b
3 c= c
2 & b
1 misses b
3 & not
abs (setopfunc b3,the carrier of c1,REAL ,c3,addreal ) < 1
/ (b2 + 1) ) ) )
by E8, E9;
end;
then E7:
for b
1 being
set holds
not ( b
1 in NAT & for b
2 being
set holds
not ( b
2 in bool c
2 & S
1[b
1,b
2] ) )
;
thus
ex b
1 being
Function of
NAT ,
bool c
2 st
for b
2 being
set holds
( b
2 in NAT implies S
1[b
2,b
1 . b
2] )
from FUNCT_2:sch 1(E7);
end;
ex b
1 being
Function of
NAT ,
bool c
2 st
for b
2 being
Nat holds
( b
1 . b
2 is
finite Subset of c
1 & not b
1 . b
2 is
empty & b
1 . b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( not b
3 is
empty & b
3 c= c
2 & b
1 . b
2 misses b
3 & not
abs (setopfunc b3,the carrier of c1,REAL ,c3,addreal ) < 1
/ (b2 + 1) ) & for b
3 being
Nat holds
( b
2 <= b
3 implies b
1 . b
2 c= b
1 . b
3 ) )
proof
consider c
4 being
Function of
NAT ,
bool c
2 such that
E7:
for b
1 being
set holds
( b
1 in NAT implies ( c
4 . b
1 is
finite Subset of c
1 & not c
4 . b
1 is
empty & c
4 . b
1 c= c
2 & for b
2 being
Real holds
( b
2 = b
1 implies for b
3 being
finite Subset of c
1 holds
not ( not b
3 is
empty & b
3 c= c
2 & c
4 . b
1 misses b
3 & not
abs (setopfunc b3,the carrier of c1,REAL ,c3,addreal ) < 1
/ (b2 + 1) ) ) ) )
by E6;
deffunc H
1(
Nat,
set )
-> set =
(c4 . (a1 + 1)) \/ a
2;
ex b
1 being
Function st
(
dom b
1 = NAT & b
1 . 0
= c
4 . 0 & for b
2 being
Element of
NAT holds b
1 . (b2 + 1) = H
1(b
2,b
1 . b
2) )
from RECDEF_1:sch 3();
then consider c
5 being
Function such that
E8:
(
dom c
5 = NAT & c
5 . 0
= c
4 . 0 & for b
1 being
Element of
NAT holds c
5 . (b1 + 1) = (c4 . (b1 + 1)) \/ (c5 . b1) )
;
defpred S
2[
Nat] means ( c
5 . a
1 is
finite Subset of c
1 & not c
5 . a
1 is
empty & c
5 . a
1 c= c
2 & for b
1 being
finite Subset of c
1 holds
not ( not b
1 is
empty & b
1 c= c
2 & c
5 . a
1 misses b
1 & not
abs (setopfunc b1,the carrier of c1,REAL ,c3,addreal ) < 1
/ (a1 + 1) ) & for b
1 being
Nat holds
( a
1 <= b
1 implies c
5 . a
1 c= c
5 . b
1 ) );
for b
1 being
Nat holds
( b
1 = 0 implies for b
2 being
Nat holds
( b
1 <= b
2 implies c
5 . b
1 c= c
5 . b
2 ) )
proof
let c
6 be
Nat;
assume E9:
c
6 = 0
;
defpred S
3[
Nat] means ( c
6 <= a
1 implies c
5 . c
6 c= c
5 . a
1 );
E10:
S
3[0]
by E9;
thus
for b
1 being
Nat holds
S
3[b
1]
from NAT_1:sch 1(E10, E11);
end;
then E9:
S
2[0]
by E7, E8;
E10:
now
let c
6 be
Nat;
assume E11:
S
2[c
6]
;
E12:
c
5 . (c6 + 1) = (c4 . (c6 + 1)) \/ (c5 . c6)
by E8;
E13:
c
4 . (c6 + 1) is
finite Subset of c
1
by E7;
E14:
ex b
1 being
set st b
1 in c
5 . c
6
by E11, XBOOLE_0:def 1;
E15:
for b
1 being
finite Subset of c
1 holds
not ( not b
1 is
empty & b
1 c= c
2 & c
5 . (c6 + 1) misses b
1 & not
abs (setopfunc b1,the carrier of c1,REAL ,c3,addreal ) < 1
/ ((c6 + 1) + 1) )
defpred S
3[
Nat] means ( c
6 + 1
<= a
1 implies c
5 . (c6 + 1) c= c
5 . a
1 );
for b
1 being
Nat holds
S
3[b
1]
proof
E16:
S
3[0]
by NAT_1:19;
E17:
for b
1 being
Nat holds
( S
3[b
1] implies S
3[b
1 + 1] )
proof
let c
7 be
Nat;
assume that
E18:
S
3[c
7]
and
E19:
c
6 + 1
<= c
7 + 1
;
now
per cases
not ( not c
6 = c
7 & not c
6 <> c
7 )
;
case
c
6 = c
7
;
hence
c
5 . (c6 + 1) c= c
5 . (c7 + 1)
;
end;
case E20:
c
6 <> c
7
;
end;
end;
hence
c
5 . (c6 + 1) c= c
5 . (c7 + 1)
;
end;
thus
for b
1 being
Nat holds
S
3[b
1]
from NAT_1:sch 1(E16, E17);
end;
hence
S
2[c
6 + 1]
by E11, E12, E13, E14, E15, FINSET_1:14, XBOOLE_0:def 2, XBOOLE_1:8;
end;
E11:
for b
1 being
Nat holds
S
2[b
1]
from NAT_1:sch 1(E9, E10);
rng c
5 c= bool c
2
then
c
5 is
Function of
NAT ,
bool c
2
by E8, FUNCT_2:4;
hence
ex b
1 being
Function of
NAT ,
bool c
2 st
for b
2 being
Nat holds
( b
1 . b
2 is
finite Subset of c
1 & not b
1 . b
2 is
empty & b
1 . b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( not b
3 is
empty & b
3 c= c
2 & b
1 . b
2 misses b
3 & not
abs (setopfunc b3,the carrier of c1,REAL ,c3,addreal ) < 1
/ (b2 + 1) ) & for b
3 being
Nat holds
( b
2 <= b
3 implies b
1 . b
2 c= b
1 . b
3 ) )
by E11;
end;
then consider c
4 being
Function of
NAT ,
bool c
2 such that
E7:
for b
1 being
Nat holds
( c
4 . b
1 is
finite Subset of c
1 & not c
4 . b
1 is
empty & c
4 . b
1 c= c
2 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & c
4 . b
1 misses b
2 & not
abs (setopfunc b2,the carrier of c1,REAL ,c3,addreal ) < 1
/ (b1 + 1) ) & for b
2 being
Nat holds
( b
1 <= b
2 implies c
4 . b
1 c= c
4 . b
2 ) )
;
defpred S
2[
set ,
set ] means ex b
1 being
finite Subset of c
1 st
( not b
1 is
empty & c
4 . a
1 = b
1 & a
2 = setopfunc b
1,the
carrier of c
1,
REAL ,c
3,
addreal );
E8:
for b
1 being
set holds
not ( b
1 in NAT & for b
2 being
set holds
not ( b
2 in REAL & S
2[b
1,b
2] ) )
proof
let c
5 be
set ;
assume E9:
c
5 in NAT
;
reconsider c
6 = c
5 as
Nat by E9;
E10:
( c
4 . c
6 is
finite Subset of c
1 & not c
4 . c
6 is
empty & c
4 . c
6 c= c
2 & for b
1 being
finite Subset of c
1 holds
not ( not b
1 is
empty & b
1 c= c
2 & c
4 . c
5 misses b
1 & not
abs (setopfunc b1,the carrier of c1,REAL ,c3,addreal ) < 1
/ (c6 + 1) ) & for b
1 being
Nat holds
( c
6 <= b
1 implies c
4 . c
6 c= c
4 . b
1 ) )
by E7;
then reconsider c
7 = c
4 . c
5 as
finite Subset of c
1 ;
reconsider c
8 =
setopfunc c
7,the
carrier of c
1,
REAL ,c
3,
addreal as
set ;
ex b
1 being
finite Subset of c
1 st
( not b
1 is
empty & c
4 . c
5 = b
1 & c
8 = setopfunc b
1,the
carrier of c
1,
REAL ,c
3,
addreal )
by E10;
hence
ex b
1 being
set st
( b
1 in REAL & S
2[c
5,b
1] )
;
end;
ex b
1 being
Function of
NAT ,
REAL st
for b
2 being
set holds
( b
2 in NAT implies S
2[b
2,b
1 . b
2] )
from FUNCT_2:sch 1(E8);
then consider c
5 being
Function of
NAT ,
REAL such that
E9:
for b
1 being
set holds
not ( b
1 in NAT & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & c
4 . b
1 = b
2 & c
5 . b
1 = setopfunc b
2,the
carrier of c
1,
REAL ,c
3,
addreal ) )
;
set c
6 = c
5;
E10:
for b
1 being
real number holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3, b
4 being
Nat st
( b
3 >= b
2 & b
4 >= b
2 & not
abs ((c5 . b3) - (c5 . b4)) < b
1 ) )
proof
let c
7 be
real number ;
assume E11:
c
7 > 0
;
E12:
c
7 / 2
> 0
/ 2
by E11, REAL_1:73;
then consider c
8 being
Nat such that
E13:
1
/ (c8 + 1) < c
7 / 2
by E2;
take
c
8
;
let c
9, c
10 be
Nat;
assume E14:
( c
9 >= c
8 & c
10 >= c
8 )
;
consider c
11 being
finite Subset of c
1 such that
E15:
( not c
11 is
empty & c
4 . c
8 = c
11 & c
5 . c
8 = setopfunc c
11,the
carrier of c
1,
REAL ,c
3,
addreal )
by E9;
consider c
12 being
finite Subset of c
1 such that
E16:
( not c
12 is
empty & c
4 . c
9 = c
12 & c
5 . c
9 = setopfunc c
12,the
carrier of c
1,
REAL ,c
3,
addreal )
by E9;
consider c
13 being
finite Subset of c
1 such that
E17:
( not c
13 is
empty & c
4 . c
10 = c
13 & c
5 . c
10 = setopfunc c
13,the
carrier of c
1,
REAL ,c
3,
addreal )
by E9;
E18:
c
11 c= c
12
by E7, E14, E15, E16;
E19:
c
11 c= c
13
by E7, E14, E15, E17;
now
per cases
not ( not c
11 = c
12 & not c
11 <> c
12 )
;
case E20:
c
11 = c
12
;
now
per cases
not ( not c
11 = c
13 & not c
11 <> c
13 )
;
case E21:
c
11 <> c
13
;
ex b
1 being
finite Subset of c
1 st
( not b
1 is
empty & b
1 c= c
2 & b
1 misses c
11 & c
11 \/ b
1 = c
13 )
then consider c
14 being
finite Subset of c
1 such that
E22:
( not c
14 is
empty & c
14 c= c
2 & c
14 misses c
11 & c
11 \/ c
14 = c
13 )
;
dom c
3 = the
carrier of c
1
by FUNCT_2:def 1;
then E23:
setopfunc c
13,the
carrier of c
1,
REAL ,c
3,
addreal =
addreal . (setopfunc c11,the carrier of c1,REAL ,c3,addreal ),
(setopfunc c14,the carrier of c1,REAL ,c3,addreal )
by E22, BHSP_5:14
.=
(setopfunc c11,the carrier of c1,REAL ,c3,addreal ) + (setopfunc c14,the carrier of c1,REAL ,c3,addreal )
by BINOP_2:def 9
;
abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal ) < 1
/ (c8 + 1)
by E7, E15, E22;
then E24:
abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal ) < c
7 / 2
by E13, XREAL_1:2;
E25:
abs ((c5 . c9) - (c5 . c10)) =
abs (- (setopfunc c14,the carrier of c1,REAL ,c3,addreal ))
by E16, E17, E20, E23
.=
abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal )
by COMPLEX1:138
;
c
7 / 2
< c
7
by E11, XREAL_1:218;
hence
abs ((c5 . c9) - (c5 . c10)) < c
7
by E24, E25, XREAL_1:2;
end;
hence
abs ((c5 . c9) - (c5 . c10)) < c
7
;
end;
case E20:
c
11 <> c
12
;
now
per cases
not ( not c
11 = c
13 & not c
11 <> c
13 )
;
case E21:
c
11 = c
13
;
ex b
1 being
finite Subset of c
1 st
( not b
1 is
empty & b
1 c= c
2 & b
1 misses c
11 & c
11 \/ b
1 = c
12 )
then consider c
14 being
finite Subset of c
1 such that
E22:
( not c
14 is
empty & c
14 c= c
2 & c
14 misses c
11 & c
11 \/ c
14 = c
12 )
;
dom c
3 = the
carrier of c
1
by FUNCT_2:def 1;
then E23:
setopfunc c
12,the
carrier of c
1,
REAL ,c
3,
addreal =
addreal . (setopfunc c11,the carrier of c1,REAL ,c3,addreal ),
(setopfunc c14,the carrier of c1,REAL ,c3,addreal )
by E22, BHSP_5:14
.=
(setopfunc c11,the carrier of c1,REAL ,c3,addreal ) + (setopfunc c14,the carrier of c1,REAL ,c3,addreal )
by BINOP_2:def 9
;
abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal ) < 1
/ (c8 + 1)
by E7, E15, E22;
then
abs ((c5 . c9) - (c5 . c10)) < c
7 / 2
by E13, E16, E17, E21, E23, XREAL_1:2;
then
(abs ((c5 . c9) - (c5 . c10))) + 0
< (c7 / 2) + (c7 / 2)
by E12, XREAL_1:10;
hence
abs ((c5 . c9) - (c5 . c10)) < c
7
;
case E21:
c
11 <> c
13
;
ex b
1 being
finite Subset of c
1 st
( not b
1 is
empty & b
1 c= c
2 & b
1 misses c
11 & c
11 \/ b
1 = c
12 )
then consider c
14 being
finite Subset of c
1 such that
E22:
( not c
14 is
empty & c
14 c= c
2 & c
14 misses c
11 & c
11 \/ c
14 = c
12 )
;
ex b
1 being
finite Subset of c
1 st
( not b
1 is
empty & b
1 c= c
2 & b
1 misses c
11 & c
11 \/ b
1 = c
13 )
then consider c
15 being
finite Subset of c
1 such that
E23:
( not c
15 is
empty & c
15 c= c
2 & c
15 misses c
11 & c
11 \/ c
15 = c
13 )
;
abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal ) < 1
/ (c8 + 1)
by E7, E15, E22;
then E24:
abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal ) < c
7 / 2
by E13, XREAL_1:2;
abs (setopfunc c15,the carrier of c1,REAL ,c3,addreal ) < 1
/ (c8 + 1)
by E7, E15, E23;
then
abs (setopfunc c15,the carrier of c1,REAL ,c3,addreal ) < c
7 / 2
by E13, XREAL_1:2;
then E25:
(abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal )) + (abs (setopfunc c15,the carrier of c1,REAL ,c3,addreal )) < (c7 / 2) + (c7 / 2)
by E24, XREAL_1:10;
dom c
3 = the
carrier of c
1
by FUNCT_2:def 1;
then E26:
setopfunc c
12,the
carrier of c
1,
REAL ,c
3,
addreal =
addreal . (setopfunc c11,the carrier of c1,REAL ,c3,addreal ),
(setopfunc c14,the carrier of c1,REAL ,c3,addreal )
by E22, BHSP_5:14
.=
(setopfunc c11,the carrier of c1,REAL ,c3,addreal ) + (setopfunc c14,the carrier of c1,REAL ,c3,addreal )
by BINOP_2:def 9
;
dom c
3 = the
carrier of c
1
by FUNCT_2:def 1;
then E27:
setopfunc c
13,the
carrier of c
1,
REAL ,c
3,
addreal =
addreal . (setopfunc c11,the carrier of c1,REAL ,c3,addreal ),
(setopfunc c15,the carrier of c1,REAL ,c3,addreal )
by E23, BHSP_5:14
.=
(setopfunc c11,the carrier of c1,REAL ,c3,addreal ) + (setopfunc c15,the carrier of c1,REAL ,c3,addreal )
by BINOP_2:def 9
;
(c5 . c9) - (c5 . c10) = (setopfunc c14,the carrier of c1,REAL ,c3,addreal ) - (setopfunc c15,the carrier of c1,REAL ,c3,addreal )
by E16, E17, E26, E27;
then
abs ((c5 . c9) - (c5 . c10)) <= (abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal )) + (abs (setopfunc c15,the carrier of c1,REAL ,c3,addreal ))
by COMPLEX1:143;
hence
abs ((c5 . c9) - (c5 . c10)) < c
7
by E25, XREAL_1:2;
end;
hence
abs ((c5 . c9) - (c5 . c10)) < c
7
;
end;
end;
hence
abs ((c5 . c9) - (c5 . c10)) < c
7
;
end;
for b
1 being
real number holds
not ( 0
< b
1 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
2 <= b
3 & not
abs ((c5 . b3) - (c5 . b2)) < b
1 ) )
proof
let c
7 be
real number ;
assume E11:
0
< c
7
;
consider c
8 being
Nat such that
E12:
for b
1, b
2 being
Nat holds
not ( b
1 >= c
8 & b
2 >= c
8 & not
abs ((c5 . b1) - (c5 . b2)) < c
7 )
by E10, E11;
for b
1 being
Nat holds
not ( c
8 <= b
1 & not
abs ((c5 . b1) - (c5 . c8)) < c
7 )
by E12;
hence
ex b
1 being
Nat st
for b
2 being
Nat holds
not ( b
1 <= b
2 & not
abs ((c5 . b2) - (c5 . b1)) < c
7 )
;
end;
then
c
5 is
convergent
by SEQ_4:58;
then consider c
7 being
real number such that
E11:
for b
1 being
real number holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
abs ((c5 . b3) - c7) < b
1 ) )
by SEQ_2:def 6;
reconsider c
8 = c
7 as
Real by XREAL_0:def 1;
E12:
for b
1 being
Real holds
not ( 0
< b
1 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( b
2 c= b
3 & b
3 c= c
2 & not
abs (c8 - (setopfunc b3,the carrier of c1,REAL ,c3,addreal )) < b
1 ) ) )
proof
let c
9 be
Real;
assume E13:
c
9 > 0
;
E14:
c
9 / 2
> 0
/ 2
by E13, REAL_1:73;
then consider c
10 being
Nat such that
E15:
for b
1 being
Nat holds
not ( b
1 >= c
10 & not
abs ((c5 . b1) - c8) < c
9 / 2 )
by E11;
consider c
11 being
Nat such that
E16:
( 1
/ (c11 + 1) < c
9 / 2 & c
11 >= c
10 )
by E14, E3;
consider c
12 being
finite Subset of c
1 such that
E17:
( not c
12 is
empty & c
4 . c
11 = c
12 & c
5 . c
11 = setopfunc c
12,the
carrier of c
1,
REAL ,c
3,
addreal )
by E9;
E18:
abs ((setopfunc c12,the carrier of c1,REAL ,c3,addreal ) - c8) < c
9 / 2
by E15, E16, E17;
now
let c
13 be
finite Subset of c
1;
assume E19:
( c
12 c= c
13 & c
13 c= c
2 )
;
now
per cases
not ( not c
12 = c
13 & not c
12 <> c
13 )
;
case
c
12 = c
13
;
then
abs (c8 - (setopfunc c13,the carrier of c1,REAL ,c3,addreal )) < c
9 / 2
by E18, UNIFORM1:13;
then
(abs (c7 - (setopfunc c13,the carrier of c1,REAL ,c3,addreal ))) + 0
< (c9 / 2) + (c9 / 2)
by E14, XREAL_1:10;
hence
abs (c8 - (setopfunc c13,the carrier of c1,REAL ,c3,addreal )) < c
9
;
end;
case E20:
c
12 <> c
13
;
ex b
1 being
finite Subset of c
1 st
( not b
1 is
empty & b
1 c= c
2 & c
12 misses b
1 & c
12 \/ b
1 = c
13 )
then consider c
14 being
finite Subset of c
1 such that
E21:
( not c
14 is
empty & c
14 c= c
2 & c
12 misses c
14 & c
12 \/ c
14 = c
13 )
;
abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal ) < 1
/ (c11 + 1)
by E7, E17, E21;
then E22:
abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal ) < c
9 / 2
by E16, XREAL_1:2;
dom c
3 = the
carrier of c
1
by FUNCT_2:def 1;
then (setopfunc c13,the carrier of c1,REAL ,c3,addreal ) - c
8 =
(addreal . (setopfunc c12,the carrier of c1,REAL ,c3,addreal ),(setopfunc c14,the carrier of c1,REAL ,c3,addreal )) - c
8
by E21, BHSP_5:14
.=
((setopfunc c12,the carrier of c1,REAL ,c3,addreal ) + (setopfunc c14,the carrier of c1,REAL ,c3,addreal )) - c
8
by BINOP_2:def 9
.=
((setopfunc c12,the carrier of c1,REAL ,c3,addreal ) - c8) + (setopfunc c14,the carrier of c1,REAL ,c3,addreal )
;
then
abs ((setopfunc c13,the carrier of c1,REAL ,c3,addreal ) - c8) <= (abs ((setopfunc c12,the carrier of c1,REAL ,c3,addreal ) - c8)) + (abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal ))
by ABSVALUE:21;
then E23:
abs (c7 - (setopfunc c13,the carrier of c1,REAL ,c3,addreal )) <= (abs ((setopfunc c12,the carrier of c1,REAL ,c3,addreal ) - c8)) + (abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal ))
by UNIFORM1:13;
(abs ((setopfunc c12,the carrier of c1,REAL ,c3,addreal ) - c8)) + (abs (setopfunc c14,the carrier of c1,REAL ,c3,addreal )) < (c9 / 2) + (c9 / 2)
by E18, E22, XREAL_1:10;
hence
abs (c8 - (setopfunc c13,the carrier of c1,REAL ,c3,addreal )) < c
9
by E23, XREAL_1:2;
end;
hence
abs (c8 - (setopfunc c13,the carrier of c1,REAL ,c3,addreal )) < c
9
;
end;
hence
ex b
1 being
finite Subset of c
1 st
( not b
1 is
empty & b
1 c= c
2 & for b
2 being
finite Subset of c
1 holds
not ( b
1 c= b
2 & b
2 c= c
2 & not
abs (c8 - (setopfunc b2,the carrier of c1,REAL ,c3,addreal )) < c
9 ) )
by E17;
end;
take
c
8
;
thus
for b
1 being
Real holds
not ( 0
< b
1 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( b
2 c= b
3 & b
3 c= c
2 & not
abs (c8 - (setopfunc b3,the carrier of c1,REAL ,c3,addreal )) < b
1 ) ) )
by E12;
end;
hence
c
2 is_summable_set_by c
3
by BHSP_6:def 6;
end;
theorem E5: :: BHSP_7:2
for b
1 being
RealUnitarySpace holds
( ( the
add of b
1 is
commutative & the
add of b
1 is
associative & the
add of b
1 is
has_a_unity ) implies ( for b
2 being
finite OrthogonalFamily of b
1 holds
( not b
2 is
empty implies for b
3 being
Function of the
carrier of b
1,the
carrier of b
1 holds
( ( b
2 c= dom b
3 & for b
4 being
Point of b
1 holds
( b
4 in b
2 implies b
3 . b
4 = b
4 ) ) implies ( for b
4 being
Function of the
carrier of b
1,
REAL holds
( ( b
2 c= dom b
4 & for b
5 being
Point of b
1 holds
( b
5 in b
2 implies b
4 . b
5 = b
5 .|. b
5 ) ) implies (
(setopfunc b2,the carrier of b1,the carrier of b1,b3,the add of b1) .|. (setopfunc b2,the carrier of b1,the carrier of b1,b3,the add of b1) = setopfunc b
2,the
carrier of b
1,
REAL ,b
4,
addreal ) ) ) ) ) ) )