:: BHSP_2 semantic presentation
deffunc H1( RealUnitarySpace) -> Element of the carrier of a1 = 0. a1;
:: deftheorem E1 defines convergent BHSP_2:def 1 :
theorem E2: :: BHSP_2:1
theorem E3: :: BHSP_2:2
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that
E4:
c
2 is
convergent
and
E5:
ex b
1 being
Nat st
for b
2 being
Nat holds
( b
1 <= b
2 implies c
3 . b
2 = c
2 . b
2 )
;
consider c
4 being
Point of c
1 such that
E6:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c2 . b3),c
4 < b
1 ) )
by E4, E1;
consider c
5 being
Nat such that
E7:
for b
1 being
Nat holds
( b
1 >= c
5 implies c
3 . b
1 = c
2 . b
1 )
by E5;
take c
6 = c
4;
:: uses BHSP_2:def 1
let c
7 be
Real;
assume
c
7 > 0
;
then consider c
8 being
Nat such that
E8:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),c
6 < c
7 )
by E6;
E9:
now
assume E10:
c
5 <= c
8
;
take c
9 = c
8;
let c
10 be
Nat;
assume E11:
c
10 >= c
9
;
then
c
10 >= c
5
by E10, XREAL_1:2;
then
c
3 . c
10 = c
2 . c
10
by E7;
hence
dist (c3 . c10),c
6 < c
7
by E8, E11;
end;
now
assume E10:
c
8 <= c
5
;
take c
9 = c
5;
let c
10 be
Nat;
assume E11:
c
10 >= c
9
;
then
c
10 >= c
8
by E10, XREAL_1:2;
then
dist (c2 . c10),c
4 < c
7
by E8;
hence
dist (c3 . c10),c
6 < c
7
by E7, E11;
end;
hence
ex b
1 being
Nat st
for b
2 being
Nat holds
not ( b
2 >= b
1 & not
dist (c3 . b2),c
6 < c
7 )
by E9;
end;
theorem E4: :: BHSP_2:3
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that
E5:
c
2 is
convergent
and
E6:
c
3 is
convergent
;
consider c
4 being
Point of c
1 such that
E7:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c2 . b3),c
4 < b
1 ) )
by E5, E1;
consider c
5 being
Point of c
1 such that
E8:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c3 . b3),c
5 < b
1 ) )
by E6, E1;
take c
6 = c
4 + c
5;
:: uses BHSP_2:def 1
let c
7 be
Real;
assume
c
7 > 0
;
then E9:
c
7 / 2
> 0
by SEQ_2:3;
then consider c
8 being
Nat such that
E10:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),c
4 < c
7 / 2 )
by E7;
consider c
9 being
Nat such that
E11:
for b
1 being
Nat holds
not ( b
1 >= c
9 & not
dist (c3 . b1),c
5 < c
7 / 2 )
by E8, E9;
take c
10 = c
8 + c
9;
let c
11 be
Nat;
assume E12:
c
11 >= c
10
;
c
8 + c
9 >= c
8
by NAT_1:37;
then
c
11 >= c
8
by E12, XREAL_1:2;
then E13:
dist (c2 . c11),c
4 < c
7 / 2
by E10;
c
10 >= c
9
by NAT_1:37;
then
c
11 >= c
9
by E12, XREAL_1:2;
then
dist (c3 . c11),c
5 < c
7 / 2
by E11;
then E14:
(dist (c2 . c11),c4) + (dist (c3 . c11),c5) < (c7 / 2) + (c7 / 2)
by E13, XREAL_1:10;
dist ((c2 + c3) . c11),c
6 = dist ((c2 . c11) + (c3 . c11)),
(c4 + c5)
by NORMSP_1:def 5;
then
dist ((c2 + c3) . c11),c
6 <= (dist (c2 . c11),c4) + (dist (c3 . c11),c5)
by BHSP_1:47;
hence
dist ((c2 + c3) . c11),c
6 < c
7
by E14, XREAL_1:2;
end;
theorem E5: :: BHSP_2:4
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that
E6:
c
2 is
convergent
and
E7:
c
3 is
convergent
;
consider c
4 being
Point of c
1 such that
E8:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c2 . b3),c
4 < b
1 ) )
by E6, E1;
consider c
5 being
Point of c
1 such that
E9:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c3 . b3),c
5 < b
1 ) )
by E7, E1;
take c
6 = c
4 - c
5;
:: uses BHSP_2:def 1
let c
7 be
Real;
assume
c
7 > 0
;
then E10:
c
7 / 2
> 0
by SEQ_2:3;
then consider c
8 being
Nat such that
E11:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),c
4 < c
7 / 2 )
by E8;
consider c
9 being
Nat such that
E12:
for b
1 being
Nat holds
not ( b
1 >= c
9 & not
dist (c3 . b1),c
5 < c
7 / 2 )
by E9, E10;
take c
10 = c
8 + c
9;
let c
11 be
Nat;
assume E13:
c
11 >= c
10
;
c
8 + c
9 >= c
8
by NAT_1:37;
then
c
11 >= c
8
by E13, XREAL_1:2;
then E14:
dist (c2 . c11),c
4 < c
7 / 2
by E11;
c
10 >= c
9
by NAT_1:37;
then
c
11 >= c
9
by E13, XREAL_1:2;
then
dist (c3 . c11),c
5 < c
7 / 2
by E12;
then E15:
(dist (c2 . c11),c4) + (dist (c3 . c11),c5) < (c7 / 2) + (c7 / 2)
by E14, XREAL_1:10;
dist ((c2 - c3) . c11),c
6 = dist ((c2 . c11) - (c3 . c11)),
(c4 - c5)
by NORMSP_1:def 6;
then
dist ((c2 - c3) . c11),c
6 <= (dist (c2 . c11),c4) + (dist (c3 . c11),c5)
by BHSP_1:48;
hence
dist ((c2 - c3) . c11),c
6 < c
7
by E15, XREAL_1:2;
end;
theorem E6: :: BHSP_2:5
proof
let c
1 be
RealUnitarySpace;
let c
2 be
Real;
let c
3 be
sequence of c
1;
assume
c
3 is
convergent
;
then consider c
4 being
Point of c
1 such that
E7:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c3 . b3),c
4 < b
1 ) )
by E1;
take c
5 = c
2 * c
4;
:: uses BHSP_2:def 1
now
assume E9:
c
2 <> 0
;
then E10:
abs c
2 > 0
by COMPLEX1:133;
let c
6 be
Real;
assume E11:
c
6 > 0
;
E12:
abs c
2 <> 0
by E9, COMPLEX1:133;
0
/ (abs c2) = 0
;
then
c
6 / (abs c2) > 0
by E10, E11, REAL_1:73;
then consider c
7 being
Nat such that
E13:
for b
1 being
Nat holds
not ( b
1 >= c
7 & not
dist (c3 . b1),c
4 < c
6 / (abs c2) )
by E7;
take c
8 = c
7;
let c
9 be
Nat;
assume
c
9 >= c
8
;
then E14:
dist (c3 . c9),c
4 < c
6 / (abs c2)
by E13;
E15:
dist (c2 * (c3 . c9)),
(c2 * c4) =
||.((c2 * (c3 . c9)) - (c2 * c4)).||
by BHSP_1:def 5
.=
||.(c2 * ((c3 . c9) - c4)).||
by RLVECT_1:48
.=
(abs c2) * ||.((c3 . c9) - c4).||
by BHSP_1:33
.=
(abs c2) * (dist (c3 . c9),c4)
by BHSP_1:def 5
;
(abs c2) * (c6 / (abs c2)) =
(abs c2) * (((abs c2) " ) * c6)
by XCMPLX_0:def 9
.=
((abs c2) * ((abs c2) " )) * c
6
.=
1
* c
6
by E12, XCMPLX_0:def 7
.=
c
6
;
then
dist (c2 * (c3 . c9)),c
5 < c
6
by E10, E14, E15, XREAL_1:70;
hence
dist ((c2 * c3) . c9),c
5 < c
6
by NORMSP_1:def 8;
end;
hence
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist ((c2 * c3) . b3),c
5 < b
1 ) )
by E8;
end;
theorem E7: :: BHSP_2:6
theorem E8: :: BHSP_2:7
proof
let c
1 be
RealUnitarySpace;
let c
2 be
Point of c
1;
let c
3 be
sequence of c
1;
assume
c
3 is
convergent
;
then consider c
4 being
Point of c
1 such that
E9:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c3 . b3),c
4 < b
1 ) )
by E1;
take
c
4 + c
2
;
:: uses BHSP_2:def 1
let c
5 be
Real;
assume
c
5 > 0
;
then consider c
6 being
Nat such that
E10:
for b
1 being
Nat holds
not ( b
1 >= c
6 & not
dist (c3 . b1),c
4 < c
5 )
by E9;
take c
7 = c
6;
let c
8 be
Nat;
assume
c
8 >= c
7
;
then E11:
dist (c3 . c8),c
4 < c
5
by E10;
dist ((c3 . c8) + c2),
(c4 + c2) <= (dist (c3 . c8),c4) + (dist c2,c2)
by BHSP_1:47;
then
dist ((c3 . c8) + c2),
(c4 + c2) <= (dist (c3 . c8),c4) + 0
by BHSP_1:41;
then
dist ((c3 . c8) + c2),
(c4 + c2) < c
5
by E11, XREAL_1:2;
hence
dist ((c3 + c2) . c8),
(c4 + c2) < c
5
by BHSP_1:def 12;
end;
theorem E9: :: BHSP_2:8
theorem E10: :: BHSP_2:9
proof
let c
1 be
RealUnitarySpace;
let c
2 be
sequence of c
1;
thus
not ( c
2 is
convergent & for b
1 being
Point of c
1 holds
ex b
2 being
Real st
( b
2 > 0 & for b
3 being
Nat holds
ex b
4 being
Nat st
( b
4 >= b
3 & not
||.((c2 . b4) - b1).|| < b
2 ) ) )
proof
assume
c
2 is
convergent
;
then consider c
3 being
Point of c
1 such that
E11:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c2 . b3),c
3 < b
1 ) )
by E1;
take
c
3
;
let c
4 be
Real;
assume
c
4 > 0
;
then consider c
5 being
Nat such that
E12:
for b
1 being
Nat holds
not ( b
1 >= c
5 & not
dist (c2 . b1),c
3 < c
4 )
by E11;
take c
6 = c
5;
let c
7 be
Nat;
assume
c
7 >= c
6
;
then
dist (c2 . c7),c
3 < c
4
by E12;
hence
||.((c2 . c7) - c3).|| < c
4
by BHSP_1:def 5;
end;
( ex b
1 being
Point of c
1 st
for b
2 being
Real holds
not ( b
2 > 0 & for b
3 being
Nat holds
ex b
4 being
Nat st
( b
4 >= b
3 & not
||.((c2 . b4) - b1).|| < b
2 ) ) implies c
2 is
convergent )
proof
given c
3 being
Point of c
1 such that
E11:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
||.((c2 . b3) - c3).|| < b
1 ) )
;
take
c
3
;
:: uses BHSP_2:def 1
let c
4 be
Real;
assume
c
4 > 0
;
then consider c
5 being
Nat such that
E12:
for b
1 being
Nat holds
not ( b
1 >= c
5 & not
||.((c2 . b1) - c3).|| < c
4 )
by E11;
take c
6 = c
5;
let c
7 be
Nat;
assume
c
7 >= c
6
;
then
||.((c2 . c7) - c3).|| < c
4
by E12;
hence
dist (c2 . c7),c
3 < c
4
by BHSP_1:def 5;
end;
hence
( ex b
1 being
Point of c
1 st
for b
2 being
Real holds
not ( b
2 > 0 & for b
3 being
Nat holds
ex b
4 being
Nat st
( b
4 >= b
3 & not
||.((c2 . b4) - b1).|| < b
2 ) ) implies c
2 is
convergent )
;
end;
definition
let c
1 be
RealUnitarySpace;
let c
2 be
sequence of c
1;
assume E11:
c
2 is
convergent
;
func lim a
2 -> Point of a
1 means :
E11:
:: BHSP_2:def 2
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (a2 . b3),a
3 < b
1 ) );
existence
ex b1 being Point of c1 st
for b2 being Real holds
not ( b2 > 0 & for b3 being Nat holds
ex b4 being Nat st
( b4 >= b3 & not dist (c2 . b4),b1 < b2 ) )
by E11, E1;
uniqueness
for b1, b2 being Point of c1 holds
( ( for b3 being Real holds
not ( b3 > 0 & for b4 being Nat holds
ex b5 being Nat st
( b5 >= b4 & not dist (c2 . b5),b1 < b3 ) ) & for b3 being Real holds
not ( b3 > 0 & for b4 being Nat holds
ex b5 being Nat st
( b5 >= b4 & not dist (c2 . b5),b2 < b3 ) ) ) implies ( b1 = b2 ) )
proof
for b
1, b
2 being
Point of c
1 holds
( ( for b
3 being
Real holds
not ( b
3 > 0 & for b
4 being
Nat holds
ex b
5 being
Nat st
( b
5 >= b
4 & not
dist (c2 . b5),b
1 < b
3 ) ) & for b
3 being
Real holds
not ( b
3 > 0 & for b
4 being
Nat holds
ex b
5 being
Nat st
( b
5 >= b
4 & not
dist (c2 . b5),b
2 < b
3 ) ) ) implies ( b
1 = b
2 ) )
proof
given c
3, c
4 being
Point of c
1 such that
E12:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c2 . b3),c
3 < b
1 ) )
and
E13:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c2 . b3),c
4 < b
1 ) )
and
E14:
c
3 <> c
4
;
E15:
dist c
3,c
4 > 0
by E14, BHSP_1:45;
then E16:
(dist c3,c4) / 4
> 0
/ 4
by REAL_1:73;
then consider c
5 being
Nat such that
E17:
for b
1 being
Nat holds
not ( b
1 >= c
5 & not
dist (c2 . b1),c
3 < (dist c3,c4) / 4 )
by E12;
consider c
6 being
Nat such that
E18:
for b
1 being
Nat holds
not ( b
1 >= c
6 & not
dist (c2 . b1),c
4 < (dist c3,c4) / 4 )
by E13, E16;
E19:
now
assume
c
5 <= c
6
;
then E20:
dist (c2 . c6),c
3 < (dist c3,c4) / 4
by E17;
dist (c2 . c6),c
4 < (dist c3,c4) / 4
by E18;
then E21:
(dist (c2 . c6),c3) + (dist (c2 . c6),c4) < ((dist c3,c4) / 4) + ((dist c3,c4) / 4)
by E20, XREAL_1:10;
dist c
3,c
4 = dist (c3 - (c2 . c6)),
(c4 - (c2 . c6))
by BHSP_1:49;
then
dist c
3,c
4 <= (dist (c2 . c6),c3) + (dist (c2 . c6),c4)
by BHSP_1:50;
then
dist c
3,c
4 <= (dist c3,c4) / 2
by E21, XREAL_1:2;
hence
not verum
by E15, XREAL_1:218;
end;
now
assume
c
5 >= c
6
;
then E20:
dist (c2 . c5),c
4 < (dist c3,c4) / 4
by E18;
dist (c2 . c5),c
3 < (dist c3,c4) / 4
by E17;
then E21:
(dist (c2 . c5),c3) + (dist (c2 . c5),c4) < ((dist c3,c4) / 4) + ((dist c3,c4) / 4)
by E20, XREAL_1:10;
dist c
3,c
4 = dist (c3 - (c2 . c5)),
(c4 - (c2 . c5))
by BHSP_1:49;
then
dist c
3,c
4 <= (dist (c2 . c5),c3) + (dist (c2 . c5),c4)
by BHSP_1:50;
then
dist c
3,c
4 <= (dist c3,c4) / 2
by E21, XREAL_1:2;
hence
not verum
by E15, XREAL_1:218;
end;
hence
not verum
by E19;
end;
hence
for b
1, b
2 being
Point of c
1 holds
( ( for b
3 being
Real holds
not ( b
3 > 0 & for b
4 being
Nat holds
ex b
5 being
Nat st
( b
5 >= b
4 & not
dist (c2 . b5),b
1 < b
3 ) ) & for b
3 being
Real holds
not ( b
3 > 0 & for b
4 being
Nat holds
ex b
5 being
Nat st
( b
5 >= b
4 & not
dist (c2 . b5),b
2 < b
3 ) ) ) implies ( b
1 = b
2 ) )
;
end;
:: deftheorem E11 defines lim BHSP_2:def 2 :
theorem E12: :: BHSP_2:10
theorem :: BHSP_2:11
theorem :: BHSP_2:12
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that
E13:
c
2 is
convergent
and
E14:
ex b
1 being
Nat st
for b
2 being
Nat holds
( b
2 >= b
1 implies c
3 . b
2 = c
2 . b
2 )
;
E15:
c
3 is
convergent
by E13, E14, E3;
consider c
4 being
Nat such that
E16:
for b
1 being
Nat holds
( b
1 >= c
4 implies c
3 . b
1 = c
2 . b
1 )
by E14;
now
let c
5 be
Real;
assume
c
5 > 0
;
then consider c
6 being
Nat such that
E17:
for b
1 being
Nat holds
not ( b
1 >= c
6 & not
dist (c2 . b1),
(lim c2) < c
5 )
by E13, E11;
E18:
now
assume E19:
c
4 <= c
6
;
take c
7 = c
6;
let c
8 be
Nat;
assume E20:
c
8 >= c
7
;
then
c
8 >= c
4
by E19, XREAL_1:2;
then
c
3 . c
8 = c
2 . c
8
by E16;
hence
dist (c3 . c8),
(lim c2) < c
5
by E17, E20;
end;
now
assume E19:
c
6 <= c
4
;
take c
7 = c
4;
let c
8 be
Nat;
assume E20:
c
8 >= c
7
;
then
c
8 >= c
6
by E19, XREAL_1:2;
then
dist (c2 . c8),
(lim c2) < c
5
by E17;
hence
dist (c3 . c8),
(lim c2) < c
5
by E16, E20;
end;
hence
ex b
1 being
Nat st
for b
2 being
Nat holds
not ( b
2 >= b
1 & not
dist (c3 . b2),
(lim c2) < c
5 )
by E18;
end;
hence
lim c
2 = lim c
3
by E15, E11;
end;
theorem E13: :: BHSP_2:13
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that
E14:
c
2 is
convergent
and
E15:
c
3 is
convergent
;
E16:
c
2 + c
3 is
convergent
by E14, E15, E4;
set c
4 =
lim c
2;
set c
5 =
lim c
3;
set c
6 =
(lim c2) + (lim c3);
now
let c
7 be
Real;
assume
c
7 > 0
;
then E17:
c
7 / 2
> 0
by SEQ_2:3;
then consider c
8 being
Nat such that
E18:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),
(lim c2) < c
7 / 2 )
by E14, E11;
consider c
9 being
Nat such that
E19:
for b
1 being
Nat holds
not ( b
1 >= c
9 & not
dist (c3 . b1),
(lim c3) < c
7 / 2 )
by E15, E17, E11;
take c
10 = c
8 + c
9;
let c
11 be
Nat;
assume E20:
c
11 >= c
10
;
c
8 + c
9 >= c
8
by NAT_1:37;
then
c
11 >= c
8
by E20, XREAL_1:2;
then E21:
dist (c2 . c11),
(lim c2) < c
7 / 2
by E18;
c
10 >= c
9
by NAT_1:37;
then
c
11 >= c
9
by E20, XREAL_1:2;
then
dist (c3 . c11),
(lim c3) < c
7 / 2
by E19;
then E22:
(dist (c2 . c11),(lim c2)) + (dist (c3 . c11),(lim c3)) < (c7 / 2) + (c7 / 2)
by E21, XREAL_1:10;
dist ((c2 + c3) . c11),
((lim c2) + (lim c3)) = dist ((c2 . c11) + (c3 . c11)),
((lim c2) + (lim c3))
by NORMSP_1:def 5;
then
dist ((c2 + c3) . c11),
((lim c2) + (lim c3)) <= (dist (c2 . c11),(lim c2)) + (dist (c3 . c11),(lim c3))
by BHSP_1:47;
hence
dist ((c2 + c3) . c11),
((lim c2) + (lim c3)) < c
7
by E22, XREAL_1:2;
end;
hence
lim (c2 + c3) = (lim c2) + (lim c3)
by E16, E11;
end;
theorem E14: :: BHSP_2:14
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that
E15:
c
2 is
convergent
and
E16:
c
3 is
convergent
;
E17:
c
2 - c
3 is
convergent
by E15, E16, E5;
set c
4 =
lim c
2;
set c
5 =
lim c
3;
set c
6 =
(lim c2) - (lim c3);
now
let c
7 be
Real;
assume
c
7 > 0
;
then E18:
c
7 / 2
> 0
by SEQ_2:3;
then consider c
8 being
Nat such that
E19:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),
(lim c2) < c
7 / 2 )
by E15, E11;
consider c
9 being
Nat such that
E20:
for b
1 being
Nat holds
not ( b
1 >= c
9 & not
dist (c3 . b1),
(lim c3) < c
7 / 2 )
by E16, E18, E11;
take c
10 = c
8 + c
9;
let c
11 be
Nat;
assume E21:
c
11 >= c
10
;
c
8 + c
9 >= c
8
by NAT_1:37;
then
c
11 >= c
8
by E21, XREAL_1:2;
then E22:
dist (c2 . c11),
(lim c2) < c
7 / 2
by E19;
c
10 >= c
9
by NAT_1:37;
then
c
11 >= c
9
by E21, XREAL_1:2;
then
dist (c3 . c11),
(lim c3) < c
7 / 2
by E20;
then E23:
(dist (c2 . c11),(lim c2)) + (dist (c3 . c11),(lim c3)) < (c7 / 2) + (c7 / 2)
by E22, XREAL_1:10;
dist ((c2 - c3) . c11),
((lim c2) - (lim c3)) = dist ((c2 . c11) - (c3 . c11)),
((lim c2) - (lim c3))
by NORMSP_1:def 6;
then
dist ((c2 - c3) . c11),
((lim c2) - (lim c3)) <= (dist (c2 . c11),(lim c2)) + (dist (c3 . c11),(lim c3))
by BHSP_1:48;
hence
dist ((c2 - c3) . c11),
((lim c2) - (lim c3)) < c
7
by E23, XREAL_1:2;
end;
hence
lim (c2 - c3) = (lim c2) - (lim c3)
by E17, E11;
end;
theorem E15: :: BHSP_2:15
proof
let c
1 be
RealUnitarySpace;
let c
2 be
Real;
let c
3 be
sequence of c
1;
assume E16:
c
3 is
convergent
;
then E17:
c
2 * c
3 is
convergent
by E6;
set c
4 =
lim c
3;
set c
5 = c
2 * (lim c3);
E18:
now
assume E19:
c
2 = 0
;
let c
6 be
Real;
assume
c
6 > 0
;
then consider c
7 being
Nat such that
E20:
for b
1 being
Nat holds
not ( b
1 >= c
7 & not
dist (c3 . b1),
(lim c3) < c
6 )
by E16, E11;
take c
8 = c
7;
let c
9 be
Nat;
assume
c
9 >= c
8
;
then E21:
dist (c3 . c9),
(lim c3) < c
6
by E20;
dist (c2 * (c3 . c9)),
(c2 * (lim c3)) =
dist (0 * (c3 . c9)),H
1(c
1)
by E19, RLVECT_1:23
.=
dist H
1(c
1),H
1(c
1)
by RLVECT_1:23
.=
0
by BHSP_1:41
;
then
dist (c2 * (c3 . c9)),
(c2 * (lim c3)) < c
6
by E21, BHSP_1:44;
hence
dist ((c2 * c3) . c9),
(c2 * (lim c3)) < c
6
by NORMSP_1:def 8;
end;
now
assume E19:
c
2 <> 0
;
then E20:
abs c
2 > 0
by COMPLEX1:133;
let c
6 be
Real;
assume E21:
c
6 > 0
;
E22:
abs c
2 <> 0
by E19, COMPLEX1:133;
0
/ (abs c2) = 0
;
then
c
6 / (abs c2) > 0
by E20, E21, REAL_1:73;
then consider c
7 being
Nat such that
E23:
for b
1 being
Nat holds
not ( b
1 >= c
7 & not
dist (c3 . b1),
(lim c3) < c
6 / (abs c2) )
by E16, E11;
take c
8 = c
7;
let c
9 be
Nat;
assume
c
9 >= c
8
;
then E24:
dist (c3 . c9),
(lim c3) < c
6 / (abs c2)
by E23;
E25:
dist (c2 * (c3 . c9)),
(c2 * (lim c3)) =
||.((c2 * (c3 . c9)) - (c2 * (lim c3))).||
by BHSP_1:def 5
.=
||.(c2 * ((c3 . c9) - (lim c3))).||
by RLVECT_1:48
.=
(abs c2) * ||.((c3 . c9) - (lim c3)).||
by BHSP_1:33
.=
(abs c2) * (dist (c3 . c9),(lim c3))
by BHSP_1:def 5
;
(abs c2) * (c6 / (abs c2)) =
(abs c2) * (((abs c2) " ) * c6)
by XCMPLX_0:def 9
.=
((abs c2) * ((abs c2) " )) * c
6
.=
1
* c
6
by E22, XCMPLX_0:def 7
.=
c
6
;
then
dist (c2 * (c3 . c9)),
(c2 * (lim c3)) < c
6
by E20, E24, E25, XREAL_1:70;
hence
dist ((c2 * c3) . c9),
(c2 * (lim c3)) < c
6
by NORMSP_1:def 8;
end;
hence
lim (c2 * c3) = c
2 * (lim c3)
by E17, E18, E11;
end;
theorem E16: :: BHSP_2:16
theorem E17: :: BHSP_2:17