:: BHSP_1 semantic presentation

begin

definition
attrc1 is strict ;
struct UNITSTR  ->  RLSStruct ;
aggrUNITSTR(# carrier, ZeroF, addF, Mult, scalar #) ->  UNITSTR ;
sel scalar c1 ->  Function of [: the carrier of c1, the carrier of c1:],REAL;
end;

registration
cluster non empty strict for UNITSTR ;
existence
 ex b1 being UNITSTR st
( not b1 is empty & b1 is strict )
proof
set D = the non empty set ;
set Z = the Element of the non empty set ;
set a = the BinOp of the non empty set ;
set m = the Function of [:REAL, the non empty set :], the non empty set ;
set s = the Function of [: the non empty set , the non empty set :],REAL;
take  UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) ; ::_thesis: ( not UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is empty & UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict )
thus  not the carrier of UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict
thus  UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict ; ::_thesis: verum
end;
end;

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;

definition
let X be non empty UNITSTR ;
let x, y be Point of X;
funcx .|. y ->  Real equals :: BHSP_1:def 1
 the scalar of X . [x,y];
correctness
coherence
the scalar of X . [x,y] is Real;
;
end;

:: deftheorem  defines .|. BHSP_1:def_1_:_
 for X being non empty UNITSTR
for x, y being Point of X holds x .|. y = the scalar of X . [x,y];

set V0 = the RealLinearSpace;

Lm1:  the carrier of ((0). the RealLinearSpace) = {(0. the RealLinearSpace)}
by RLSUB_1:def_3;

reconsider nilfunc = [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):] --> 0 as Function of [: the carrier of ((0). the RealLinearSpace), the carrier of ((0). the RealLinearSpace):],REAL by FUNCOP_1:45;

 ( ( for x, y being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [x,y] = 0 ) & 0. the RealLinearSpace in the carrier of ((0). the RealLinearSpace) )
by Lm1, FUNCOP_1:7, TARSKI:def_1;

then Lm2:  nilfunc . [(0. the RealLinearSpace),(0. the RealLinearSpace)] = 0
;

Lm3:  for u, v being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [u,v] = nilfunc . [v,u]
proof
let u, v be VECTOR of ((0). the RealLinearSpace); ::_thesis: nilfunc . [u,v] = nilfunc . [v,u]
 ( u = 0. the RealLinearSpace & v = 0. the RealLinearSpace ) by Lm1, TARSKI:def_1;
hence  nilfunc . [u,v] = nilfunc . [v,u] ; ::_thesis: verum
end;

Lm4:  for u, v, w being VECTOR of ((0). the RealLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
proof
let u, v, w be VECTOR of ((0). the RealLinearSpace); ::_thesis: nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
A1: w = 0. the RealLinearSpace by Lm1, TARSKI:def_1;
 ( u = 0. the RealLinearSpace & v = 0. the RealLinearSpace ) by Lm1, TARSKI:def_1;
hence  nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w]) by A1, Lm1, Lm2, TARSKI:def_1; ::_thesis: verum
end;

Lm5:  for u, v being VECTOR of ((0). the RealLinearSpace)
for a being Real holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
proof
let u, v be VECTOR of ((0). the RealLinearSpace); ::_thesis: for a being Real holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
let a be Real; ::_thesis: nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
 ( u = 0. the RealLinearSpace & v = 0. the RealLinearSpace ) by Lm1, TARSKI:def_1;
hence  nilfunc . [(a * u),v] = a * (nilfunc . [u,v]) by Lm1, Lm2, TARSKI:def_1; ::_thesis: verum
end;

set X0 = UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #);

Lm6: now__::_thesis:_for_x,_y,_z_being_Point_of_UNITSTR(#_the_carrier_of_((0)._the_RealLinearSpace),(0._((0)._the_RealLinearSpace)),_the_addF_of_((0)._the_RealLinearSpace),_the_Mult_of_((0)._the_RealLinearSpace),nilfunc_#)
for_a_being_Real_holds_
(_(_x_.|._x_=_0_implies_x_=_H1(_UNITSTR(#_the_carrier_of_((0)._the_RealLinearSpace),(0._((0)._the_RealLinearSpace)),_the_addF_of_((0)._the_RealLinearSpace),_the_Mult_of_((0)._the_RealLinearSpace),nilfunc_#))_)_&_(_x_=_H1(_UNITSTR(#_the_carrier_of_((0)._the_RealLinearSpace),(0._((0)._the_RealLinearSpace)),_the_addF_of_((0)._the_RealLinearSpace),_the_Mult_of_((0)._the_RealLinearSpace),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 x, y, z be Point of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); ::_thesis: for a being Real holds
( ( x .|. x = 0 implies x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),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). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) & ( x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),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). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) = 0. the RealLinearSpace by RLSUB_1:11;
hence  ( x .|. x = 0 iff x = H1( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) ) by Lm1, FUNCOP_1:7, TARSKI:def_1; ::_thesis: ( 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:7; ::_thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
thus  x .|. y = y .|. x by Lm3; ::_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)
proof
reconsider u = x, v = y, w = z as VECTOR of ((0). the RealLinearSpace) ;
 (x + y) .|. z = nilfunc . [(u + v),w] ;
hence  (x + y) .|. z = (x .|. z) + (y .|. z) by Lm4; ::_thesis: verum
end;
thus  (a * x) .|. y = a * (x .|. y) ::_thesis: verum
proof
reconsider u = x, v = y as VECTOR of ((0). the RealLinearSpace) ;
 (a * x) .|. y = nilfunc . [(a * u),v] ;
hence  (a * x) .|. y = a * (x .|. y) by Lm5; ::_thesis: verum
end;
end;

definition
let IT be non empty UNITSTR ;
attrIT is RealUnitarySpace-like  means :Def2: :: BHSP_1:def 2
 for x, y, z being Point of IT
for a being Real holds
( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) );
end;

:: deftheorem Def2 defines RealUnitarySpace-like BHSP_1:def_2_:_
 for IT being non empty UNITSTR holds
( IT is RealUnitarySpace-like iff for x, y, z being Point of IT
for a being Real holds
( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) );

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like for UNITSTR ;
existence
 ex b1 being non empty UNITSTR st
( b1 is RealUnitarySpace-like & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof
take  UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) ; ::_thesis: ( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is RealUnitarySpace-like & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is vector-distributive & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-distributive & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-associative & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-unital & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is Abelian & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is add-associative & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_zeroed & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_complementable & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is strict )
thus  UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is RealUnitarySpace-like by Def2, Lm6; ::_thesis: ( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is vector-distributive & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-distributive & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-associative & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-unital & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is Abelian & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is add-associative & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_zeroed & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_complementable & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is strict )
thus  ( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is vector-distributive & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-distributive & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-associative & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-unital ) ::_thesis: ( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is Abelian & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is add-associative & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_zeroed & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_complementable & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is strict )
proof
thus  for a being real number
for v, w being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-distributive & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-associative & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-unital )
proof
let a be real number ; ::_thesis: for v, w being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider v9 = v, w9 = w as VECTOR of ((0). the RealLinearSpace) ;
thus a * (v + w) = a * (v9 + w9)
.= (a * v9) + (a * w9) by RLVECT_1:def_5
.= (a * v) + (a * w) ; ::_thesis: verum
end;
thus  for a, b being real number
for v being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-associative & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-unital )
proof
let a, b be real number ; ::_thesis: for v being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
thus (a + b) * v = (a + b) * v9
.= (a * v9) + (b * v9) by RLVECT_1:def_6
.= (a * v) + (b * v) ; ::_thesis: verum
end;
thus  for a, b being real number
for v being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is scalar-unital
proof
let a, b be real number ; ::_thesis: for v being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) holds (a * b) * v = a * (b * v)
let v be VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); ::_thesis: (a * b) * v = a * (b * v)
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by RLVECT_1:def_7
.= a * (b * v) ; ::_thesis: verum
end;
let v be VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
thus 1 * v = 1 * v9
.= v by RLVECT_1:def_8 ; ::_thesis: verum
end;
A1: for x, y being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)
for x9, y9 being VECTOR of ((0). the RealLinearSpace) st x = x9 & y = y9 holds
( x + y = x9 + y9 & ( for a being Real holds a * x = a * x9 ) ) ;
thus  for v, w being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) holds v + w = w + v :: according to RLVECT_1:def_2 ::_thesis: ( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is add-associative & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_zeroed & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_complementable & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is strict )
proof
let v, w be VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); ::_thesis: v + w = w + v
reconsider v9 = v, w9 = w as VECTOR of ((0). the RealLinearSpace) ;
thus v + w = w9 + v9 by A1
.= w + v ; ::_thesis: verum
end;
thus  for u, v, w being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) holds (u + v) + w = u + (v + w) :: according to RLVECT_1:def_3 ::_thesis: ( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_zeroed & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_complementable & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is strict )
proof
let u, v, w be VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); ::_thesis: (u + v) + w = u + (v + w)
reconsider u9 = u, v9 = v, w9 = w as VECTOR of ((0). the RealLinearSpace) ;
thus (u + v) + w = (u9 + v9) + w9
.= u9 + (v9 + w9) by RLVECT_1:def_3
.= u + (v + w) ; ::_thesis: verum
end;
thus  for v being VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) holds v + (0. UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) = v :: according to RLVECT_1:def_4 ::_thesis: ( UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_complementable & UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is strict )
proof
let v be VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); ::_thesis: v + (0. UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) = v
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
thus v + (0. UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)) = v9 + (0. ((0). the RealLinearSpace))
.= v by RLVECT_1:4 ; ::_thesis: verum
end;
thus  UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is right_complementable ::_thesis: UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is strict
proof
let v be VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
consider w9 being VECTOR of ((0). the RealLinearSpace) such that
A2: v9 + w9 = 0. ((0). the RealLinearSpace) by ALGSTR_0:def_11;
reconsider w = w9 as VECTOR of UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #)
thus  v + w = 0. UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) by A2; ::_thesis: verum
end;
thus  UNITSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),nilfunc #) is strict ; ::_thesis: verum
end;
end;

definition
mode RealUnitarySpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR ;
end;


definition
let X be RealUnitarySpace;
let x, y be Point of X;
:: original: .|.
redefine funcx .|. y ->  Real;
commutativity
 for x, y being Point of X holds x .|. y = y .|. x by Def2;
end;

theorem :: BHSP_1:1
for X being RealUnitarySpace holds (0. X) .|. (0. X) = 0 by Def2;

theorem :: BHSP_1:2
for X being RealUnitarySpace
for x, y, z being Point of X holds x .|. (y + z) = (x .|. y) + (x .|. z) by Def2;

theorem :: BHSP_1:3
for a being Real
for X being RealUnitarySpace
for x, y being Point of X holds x .|. (a * y) = a * (x .|. y) by Def2;

theorem :: BHSP_1:4
for a being Real
for X being RealUnitarySpace
for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)
proof
let a be Real; ::_thesis: for X being RealUnitarySpace
for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)
let x, y be Point of X; ::_thesis: (a * x) .|. y = x .|. (a * y)
 (a * x) .|. y = a * (x .|. y) by Def2;
hence  (a * x) .|. y = x .|. (a * y) by Def2; ::_thesis: verum
end;

theorem Th5: :: BHSP_1:5
for a, b being Real
for X being RealUnitarySpace
for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))
proof
let a, b be Real; ::_thesis: for X being RealUnitarySpace
for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))
let X be RealUnitarySpace; ::_thesis: for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))
let x, y, z be Point of X; ::_thesis: ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))
((a * x) + (b * y)) .|. z = ((a * x) .|. z) + ((b * y) .|. z) by Def2
.= (a * (x .|. z)) + ((b * y) .|. z) by Def2 ;
hence  ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z)) by Def2; ::_thesis: verum
end;

theorem :: BHSP_1:6
for a, b being Real
for X being RealUnitarySpace
for x, y, z being Point of X holds x .|. ((a * y) + (b * z)) = (a * (x .|. y)) + (b * (x .|. z)) by Th5;

theorem :: BHSP_1:7
for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. y = x .|. (- y)
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds (- x) .|. y = x .|. (- y)
let x, y be Point of X; ::_thesis: (- x) .|. y = x .|. (- y)
(- x) .|. y = ((- 1) * x) .|. y by RLVECT_1:16
.= (- 1) * (x .|. y) by Def2
.= x .|. ((- 1) * y) by Def2 ;
hence  (- x) .|. y = x .|. (- y) by RLVECT_1:16; ::_thesis: verum
end;

theorem Th8: :: BHSP_1:8
for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. y = - (x .|. y)
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds (- x) .|. y = - (x .|. y)
let x, y be Point of X; ::_thesis: (- x) .|. y = - (x .|. y)
(- x) .|. y = ((- 1) * x) .|. y by RLVECT_1:16
.= (- 1) * (x .|. y) by Def2 ;
hence  (- x) .|. y = - (x .|. y) ; ::_thesis: verum
end;

theorem :: BHSP_1:9
for X being RealUnitarySpace
for x, y being Point of X holds x .|. (- y) = - (x .|. y) by Th8;

theorem Th10: :: BHSP_1:10
for X being RealUnitarySpace
for x, y being Point of X holds (- x) .|. (- y) = x .|. y
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds (- x) .|. (- y) = x .|. y
let x, y be Point of X; ::_thesis: (- x) .|. (- y) = x .|. y
(- x) .|. (- y) = - (x .|. (- y)) by Th8
.= - (- (x .|. y)) by Th8 ;
hence  (- x) .|. (- y) = x .|. y ; ::_thesis: verum
end;

theorem Th11: :: BHSP_1:11
for X being RealUnitarySpace
for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)
proof
let X be RealUnitarySpace; ::_thesis: for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)
let x, y, z be Point of X; ::_thesis: (x - y) .|. z = (x .|. z) - (y .|. z)
(x - y) .|. z = (x .|. z) + ((- y) .|. z) by Def2
.= (x .|. z) + (- (y .|. z)) by Th8 ;
hence  (x - y) .|. z = (x .|. z) - (y .|. z) ; ::_thesis: verum
end;

theorem Th12: :: BHSP_1:12
for X being RealUnitarySpace
for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z)
proof
let X be RealUnitarySpace; ::_thesis: for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z)
let x, y, z be Point of X; ::_thesis: x .|. (y - z) = (x .|. y) - (x .|. z)
x .|. (y - z) = (x .|. y) + (x .|. (- z)) by Def2
.= (x .|. y) + (- (x .|. z)) by Th8 ;
hence  x .|. (y - z) = (x .|. y) - (x .|. z) ; ::_thesis: verum
end;

theorem :: BHSP_1:13
for X being RealUnitarySpace
for x, y, u, v being Point of X holds (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v)
proof
let X be RealUnitarySpace; ::_thesis: for x, y, u, v being Point of X holds (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v)
let x, y, u, v be Point of X; ::_thesis: (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v)
(x - y) .|. (u - v) = (x .|. (u - v)) - (y .|. (u - v)) by Th11
.= ((x .|. u) - (x .|. v)) - (y .|. (u - v)) by Th12
.= ((x .|. u) - (x .|. v)) - ((y .|. u) - (y .|. v)) by Th12 ;
hence  (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v) ; ::_thesis: verum
end;

theorem Th14: :: BHSP_1:14
for X being RealUnitarySpace
for x being Point of X holds (0. X) .|. x = 0
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X holds (0. X) .|. x = 0
let x be Point of X; ::_thesis: (0. X) .|. x = 0
H1(X) .|. x = (x + (- x)) .|. x by RLVECT_1:5
.= (x .|. x) + ((- x) .|. x) by Def2
.= (x .|. x) + (- (x .|. x)) by Th8 ;
hence  (0. X) .|. x = 0 ; ::_thesis: verum
end;

theorem :: BHSP_1:15
for X being RealUnitarySpace
for x being Point of X holds x .|. (0. X) = 0 by Th14;

theorem Th16: :: BHSP_1:16
for X being RealUnitarySpace
for x, y being Point of X holds (x + y) .|. (x + y) = ((x .|. x) + (2 * (x .|. y))) + (y .|. y)
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds (x + y) .|. (x + y) = ((x .|. x) + (2 * (x .|. y))) + (y .|. y)
let x, y be Point of X; ::_thesis: (x + y) .|. (x + y) = ((x .|. x) + (2 * (x .|. y))) + (y .|. y)
(x + y) .|. (x + y) = (x .|. (x + y)) + (y .|. (x + y)) by Def2
.= ((x .|. x) + (x .|. y)) + (y .|. (x + y)) by Def2
.= ((x .|. x) + (x .|. y)) + ((x .|. y) + (y .|. y)) by Def2
.= ((x .|. x) + ((x .|. y) + (x .|. y))) + (y .|. y) ;
hence  (x + y) .|. (x + y) = ((x .|. x) + (2 * (x .|. y))) + (y .|. y) ; ::_thesis: verum
end;

theorem :: BHSP_1:17
for X being RealUnitarySpace
for x, y being Point of X holds (x + y) .|. (x - y) = (x .|. x) - (y .|. y)
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds (x + y) .|. (x - y) = (x .|. x) - (y .|. y)
let x, y be Point of X; ::_thesis: (x + y) .|. (x - y) = (x .|. x) - (y .|. y)
(x + y) .|. (x - y) = (x .|. (x - y)) + (y .|. (x - y)) by Def2
.= ((x .|. x) - (x .|. y)) + (y .|. (x - y)) by Th12
.= ((x .|. x) - (x .|. y)) + ((x .|. y) - (y .|. y)) by Th12 ;
hence  (x + y) .|. (x - y) = (x .|. x) - (y .|. y) ; ::_thesis: verum
end;

theorem Th18: :: BHSP_1:18
for X being RealUnitarySpace
for x, y being Point of X holds (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y)
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y)
let x, y be Point of X; ::_thesis: (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y)
(x - y) .|. (x - y) = (x .|. (x - y)) - (y .|. (x - y)) by Th11
.= ((x .|. x) - (x .|. y)) - (y .|. (x - y)) by Th12
.= ((x .|. x) - (x .|. y)) - ((x .|. y) - (y .|. y)) by Th12
.= ((x .|. x) - ((x .|. y) + (x .|. y))) + (y .|. y) ;
hence  (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y) ; ::_thesis: verum
end;

theorem Th19: :: BHSP_1:19
for X being RealUnitarySpace
for x, y being Point of X holds abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y))
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y))
let x, y be Point of X; ::_thesis: abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y))
A1: ( x <> H1(X) implies abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y)) )
proof
A2: for t being real number holds (((x .|. x) * (t ^2)) + ((2 * (x .|. y)) * t)) + (y .|. y) >= 0
proof
let t be real number ; ::_thesis: (((x .|. x) * (t ^2)) + ((2 * (x .|. y)) * t)) + (y .|. y) >= 0
reconsider t = t as Real by XREAL_0:def_1;
 ((t * x) + y) .|. ((t * x) + y) >= 0 by Def2;
then  (((t * x) .|. (t * x)) + (2 * ((t * x) .|. y))) + (y .|. y) >= 0 by Th16;
then  ((t * (x .|. (t * x))) + (2 * ((t * x) .|. y))) + (y .|. y) >= 0 by Def2;
then  ((t * (t * (x .|. x))) + (2 * ((t * x) .|. y))) + (y .|. y) >= 0 by Def2;
then  (((x .|. x) * (t ^2)) + (2 * ((x .|. y) * t))) + (y .|. y) >= 0 by Def2;
hence  (((x .|. x) * (t ^2)) + ((2 * (x .|. y)) * t)) + (y .|. y) >= 0 ; ::_thesis: verum
end;
A3: x .|. x >= 0 by Def2;
assume  x <> H1(X) ; ::_thesis: abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y))
then  x .|. x <> 0 by Def2;
then  delta ((x .|. x),(2 * (x .|. y)),(y .|. y)) <= 0 by A3, A2, QUIN_1:10;
then  ((2 * (x .|. y)) ^2) - ((4 * (x .|. x)) * (y .|. y)) <= 0 by QUIN_1:def_1;
then  4 * (((x .|. y) ^2) - ((x .|. x) * (y .|. y))) <= 0 ;
then  ((x .|. y) ^2) - ((x .|. x) * (y .|. y)) <= 0 / 4 by XREAL_1:77;
then  (x .|. y) ^2 <= (x .|. x) * (y .|. y) by XREAL_1:50;
then  ( (abs (x .|. y)) ^2 >= 0 & (abs (x .|. y)) ^2 <= (x .|. x) * (y .|. y) ) by COMPLEX1:75, XREAL_1:63;
then  sqrt ((abs (x .|. y)) ^2) <= sqrt ((x .|. x) * (y .|. y)) by SQUARE_1:26;
then A4: abs (x .|. y) <= sqrt ((x .|. x) * (y .|. y)) by COMPLEX1:46, SQUARE_1:22;
 y .|. y >= 0 by Def2;
hence  abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y)) by A3, A4, SQUARE_1:29; ::_thesis: verum
end;
 ( x = H1(X) implies abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y)) )
proof
assume  x = H1(X) ; ::_thesis: abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y))
then  ( x .|. y = 0 & sqrt (x .|. x) = 0 ) by Th14, SQUARE_1:17;
hence  abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y)) by ABSVALUE:2; ::_thesis: verum
end;
hence  abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y)) by A1; ::_thesis: verum
end;

definition
let X be RealUnitarySpace;
let x, y be Point of X;
predx,y are_orthogonal  means :Def3: :: BHSP_1:def 3
x .|. y = 0 ;
symmetry
 for x, y being Point of X st x .|. y = 0 holds
y .|. x = 0 ;
end;

:: deftheorem Def3 defines are_orthogonal BHSP_1:def_3_:_
 for X being RealUnitarySpace
for x, y being Point of X holds
( x,y are_orthogonal iff x .|. y = 0 );

theorem :: BHSP_1:20
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
x, - y are_orthogonal
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds
x, - y are_orthogonal
let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies x, - y are_orthogonal )
assume  x,y are_orthogonal ; ::_thesis: x, - y are_orthogonal
then  - (x .|. y) = - 0 by Def3;
then  x .|. (- y) = 0 by Th8;
hence  x, - y are_orthogonal by Def3; ::_thesis: verum
end;

theorem :: BHSP_1:21
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x,y are_orthogonal
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds
- x,y are_orthogonal
let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies - x,y are_orthogonal )
assume  x,y are_orthogonal ; ::_thesis: - x,y are_orthogonal
then  - (x .|. y) = - 0 by Def3;
then  (- x) .|. y = 0 by Th8;
hence  - x,y are_orthogonal by Def3; ::_thesis: verum
end;

theorem :: BHSP_1:22
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x, - y are_orthogonal
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds
- x, - y are_orthogonal
let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies - x, - y are_orthogonal )
assume  x,y are_orthogonal ; ::_thesis: - x, - y are_orthogonal
then  x .|. y = 0 by Def3;
then  (- x) .|. (- y) = 0 by Th10;
hence  - x, - y are_orthogonal by Def3; ::_thesis: verum
end;

theorem :: BHSP_1:23
for X being RealUnitarySpace
for x being Point of X holds x, 0. X are_orthogonal
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X holds x, 0. X are_orthogonal
let x be Point of X; ::_thesis: x, 0. X are_orthogonal
 x .|. H1(X) = 0 by Th14;
hence  x, 0. X are_orthogonal by Def3; ::_thesis: verum
end;

theorem :: BHSP_1:24
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
(x + y) .|. (x + y) = (x .|. x) + (y .|. y)
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds
(x + y) .|. (x + y) = (x .|. x) + (y .|. y)
let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies (x + y) .|. (x + y) = (x .|. x) + (y .|. y) )
assume  x,y are_orthogonal ; ::_thesis: (x + y) .|. (x + y) = (x .|. x) + (y .|. y)
then A1: x .|. y = 0 by Def3;
 (x + y) .|. (x + y) = ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by Th16;
hence  (x + y) .|. (x + y) = (x .|. x) + (y .|. y) by A1; ::_thesis: verum
end;

theorem :: BHSP_1:25
for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
(x - y) .|. (x - y) = (x .|. x) + (y .|. y)
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds
(x - y) .|. (x - y) = (x .|. x) + (y .|. y)
let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies (x - y) .|. (x - y) = (x .|. x) + (y .|. y) )
assume  x,y are_orthogonal ; ::_thesis: (x - y) .|. (x - y) = (x .|. x) + (y .|. y)
then A1: x .|. y = 0 by Def3;
(x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y) by Th18
.= ((x .|. x) + (y .|. y)) - 0 by A1 ;
hence  (x - y) .|. (x - y) = (x .|. x) + (y .|. y) ; ::_thesis: verum
end;

definition
let X be RealUnitarySpace;
let x be Point of X;
func||.x.|| ->  Real equals :: BHSP_1:def 4
 sqrt (x .|. x);
correctness
coherence
sqrt (x .|. x) is Real;
;
end;

:: deftheorem  defines ||. BHSP_1:def_4_:_
 for X being RealUnitarySpace
for x being Point of X holds ||.x.|| = sqrt (x .|. x);

theorem Th26: :: BHSP_1:26
for X being RealUnitarySpace
for x being Point of X holds
( ||.x.|| = 0 iff x = 0. X )
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X holds
( ||.x.|| = 0 iff x = 0. X )
let x be Point of X; ::_thesis: ( ||.x.|| = 0 iff x = 0. X )
thus  ( ||.x.|| = 0 implies x = H1(X) ) ::_thesis: ( x = 0. X implies ||.x.|| = 0 )
proof
assume A1: ||.x.|| = 0 ; ::_thesis: x = H1(X)
 0 <= x .|. x by Def2;
then  x .|. x = 0 by A1, SQUARE_1:24;
hence  x = H1(X) by Def2; ::_thesis: verum
end;
assume  x = H1(X) ; ::_thesis: ||.x.|| = 0
hence  ||.x.|| = 0 by Def2, SQUARE_1:17; ::_thesis: verum
end;

theorem Th27: :: BHSP_1:27
for a being Real
for X being RealUnitarySpace
for x being Point of X holds ||.(a * x).|| = (abs a) * ||.x.||
proof
let a be Real; ::_thesis: for X being RealUnitarySpace
for x being Point of X holds ||.(a * x).|| = (abs a) * ||.x.||
let X be RealUnitarySpace; ::_thesis: for x being Point of X holds ||.(a * x).|| = (abs a) * ||.x.||
let x be Point of X; ::_thesis: ||.(a * x).|| = (abs a) * ||.x.||
A1: ( 0 <= a ^2 & 0 <= x .|. x ) by Def2, XREAL_1:63;
||.(a * x).|| = sqrt (a * (x .|. (a * x))) by Def2
.= sqrt (a * (a * (x .|. x))) by Def2
.= sqrt ((a ^2) * (x .|. x))
.= (sqrt (a ^2)) * (sqrt (x .|. x)) by A1, SQUARE_1:29
.= (abs a) * (sqrt (x .|. x)) by COMPLEX1:72 ;
hence  ||.(a * x).|| = (abs a) * ||.x.|| ; ::_thesis: verum
end;

theorem Th28: :: BHSP_1:28
for X being RealUnitarySpace
for x being Point of X holds 0 <= ||.x.||
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X holds 0 <= ||.x.||
let x be Point of X; ::_thesis: 0 <= ||.x.||
 0 <= x .|. x by Def2;
hence  0 <= ||.x.|| by SQUARE_1:def_2; ::_thesis: verum
end;

theorem :: BHSP_1:29
for X being RealUnitarySpace
for x, y being Point of X holds abs (x .|. y) <= ||.x.|| * ||.y.|| by Th19;

theorem Th30: :: BHSP_1:30
for X being RealUnitarySpace
for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.||
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.||
let x, y be Point of X; ::_thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
A1: sqrt (||.(x + y).|| ^2) = sqrt ((x + y) .|. (x + y)) by Th28, SQUARE_1:22;
 ( (x + y) .|. (x + y) >= 0 & ||.(x + y).|| ^2 >= 0 ) by Def2, XREAL_1:63;
then  ||.(x + y).|| ^2 = (x + y) .|. (x + y) by A1, SQUARE_1:28;
then A2: ||.(x + y).|| ^2 = ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by Th16;
 x .|. x >= 0 by Def2;
then A3: ||.(x + y).|| ^2 = (((sqrt (x .|. x)) ^2) + (2 * (x .|. y))) + (y .|. y) by A2, SQUARE_1:def_2;
A4: ( ||.x.|| >= 0 & ||.y.|| >= 0 ) by Th28;
 ( abs (x .|. y) <= ||.x.|| * ||.y.|| & x .|. y <= abs (x .|. y) ) by Th19, ABSVALUE:4;
then  x .|. y <= ||.x.|| * ||.y.|| by XXREAL_0:2;
then  2 * (x .|. y) <= 2 * (||.x.|| * ||.y.||) by XREAL_1:64;
then  (||.x.|| ^2) + (2 * (x .|. y)) <= (||.x.|| ^2) + ((2 * ||.x.||) * ||.y.||) by XREAL_1:7;
then A5: ((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2) <= ((||.x.|| ^2) + ((2 * ||.x.||) * ||.y.||)) + (||.y.|| ^2) by XREAL_1:6;
 y .|. y >= 0 by Def2;
then  ||.(x + y).|| ^2 <= (||.x.|| + ||.y.||) ^2 by A3, A5, SQUARE_1:def_2;
hence  ||.(x + y).|| <= ||.x.|| + ||.y.|| by A4, SQUARE_1:16; ::_thesis: verum
end;

theorem Th31: :: BHSP_1:31
for X being RealUnitarySpace
for x being Point of X holds ||.(- x).|| = ||.x.||
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X holds ||.(- x).|| = ||.x.||
let x be Point of X; ::_thesis: ||.(- x).|| = ||.x.||
A1: abs (- 1) = - (- 1) by ABSVALUE:def_1;
||.(- x).|| = ||.((- 1) * x).|| by RLVECT_1:16
.= 1 * ||.x.|| by A1, Th27 ;
hence  ||.(- x).|| = ||.x.|| ; ::_thesis: verum
end;

theorem Th32: :: BHSP_1:32
for X being RealUnitarySpace
for x, y being Point of X holds ||.x.|| - ||.y.|| <= ||.(x - y).||
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds ||.x.|| - ||.y.|| <= ||.(x - y).||
let x, y be Point of X; ::_thesis: ||.x.|| - ||.y.|| <= ||.(x - y).||
(x - y) + y = x - (y - y) by RLVECT_1:29
.= x - H1(X) by RLVECT_1:15
.= x by RLVECT_1:13 ;
then  ||.x.|| <= ||.(x - y).|| + ||.y.|| by Th30;
hence  ||.x.|| - ||.y.|| <= ||.(x - y).|| by XREAL_1:20; ::_thesis: verum
end;

theorem :: BHSP_1:33
for X being RealUnitarySpace
for x, y being Point of X holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
let x, y be Point of X; ::_thesis: abs (||.x.|| - ||.y.||) <= ||.(x - y).||
(y - x) + x = y - (x - x) by RLVECT_1:29
.= y - H1(X) by RLVECT_1:15
.= y by RLVECT_1:13 ;
then  ||.y.|| <= ||.(y - x).|| + ||.x.|| by Th30;
then  ||.y.|| - ||.x.|| <= ||.(y - x).|| by XREAL_1:20;
then  ||.y.|| - ||.x.|| <= ||.(- (x - y)).|| by RLVECT_1:33;
then  ||.y.|| - ||.x.|| <= ||.(x - y).|| by Th31;
then A1: - ||.(x - y).|| <= - (||.y.|| - ||.x.||) by XREAL_1:24;
 ||.x.|| - ||.y.|| <= ||.(x - y).|| by Th32;
hence  abs (||.x.|| - ||.y.||) <= ||.(x - y).|| by A1, ABSVALUE:5; ::_thesis: verum
end;

definition
let X be RealUnitarySpace;
let x, y be Point of X;
func dist (x,y) ->  Real equals :: BHSP_1:def 5
||.(x - y).||;
correctness
coherence
||.(x - y).|| is Real;
;
commutativity
 for b1 being Real
for x, y being Point of X st b1 = ||.(x - y).|| holds
b1 = ||.(y - x).||
proof
let IT be Real; ::_thesis: for x, y being Point of X st IT = ||.(x - y).|| holds
IT = ||.(y - x).||
let x, y be Point of X; ::_thesis: ( IT = ||.(x - y).|| implies IT = ||.(y - x).|| )
||.(x - y).|| = ||.(- (y - x)).|| by RLVECT_1:33
.= ||.(y - x).|| by Th31 ;
hence  ( IT = ||.(x - y).|| implies IT = ||.(y - x).|| ) ; ::_thesis: verum
end;
end;

:: deftheorem  defines dist BHSP_1:def_5_:_
 for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) = ||.(x - y).||;

theorem Th34: :: BHSP_1:34
for X being RealUnitarySpace
for x being Point of X holds dist (x,x) = 0
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X holds dist (x,x) = 0
let x be Point of X; ::_thesis: dist (x,x) = 0
thus  dist (x,x) = ||.H1(X).|| by RLVECT_1:15
.= 0 by Th26 ; ::_thesis: verum
end;

theorem :: BHSP_1:35
for X being RealUnitarySpace
for x, z, y being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))
proof
let X be RealUnitarySpace; ::_thesis: for x, z, y being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))
let x, z, y be Point of X; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
dist (x,z) = ||.((x - z) + H1(X)).|| by RLVECT_1:4
.= ||.((x - z) + (y - y)).|| by RLVECT_1:15
.= ||.(x - (z - (y - y))).|| by RLVECT_1:29
.= ||.(x - (y + (z - y))).|| by RLVECT_1:29
.= ||.((x - y) - (z - y)).|| by RLVECT_1:27
.= ||.((x - y) + (y - z)).|| by RLVECT_1:33 ;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by Th30; ::_thesis: verum
end;

theorem Th36: :: BHSP_1:36
for X being RealUnitarySpace
for x, y being Point of X holds
( x <> y iff dist (x,y) <> 0 )
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds
( x <> y iff dist (x,y) <> 0 )
let x, y be Point of X; ::_thesis: ( x <> y iff dist (x,y) <> 0 )
thus  ( x <> y implies dist (x,y) <> 0 ) ::_thesis: ( dist (x,y) <> 0 implies x <> y )
proof
assume that
A1: x <> y and
A2: dist (x,y) = 0 ; ::_thesis: contradiction
 x - y = H1(X) by A2, Th26;
hence  contradiction by A1, RLVECT_1:21; ::_thesis: verum
end;
thus  ( dist (x,y) <> 0 implies x <> y ) by Th34; ::_thesis: verum
end;

theorem :: BHSP_1:37
for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) >= 0 by Th28;

theorem :: BHSP_1:38
for X being RealUnitarySpace
for x, y being Point of X holds
( x <> y iff dist (x,y) > 0 )
proof
let X be RealUnitarySpace; ::_thesis: for x, y being Point of X holds
( x <> y iff dist (x,y) > 0 )
let x, y be Point of X; ::_thesis: ( x <> y iff dist (x,y) > 0 )
thus  ( x <> y implies dist (x,y) > 0 ) ::_thesis: ( dist (x,y) > 0 implies x <> y )
proof
assume  x <> y ; ::_thesis: dist (x,y) > 0
then  dist (x,y) <> 0 by Th36;
hence  dist (x,y) > 0 by Th28; ::_thesis: verum
end;
thus  ( dist (x,y) > 0 implies x <> y ) by Th34; ::_thesis: verum
end;

theorem :: BHSP_1:39
for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) = sqrt ((x - y) .|. (x - y)) ;

theorem :: BHSP_1:40
for X being RealUnitarySpace
for x, y, u, v being Point of X holds dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v))
proof
let X be RealUnitarySpace; ::_thesis: for x, y, u, v being Point of X holds dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v))
let x, y, u, v be Point of X; ::_thesis: dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v))
dist ((x + y),(u + v)) = ||.(((- u) + (- v)) + (x + y)).|| by RLVECT_1:31
.= ||.((x + ((- u) + (- v))) + y).|| by RLVECT_1:def_3
.= ||.(((x - u) + (- v)) + y).|| by RLVECT_1:def_3
.= ||.((x - u) + (y - v)).|| by RLVECT_1:def_3 ;
hence  dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v)) by Th30; ::_thesis: verum
end;

theorem :: BHSP_1:41
for X being RealUnitarySpace
for x, y, u, v being Point of X holds dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v))
proof
let X be RealUnitarySpace; ::_thesis: for x, y, u, v being Point of X holds dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v))
let x, y, u, v be Point of X; ::_thesis: dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v))
dist ((x - y),(u - v)) = ||.(((x - y) - u) + v).|| by RLVECT_1:29
.= ||.((x - (u + y)) + v).|| by RLVECT_1:27
.= ||.(((x - u) - y) + v).|| by RLVECT_1:27
.= ||.((x - u) - (y - v)).|| by RLVECT_1:29
.= ||.((x - u) + (- (y - v))).|| ;
then  dist ((x - y),(u - v)) <= ||.(x - u).|| + ||.(- (y - v)).|| by Th30;
hence  dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v)) by Th31; ::_thesis: verum
end;

theorem :: BHSP_1:42
for X being RealUnitarySpace
for x, z, y being Point of X holds dist ((x - z),(y - z)) = dist (x,y)
proof
let X be RealUnitarySpace; ::_thesis: for x, z, y being Point of X holds dist ((x - z),(y - z)) = dist (x,y)
let x, z, y be Point of X; ::_thesis: dist ((x - z),(y - z)) = dist (x,y)
thus  dist ((x - z),(y - z)) = ||.(((x - z) - y) + z).|| by RLVECT_1:29
.= ||.((x - (y + z)) + z).|| by RLVECT_1:27
.= ||.(((x - y) - z) + z).|| by RLVECT_1:27
.= ||.((x - y) - (z - z)).|| by RLVECT_1:29
.= ||.((x - y) - H1(X)).|| by RLVECT_1:15
.= dist (x,y) by RLVECT_1:13 ; ::_thesis: verum
end;

theorem :: BHSP_1:43
for X being RealUnitarySpace
for x, z, y being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))
proof
let X be RealUnitarySpace; ::_thesis: for x, z, y being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))
let x, z, y be Point of X; ::_thesis: dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))
dist ((x - z),(y - z)) = ||.((x - z) + (z - y)).|| by RLVECT_1:33
.= ||.((- (z - x)) + (z - y)).|| by RLVECT_1:33 ;
then  dist ((x - z),(y - z)) <= ||.(- (z - x)).|| + ||.(z - y).|| by Th30;
hence  dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y)) by Th31; ::_thesis: verum
end;


definition
let X be non empty addLoopStr ;
let seq be sequence of X;
let x be Point of X;
funcseq + x ->  sequence of X means :Def6: :: BHSP_1:def 6
 for n being Element of NAT holds it . n = (seq . n) + x;
existence
 ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (seq . n) + x
proof
deffunc H2( Element of NAT ) ->  Element of the carrier of X = (seq . $1) + x;
 ex seq being sequence of X st
for n being Element of NAT holds seq . n = H2(n) from FUNCT_2:sch_4();
hence  ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (seq . n) + x ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (seq . n) + x ) & ( for n being Element of NAT holds b2 . n = (seq . n) + x ) holds
b1 = b2
proof
let seq1, seq2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = (seq . n) + x ) & ( for n being Element of NAT holds seq2 . n = (seq . n) + x ) implies seq1 = seq2 )
assume that
A1: for n being Element of NAT holds seq1 . n = (seq . n) + x and
A2: for n being Element of NAT holds seq2 . n = (seq . n) + x ; ::_thesis: seq1 = seq2
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: seq1 . n = seq2 . n
 seq1 . n = (seq . n) + x by A1;
hence  seq1 . n = seq2 . n by A2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines + BHSP_1:def_6_:_
 for X being non empty addLoopStr
for seq being sequence of X
for x being Point of X
for b4 being sequence of X holds
( b4 = seq + x iff for n being Element of NAT holds b4 . n = (seq . n) + x );

theorem Th44: :: BHSP_1:44
for n being Element of NAT
for X being non empty addLoopStr
for seq being sequence of X holds (- seq) . n = - (seq . n)
proof
let n be Element of NAT ; ::_thesis: for X being non empty addLoopStr
for seq being sequence of X holds (- seq) . n = - (seq . n)
let X be non empty addLoopStr ; ::_thesis: for seq being sequence of X holds (- seq) . n = - (seq . n)
let seq be sequence of X; ::_thesis: (- seq) . n = - (seq . n)
A1: dom (- seq) = NAT by FUNCT_2:def_1;
thus (- seq) . n = (- seq) /. n
.= - (seq /. n) by A1, VFUNCT_1:def_5
.= - (seq . n) ; ::_thesis: verum
end;

definition
let X be RealUnitarySpace;
let seq1, seq2 be sequence of X;
:: original: +
redefine funcseq1 + seq2 ->  Element of bool [:NAT, the carrier of X:];
commutativity
 for seq1, seq2 being sequence of X holds seq1 + seq2 = seq2 + seq1
proof
let seq1, seq2 be sequence of X; ::_thesis: seq1 + seq2 = seq2 + seq1
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (seq1 + seq2) . n = (seq2 + seq1) . n
thus (seq1 + seq2) . n = (seq2 . n) + (seq1 . n) by NORMSP_1:def_2
.= (seq2 + seq1) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
end;

theorem :: BHSP_1:45
for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3
proof
let X be RealUnitarySpace; ::_thesis: for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3
let seq1, seq2, seq3 be sequence of X; ::_thesis: seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (seq1 + (seq2 + seq3)) . n = ((seq1 + seq2) + seq3) . n
thus (seq1 + (seq2 + seq3)) . n = (seq1 . n) + ((seq2 + seq3) . n) by NORMSP_1:def_2
.= (seq1 . n) + ((seq2 . n) + (seq3 . n)) by NORMSP_1:def_2
.= ((seq1 . n) + (seq2 . n)) + (seq3 . n) by RLVECT_1:def_3
.= ((seq1 + seq2) . n) + (seq3 . n) by NORMSP_1:def_2
.= ((seq1 + seq2) + seq3) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;

theorem :: BHSP_1:46
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant holds
seq1 + seq2 is constant
proof
let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant holds
seq1 + seq2 is constant
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is constant & seq2 is constant implies seq1 + seq2 is constant )
assume that
A1: seq1 is constant and
A2: seq2 is constant ; ::_thesis: seq1 + seq2 is constant
set seq = seq1 + seq2;
consider x being Point of X such that
A3: for n being Nat holds seq1 . n = x by A1, VALUED_0:def_18;
consider y being Point of X such that
A4: for n being Nat holds seq2 . n = y by A2, VALUED_0:def_18;
take z = x + y; :: according to VALUED_0:def_20 ::_thesis: for b1 being set holds (seq1 + seq2) . b1 = z
let n be Nat; ::_thesis: (seq1 + seq2) . n = z
 n in NAT by ORDINAL1:def_12;
hence (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) by NORMSP_1:def_2
.= x + (seq2 . n) by A3
.= z by A4 ;
::_thesis: verum
end;

theorem :: BHSP_1:47
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant holds
seq1 - seq2 is constant
proof
let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant holds
seq1 - seq2 is constant
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is constant & seq2 is constant implies seq1 - seq2 is constant )
assume that
A1: seq1 is constant and
A2: seq2 is constant ; ::_thesis: seq1 - seq2 is constant
set seq = seq1 - seq2;
consider x being Point of X such that
A3: for n being Nat holds seq1 . n = x by A1, VALUED_0:def_18;
consider y being Point of X such that
A4: for n being Nat holds seq2 . n = y by A2, VALUED_0:def_18;
take z = x - y; :: according to VALUED_0:def_20 ::_thesis: for b1 being set holds (seq1 - seq2) . b1 = z
let n be Nat; ::_thesis: (seq1 - seq2) . n = z
 n in NAT by ORDINAL1:def_12;
hence (seq1 - seq2) . n = (seq1 . n) - (seq2 . n) by NORMSP_1:def_3
.= x - (seq2 . n) by A3
.= z by A4 ;
::_thesis: verum
end;

theorem :: BHSP_1:48
for a being Real
for X being RealUnitarySpace
for seq1 being sequence of X st seq1 is constant holds
a * seq1 is constant
proof
let a be Real; ::_thesis: for X being RealUnitarySpace
for seq1 being sequence of X st seq1 is constant holds
a * seq1 is constant
let X be RealUnitarySpace; ::_thesis: for seq1 being sequence of X st seq1 is constant holds
a * seq1 is constant
let seq1 be sequence of X; ::_thesis: ( seq1 is constant implies a * seq1 is constant )
assume A1: seq1 is constant ; ::_thesis: a * seq1 is constant
set seq = a * seq1;
consider x being Point of X such that
A2: for n being Nat holds seq1 . n = x by A1, VALUED_0:def_18;
take z = a * x; :: according to VALUED_0:def_20 ::_thesis: for b1 being set holds (a * seq1) . b1 = z
let n be Nat; ::_thesis: (a * seq1) . n = z
 n in NAT by ORDINAL1:def_12;
hence (a * seq1) . n = a * (seq1 . n) by NORMSP_1:def_5
.= z by A2 ;
::_thesis: verum
end;

theorem :: BHSP_1:49
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2)
proof
let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2)
let seq1, seq2 be sequence of X; ::_thesis: seq1 - seq2 = seq1 + (- seq2)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (seq1 - seq2) . n = (seq1 + (- seq2)) . n
thus (seq1 - seq2) . n = (seq1 . n) - (seq2 . n) by NORMSP_1:def_3
.= (seq1 . n) + ((- seq2) . n) by Th44
.= (seq1 + (- seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;

theorem :: BHSP_1:50
for X being RealUnitarySpace
for seq being sequence of X holds seq = seq + (0. X)
proof
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds seq = seq + (0. X)
let seq be sequence of X; ::_thesis: seq = seq + (0. X)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: seq . n = (seq + (0. X)) . n
thus (seq + H1(X)) . n = (seq . n) + H1(X) by Def6
.= seq . n by RLVECT_1:4 ; ::_thesis: verum
end;

theorem :: BHSP_1:51
for a being Real
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2)
proof
let a be Real; ::_thesis: for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2)
let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2)
let seq1, seq2 be sequence of X; ::_thesis: a * (seq1 + seq2) = (a * seq1) + (a * seq2)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (a * (seq1 + seq2)) . n = ((a * seq1) + (a * seq2)) . n
thus (a * (seq1 + seq2)) . n = a * ((seq1 + seq2) . n) by NORMSP_1:def_5
.= a * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def_2
.= (a * (seq1 . n)) + (a * (seq2 . n)) by RLVECT_1:def_5
.= ((a * seq1) . n) + (a * (seq2 . n)) by NORMSP_1:def_5
.= ((a * seq1) . n) + ((a * seq2) . n) by NORMSP_1:def_5
.= ((a * seq1) + (a * seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;

theorem :: BHSP_1:52
for a, b being Real
for X being RealUnitarySpace
for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq)
proof
let a, b be Real; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq)
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq)
let seq be sequence of X; ::_thesis: (a + b) * seq = (a * seq) + (b * seq)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((a + b) * seq) . n = ((a * seq) + (b * seq)) . n
thus ((a + b) * seq) . n = (a + b) * (seq . n) by NORMSP_1:def_5
.= (a * (seq . n)) + (b * (seq . n)) by RLVECT_1:def_6
.= ((a * seq) . n) + (b * (seq . n)) by NORMSP_1:def_5
.= ((a * seq) . n) + ((b * seq) . n) by NORMSP_1:def_5
.= ((a * seq) + (b * seq)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;

theorem :: BHSP_1:53
for a, b being Real
for X being RealUnitarySpace
for seq being sequence of X holds (a * b) * seq = a * (b * seq)
proof
let a, b be Real; ::_thesis: for X being RealUnitarySpace
for seq being sequence of X holds (a * b) * seq = a * (b * seq)
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds (a * b) * seq = a * (b * seq)
let seq be sequence of X; ::_thesis: (a * b) * seq = a * (b * seq)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((a * b) * seq) . n = (a * (b * seq)) . n
thus ((a * b) * seq) . n = (a * b) * (seq . n) by NORMSP_1:def_5
.= a * (b * (seq . n)) by RLVECT_1:def_7
.= a * ((b * seq) . n) by NORMSP_1:def_5
.= (a * (b * seq)) . n by NORMSP_1:def_5 ; ::_thesis: verum
end;

theorem :: BHSP_1:54
for X being RealUnitarySpace
for seq being sequence of X holds 1 * seq = seq
proof
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds 1 * seq = seq
let seq be sequence of X; ::_thesis: 1 * seq = seq
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (1 * seq) . n = seq . n
thus (1 * seq) . n = 1 * (seq . n) by NORMSP_1:def_5
.= seq . n by RLVECT_1:def_8 ; ::_thesis: verum
end;

theorem :: BHSP_1:55
for X being RealUnitarySpace
for seq being sequence of X holds (- 1) * seq = - seq
proof
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds (- 1) * seq = - seq
let seq be sequence of X; ::_thesis: (- 1) * seq = - seq
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((- 1) * seq) . n = (- seq) . n
thus ((- 1) * seq) . n = (- 1) * (seq . n) by NORMSP_1:def_5
.= - (seq . n) by RLVECT_1:16
.= (- seq) . n by Th44 ; ::_thesis: verum
end;

theorem :: BHSP_1:56
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X holds seq - x = seq + (- x)
proof
let X be RealUnitarySpace; ::_thesis: for x being Point of X
for seq being sequence of X holds seq - x = seq + (- x)
let x be Point of X; ::_thesis: for seq being sequence of X holds seq - x = seq + (- x)
let seq be sequence of X; ::_thesis: seq - x = seq + (- x)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (seq - x) . n = (seq + (- x)) . n
thus (seq - x) . n = (seq . n) - x by NORMSP_1:def_4
.= (seq + (- x)) . n by Def6 ; ::_thesis: verum
end;

theorem :: BHSP_1:57
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1)
proof
let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1)
let seq1, seq2 be sequence of X; ::_thesis: seq1 - seq2 = - (seq2 - seq1)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (seq1 - seq2) . n = (- (seq2 - seq1)) . n
thus (seq1 - seq2) . n = (seq1 . n) - (seq2 . n) by NORMSP_1:def_3
.= - ((seq2 . n) - (seq1 . n)) by RLVECT_1:33
.= - ((seq2 - seq1) . n) by NORMSP_1:def_3
.= (- (seq2 - seq1)) . n by Th44 ; ::_thesis: verum
end;

theorem :: BHSP_1:58
for X being RealUnitarySpace
for seq being sequence of X holds seq = seq - (0. X)
proof
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds seq = seq - (0. X)
let seq be sequence of X; ::_thesis: seq = seq - (0. X)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: seq . n = (seq - (0. X)) . n
thus (seq - H1(X)) . n = (seq . n) - H1(X) by NORMSP_1:def_4
.= seq . n by RLVECT_1:13 ; ::_thesis: verum
end;

theorem :: BHSP_1:59
for X being RealUnitarySpace
for seq being sequence of X holds seq = - (- seq)
proof
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds seq = - (- seq)
let seq be sequence of X; ::_thesis: seq = - (- seq)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: seq . n = (- (- seq)) . n
thus (- (- seq)) . n = - ((- seq) . n) by Th44
.= - (- (seq . n)) by Th44
.= seq . n by RLVECT_1:17 ; ::_thesis: verum
end;

theorem :: BHSP_1:60
for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proof
let X be RealUnitarySpace; ::_thesis: for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
let seq1, seq2, seq3 be sequence of X; ::_thesis: seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (seq1 - (seq2 + seq3)) . n = ((seq1 - seq2) - seq3) . n
thus (seq1 - (seq2 + seq3)) . n = (seq1 . n) - ((seq2 + seq3) . n) by NORMSP_1:def_3
.= (seq1 . n) - ((seq2 . n) + (seq3 . n)) by NORMSP_1:def_2
.= ((seq1 . n) - (seq2 . n)) - (seq3 . n) by RLVECT_1:27
.= ((seq1 - seq2) . n) - (seq3 . n) by NORMSP_1:def_3
.= ((seq1 - seq2) - seq3) . n by NORMSP_1:def_3 ; ::_thesis: verum
end;

theorem :: BHSP_1:61
for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)
proof
let X be RealUnitarySpace; ::_thesis: for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)
let seq1, seq2, seq3 be sequence of X; ::_thesis: (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((seq1 + seq2) - seq3) . n = (seq1 + (seq2 - seq3)) . n
thus ((seq1 + seq2) - seq3) . n = ((seq1 + seq2) . n) - (seq3 . n) by NORMSP_1:def_3
.= ((seq1 . n) + (seq2 . n)) - (seq3 . n) by NORMSP_1:def_2
.= (seq1 . n) + ((seq2 . n) - (seq3 . n)) by RLVECT_1:def_3
.= (seq1 . n) + ((seq2 - seq3) . n) by NORMSP_1:def_3
.= (seq1 + (seq2 - seq3)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;

theorem :: BHSP_1:62
for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proof
let X be RealUnitarySpace; ::_thesis: for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
let seq1, seq2, seq3 be sequence of X; ::_thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (seq1 - (seq2 - seq3)) . n = ((seq1 - seq2) + seq3) . n
thus (seq1 - (seq2 - seq3)) . n = (seq1 . n) - ((seq2 - seq3) . n) by NORMSP_1:def_3
.= (seq1 . n) - ((seq2 . n) - (seq3 . n)) by NORMSP_1:def_3
.= ((seq1 . n) - (seq2 . n)) + (seq3 . n) by RLVECT_1:29
.= ((seq1 - seq2) . n) + (seq3 . n) by NORMSP_1:def_3
.= ((seq1 - seq2) + seq3) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;

theorem :: BHSP_1:63
for a being Real
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)
proof
let a be Real; ::_thesis: for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)
let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)
let seq1, seq2 be sequence of X; ::_thesis: a * (seq1 - seq2) = (a * seq1) - (a * seq2)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (a * (seq1 - seq2)) . n = ((a * seq1) - (a * seq2)) . n
thus (a * (seq1 - seq2)) . n = a * ((seq1 - seq2) . n) by NORMSP_1:def_5
.= a * ((seq1 . n) - (seq2 . n)) by NORMSP_1:def_3
.= (a * (seq1 . n)) - (a * (seq2 . n)) by RLVECT_1:34
.= ((a * seq1) . n) - (a * (seq2 . n)) by NORMSP_1:def_5
.= ((a * seq1) . n) - ((a * seq2) . n) by NORMSP_1:def_5
.= ((a * seq1) - (a * seq2)) . n by NORMSP_1:def_3 ; ::_thesis: verum
end;