begin
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;
( ( for x, y being VECTOR of holds nilfunc . [x,y] = 0 ) & 0. V0 in the carrier of ((0). V0) )
by Lm1, FUNCOP_1:13, TARSKI:def 1;
then Lm2:
nilfunc . [(0. V0),(0. V0)] = 0
;
Lm3:
for u, v being VECTOR of holds nilfunc . [u,v] = nilfunc . [v,u]
Lm4:
for u, v, w being VECTOR of holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
Lm5:
for u, v being VECTOR of
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 #);
Lm6:
now
let x,
y,
z be
Point of ;
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;
( ( 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) )
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;
( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
0 <= x .|. x
by FUNCOP_1:13;
( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
x .|. y = y .|. x
by Lm3;
( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(x + y) .|. z = (x .|. z) + (y .|. z)
(a * x) .|. y = a * (x .|. y)
thus
(a * x) .|. y = a * (x .|. y)
verum
end;
:: deftheorem Def2 defines RealUnitarySpace-like BHSP_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th10:
theorem
theorem
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem
theorem Th21:
theorem
theorem Th23:
theorem Th24:
:: deftheorem Def3 defines are_orthogonal BHSP_1:def 3 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines ||. BHSP_1:def 4 :
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem
:: deftheorem defines dist BHSP_1:def 5 :
theorem
canceled;
theorem Th41:
theorem
theorem Th43:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th55:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem