:: Introduction to Banach and Hilbert spaces - Part I
:: by Jan Popio{\l}ek
::
:: Received July 19, 1991
:: Copyright (c) 1991 Association of Mizar Users
registration
let D be non
empty set ;
let Z be
Element of
D;
let a be
BinOp of
D;
let m be
Function of
[:REAL ,D:],
D;
let s be
Function of
[:D,D:],
REAL ;
cluster UNITSTR(#
D,
Z,
a,
m,
s #)
-> non
empty ;
coherence
not UNITSTR(# D,Z,a,m,s #) is empty
;
end;
deffunc H1( UNITSTR ) -> Element of the carrier of $1 = 0. $1;
:: deftheorem defines .|. BHSP_1:def 1 :
consider V0 being RealLinearSpace;
Lm1:
the carrier of ((0). V0) = {(0. V0)}
by RLSUB_1:def 3;
reconsider nilfunc = [:the carrier of ((0). V0),the carrier of ((0). V0):] --> 0 as Function of [:the carrier of ((0). V0),the carrier of ((0). V0):], REAL by FUNCOP_1:57;
Lm2:
for x, y being VECTOR of ((0). V0) holds nilfunc . [x,y] = 0
by FUNCOP_1:13;
0. V0 in the carrier of ((0). V0)
by Lm1, TARSKI:def 1;
then Lm3:
nilfunc . [(0. V0),(0. V0)] = 0
by Lm2;
Lm4:
for u, v being VECTOR of ((0). V0) holds nilfunc . [u,v] = nilfunc . [v,u]
Lm5:
for u, v, w being VECTOR of ((0). V0) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
Lm6:
for u, v being VECTOR of ((0). V0)
for a being Real holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
set X0 = UNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #);
Lm7:
now
let x,
y,
z be
Point of
UNITSTR(# the
carrier of
((0). V0),
(0. ((0). V0)),the
addF of
((0). V0),the
Mult of
((0). V0),
nilfunc #);
:: thesis: for a being Real holds
( ( x .|. x = 0 implies x = H1( UNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #)) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )let a be
Real;
:: thesis: ( ( x .|. x = 0 implies x = H1( UNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #)) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(
x .|. x = 0 iff
x = H1(
UNITSTR(# the
carrier of
((0). V0),
(0. ((0). V0)),the
addF of
((0). V0),the
Mult of
((0). V0),
nilfunc #)) )
:: thesis: ( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
proof
H1(
UNITSTR(# the
carrier of
((0). V0),
(0. ((0). V0)),the
addF of
((0). V0),the
Mult of
((0). V0),
nilfunc #))
= 0. V0
by RLSUB_1:19;
hence
(
x .|. x = 0 iff
x = H1(
UNITSTR(# the
carrier of
((0). V0),
(0. ((0). V0)),the
addF of
((0). V0),the
Mult of
((0). V0),
nilfunc #)) )
by Lm1, FUNCOP_1:13, TARSKI:def 1;
:: thesis: verum
end;
thus
0 <= x .|. x
by FUNCOP_1:13;
:: thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
x .|. y = y .|. x
by Lm4;
:: thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(x + y) .|. z = (x .|. z) + (y .|. z)
:: thesis: (a * x) .|. y = a * (x .|. y)
thus
(a * x) .|. y = a * (x .|. y)
:: thesis: verum
end;
:: deftheorem Def2 defines RealUnitarySpace-like BHSP_1:def 2 :
theorem :: BHSP_1:1
canceled;
theorem :: BHSP_1:2
canceled;
theorem :: BHSP_1:3
canceled;
theorem :: BHSP_1:4
canceled;
theorem :: BHSP_1:5
canceled;
theorem :: BHSP_1:6
theorem :: BHSP_1:7
theorem :: BHSP_1:8
theorem :: BHSP_1:9
theorem Th10: :: BHSP_1:10
theorem :: BHSP_1:11
theorem :: BHSP_1:12
theorem Th13: :: BHSP_1:13
theorem :: BHSP_1:14
theorem Th15: :: BHSP_1:15
theorem Th16: :: BHSP_1:16
theorem Th17: :: BHSP_1:17
theorem :: BHSP_1:18
theorem Th19: :: BHSP_1:19
theorem :: BHSP_1:20
theorem Th21: :: BHSP_1:21
theorem :: BHSP_1:22
theorem Th23: :: BHSP_1:23
theorem Th24: :: BHSP_1:24
:: deftheorem Def3 defines are_orthogonal BHSP_1:def 3 :
theorem :: BHSP_1:25
canceled;
theorem :: BHSP_1:26
theorem :: BHSP_1:27
theorem :: BHSP_1:28
theorem :: BHSP_1:29
theorem :: BHSP_1:30
theorem :: BHSP_1:31
:: deftheorem defines ||. BHSP_1:def 4 :
theorem Th32: :: BHSP_1:32
theorem Th33: :: BHSP_1:33
theorem Th34: :: BHSP_1:34
theorem :: BHSP_1:35
theorem Th36: :: BHSP_1:36
theorem Th37: :: BHSP_1:37
theorem Th38: :: BHSP_1:38
theorem :: BHSP_1:39
:: deftheorem defines dist BHSP_1:def 5 :
theorem :: BHSP_1:40
canceled;
theorem Th41: :: BHSP_1:41
theorem :: BHSP_1:42
theorem Th43: :: BHSP_1:43
theorem :: BHSP_1:44
theorem :: BHSP_1:45
theorem :: BHSP_1:46
theorem :: BHSP_1:47
theorem :: BHSP_1:48
theorem :: BHSP_1:49
theorem :: BHSP_1:50
:: deftheorem BHSP_1:def 6 :
canceled;
:: deftheorem BHSP_1:def 7 :
canceled;
:: deftheorem BHSP_1:def 8 :
canceled;
:: deftheorem BHSP_1:def 9 :
canceled;
:: deftheorem Def10 defines - BHSP_1:def 10 :
:: deftheorem BHSP_1:def 11 :
canceled;
:: deftheorem Def12 defines + BHSP_1:def 12 :
theorem :: BHSP_1:51
canceled;
theorem :: BHSP_1:52
canceled;
theorem :: BHSP_1:53
canceled;
theorem :: BHSP_1:54
canceled;
theorem Th55: :: BHSP_1:55
theorem :: BHSP_1:56
theorem :: BHSP_1:57
theorem :: BHSP_1:58
theorem :: BHSP_1:59
theorem :: BHSP_1:60
canceled;
theorem :: BHSP_1:61
canceled;
theorem :: BHSP_1:62
canceled;
theorem :: BHSP_1:63
canceled;
theorem :: BHSP_1:64
canceled;
theorem :: BHSP_1:65
canceled;
theorem :: BHSP_1:66
canceled;
theorem :: BHSP_1:67
canceled;
theorem :: BHSP_1:68
canceled;
theorem :: BHSP_1:69
canceled;
theorem :: BHSP_1:70
canceled;
theorem :: BHSP_1:71
theorem :: BHSP_1:72
theorem :: BHSP_1:73
theorem :: BHSP_1:74
theorem :: BHSP_1:75
theorem :: BHSP_1:76
theorem :: BHSP_1:77
theorem :: BHSP_1:78
theorem :: BHSP_1:79
theorem :: BHSP_1:80
theorem :: BHSP_1:81
theorem :: BHSP_1:82
theorem :: BHSP_1:83
theorem :: BHSP_1:84
theorem :: BHSP_1:85