:: BHSP_1 semantic presentation

definition
attr a1 is strict;
struct UNITSTR -> RLSStruct ;
aggr UNITSTR(# carrier, Zero, add, Mult, scalar #) -> UNITSTR ;
sel scalar c1 -> Function of [:the carrier of a1,the carrier of a1:], REAL ;
end;

registration
cluster non empty strict UNITSTR ;
existence
ex b1 being UNITSTR st
( not b1 is empty & b1 is strict )
proof
consider c1 being non empty set , c2 being Element of c1, c3 being BinOp of c1, c4 being Function of [:REAL ,c1:],c1, c5 being Function of [:c1,c1:], REAL ;
take UNITSTR(# c1,c2,c3,c4,c5 #) ;
thus not the carrier of UNITSTR(# c1,c2,c3,c4,c5 #) is empty ; :: according to STRUCT_0:def 1
thus UNITSTR(# c1,c2,c3,c4,c5 #) is strict ;
end;
end;

registration
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be BinOp of c1;
let c4 be Function of [:REAL ,c1:],c1;
let c5 be Function of [:c1,c1:], REAL ;
cluster UNITSTR(# a1,a2,a3,a4,a5 #) -> non empty ;
coherence
not UNITSTR(# c1,c2,c3,c4,c5 #) is empty
proof
thus not the carrier of UNITSTR(# c1,c2,c3,c4,c5 #) is empty ; :: according to STRUCT_0:def 1
end;
end;

deffunc H1( UNITSTR ) -> Element of the carrier of a1 = 0. a1;

definition
let c1 be non empty UNITSTR ;
let c2, c3 be Point of c1;
func c2 .|. c3 -> Real equals :: BHSP_1:def 1
the scalar of a1 . [a2,a3];
correctness
coherence
the scalar of c1 . [c2,c3] is Real;
;
end;

:: deftheorem defines .|. BHSP_1:def 1 :
for b1 being non empty UNITSTR
for b2, b3 being Point of b1 holds b2 .|. b3 = the scalar of b1 . [b2,b3];

consider c1 being RealLinearSpace;

E1: the carrier of ((0). c1) = {(0. c1)}
by RLSUB_1:def 3;

reconsider c2 = [:the carrier of ((0). c1),the carrier of ((0). c1):] --> 0 as Function of [:the carrier of ((0). c1),the carrier of ((0). c1):], REAL by FUNCOP_1:57;

E2: for b1, b2 being VECTOR of ((0). c1) holds c2 . [b1,b2] = 0
by FUNCOP_1:13;

0. c1 in the carrier of ((0). c1)
by E1, TARSKI:def 1;

then E3: c2 . [(0. c1),(0. c1)] = 0
by E2;

E4: for b1, b2 being VECTOR of ((0). c1) holds c2 . [b1,b2] = c2 . [b2,b1]
proof
let c3, c4 be VECTOR of ((0). c1);
( c3 = 0. c1 & c4 = 0. c1 ) by E1, TARSKI:def 1;
hence c2 . [c3,c4] = c2 . [c4,c3] ;
end;

E5: for b1, b2, b3 being VECTOR of ((0). c1) holds c2 . [(b1 + b2),b3] = (c2 . [b1,b3]) + (c2 . [b2,b3])
proof
let c3, c4, c5 be VECTOR of ((0). c1);
( c3 = 0. c1 & c4 = 0. c1 & c5 = 0. c1 ) by E1, TARSKI:def 1;
hence c2 . [(c3 + c4),c5] = (c2 . [c3,c5]) + (c2 . [c4,c5]) by E1, E3, TARSKI:def 1;
end;

E6: for b1, b2 being VECTOR of ((0). c1)
for b3 being Real holds c2 . [(b3 * b1),b2] = b3 * (c2 . [b1,b2])
proof
let c3, c4 be VECTOR of ((0). c1);
let c5 be Real;
( c3 = 0. c1 & c4 = 0. c1 ) by E1, TARSKI:def 1;
hence c2 . [(c5 * c3),c4] = c5 * (c2 . [c3,c4]) by E1, E3, TARSKI:def 1;
end;

set c3 = UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);

E7: now
let c4, c5, c6 be Point of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
let c7 be Real;
thus ( c4 .|. c4 = 0 iff c4 = H1( UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)) )
proof
H1( UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)) = the Zero of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)
.= 0. ((0). c1)
.= 0. c1 by RLSUB_1:19 ;
hence ( c4 .|. c4 = 0 iff c4 = H1( UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)) ) by E1, E3, TARSKI:def 1;
end;
thus 0 <= c4 .|. c4 by FUNCOP_1:13;
thus c4 .|. c5 = c5 .|. c4 by E4;
thus (c4 + c5) .|. c6 = (c4 .|. c6) + (c5 .|. c6)
proof
reconsider c8 = c4, c9 = c5, c10 = c6 as VECTOR of ((0). c1) ;
( (c4 + c5) .|. c6 = c2 . [(c8 + c9),c10] & c4 .|. c6 = c2 . [c8,c10] & c5 .|. c6 = c2 . [c9,c10] ) ;
hence (c4 + c5) .|. c6 = (c4 .|. c6) + (c5 .|. c6) by E5;
end;
thus (c7 * c4) .|. c5 = c7 * (c4 .|. c5)
proof
reconsider c8 = c4, c9 = c5 as VECTOR of ((0). c1) ;
( (c7 * c4) .|. c5 = c2 . [(c7 * c8),c9] & c4 .|. c5 = c2 . [c8,c9] ) ;
hence (c7 * c4) .|. c5 = c7 * (c4 .|. c5) by E6;
end;
end;

definition
let c4 be non empty UNITSTR ;
attr a1 is RealUnitarySpace-like means :E8: :: BHSP_1:def 2
for b1, b2, b3 being Point of a1
for b4 being Real holds
( ( b1 .|. b1 = 0 implies b1 = 0. a1 ) & ( b1 = 0. a1 implies b1 .|. b1 = 0 ) & 0 <= b1 .|. b1 & b1 .|. b2 = b2 .|. b1 & (b1 + b2) .|. b3 = (b1 .|. b3) + (b2 .|. b3) & (b4 * b1) .|. b2 = b4 * (b1 .|. b2) );
end;

:: deftheorem E8 defines RealUnitarySpace-like BHSP_1:def 2 :
for b1 being non empty UNITSTR holds
( b1 is RealUnitarySpace-like iff for b2, b3, b4 being Point of b1
for b5 being Real holds
( ( b2 .|. b2 = 0 implies b2 = 0. b1 ) & ( b2 = 0. b1 implies b2 .|. b2 = 0 ) & 0 <= b2 .|. b2 & b2 .|. b3 = b3 .|. b2 & (b2 + b3) .|. b4 = (b2 .|. b4) + (b3 .|. b4) & (b5 * b2) .|. b3 = b5 * (b2 .|. b3) ) );

registration
cluster non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like strict RealUnitarySpace-like UNITSTR ;
existence
ex b1 being non empty UNITSTR st
( b1 is RealUnitarySpace-like & b1 is RealLinearSpace-like & 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). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) ;
thus UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) is RealUnitarySpace-like by E8, E7;
E9: for b1, b2 being VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)
for b3, b4 being VECTOR of ((0). c1) holds
( ( b1 = b3 & b2 = b4 ) implies ( ( b1 + b2 = b3 + b4 & ( for b5 being Real holds b5 * b1 = b5 * b3 ) ) ) ) ;
thus UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) is RealLinearSpace-like
proof
thus for b1 being Real
for b2, b3 being VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) holds b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) :: according to RLVECT_1:def 9
proof
let c4 be Real;
let c5, c6 be VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
reconsider c7 = c5, c8 = c6 as VECTOR of ((0). c1) ;
thus c4 * (c5 + c6) = c4 * (c7 + c8)
.= (c4 * c7) + (c4 * c8) by RLVECT_1:def 9
.= (c4 * c5) + (c4 * c6) ;
end;
thus for b1, b2 being Real
for b3 being VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) holds (b1 + b2) * b3 = (b1 * b3) + (b2 * b3)
proof
let c4, c5 be Real;
let c6 be VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
reconsider c7 = c6 as VECTOR of ((0). c1) ;
thus (c4 + c5) * c6 = (c4 + c5) * c7
.= (c4 * c7) + (c5 * c7) by RLVECT_1:def 9
.= (c4 * c6) + (c5 * c6) ;
end;
thus for b1, b2 being Real
for b3 being VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) holds (b1 * b2) * b3 = b1 * (b2 * b3)
proof
let c4, c5 be Real;
let c6 be VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
reconsider c7 = c6 as VECTOR of ((0). c1) ;
thus (c4 * c5) * c6 = (c4 * c5) * c7
.= c4 * (c5 * c7) by RLVECT_1:def 9
.= c4 * (c5 * c6) ;
end;
let c4 be VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
reconsider c5 = c4 as VECTOR of ((0). c1) ;
thus 1 * c4 = 1 * c5
.= c4 by RLVECT_1:def 9 ;
end;
thus for b1, b2 being VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) holds b1 + b2 = b2 + b1 :: according to RLVECT_1:def 5
proof
let c4, c5 be VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
reconsider c6 = c4, c7 = c5 as VECTOR of ((0). c1) ;
thus c4 + c5 = c7 + c6 by E9
.= c5 + c4 ;
end;
thus for b1, b2, b3 being VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) holds (b1 + b2) + b3 = b1 + (b2 + b3) :: according to RLVECT_1:def 6
proof
let c4, c5, c6 be VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
reconsider c7 = c4, c8 = c5, c9 = c6 as VECTOR of ((0). c1) ;
thus (c4 + c5) + c6 = (c7 + c8) + c9
.= c7 + (c8 + c9) by RLVECT_1:def 6
.= c4 + (c5 + c6) ;
end;
thus for b1 being VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) holds b1 + (0. UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)) = b1 :: according to RLVECT_1:def 7
proof
let c4 be VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
reconsider c5 = c4 as VECTOR of ((0). c1) ;
thus c4 + (0. UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #)) = c5 + (0. ((0). c1))
.= c4 by RLVECT_1:10 ;
end;
thus for b1 being VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) holds
ex b2 being VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) st b1 + b2 = 0. UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) :: according to RLVECT_1:def 8
proof
let c4 be VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
reconsider c5 = c4 as VECTOR of ((0). c1) ;
consider c6 being VECTOR of ((0). c1) such that
E10: c5 + c6 = 0. ((0). c1) by RLVECT_1:def 8;
reconsider c7 = c6 as VECTOR of UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) ;
take c7 ;
thus c4 + c7 = 0. UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) by E10;
end;
thus UNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #) is strict ;
end;
end;

definition
mode RealUnitarySpace is non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealUnitarySpace-like UNITSTR ;
end;

definition
let c4 be RealUnitarySpace;
let c5, c6 be Point of c4;
redefine func .|. as c2 .|. c3 -> Real;
commutativity
for b1, b2 being Point of c4 holds b1 .|. b2 = b2 .|. b1 by E8;
end;

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
for b1 being RealUnitarySpace holds (0. b1) .|. (0. b1) = 0 by E8;

theorem :: BHSP_1:7
for b1 being RealUnitarySpace
for b2, b3, b4 being Point of b1 holds b2 .|. (b3 + b4) = (b2 .|. b3) + (b2 .|. b4) by E8;

theorem :: BHSP_1:8
for b1 being Real
for b2 being RealUnitarySpace
for b3, b4 being Point of b2 holds b3 .|. (b1 * b4) = b1 * (b3 .|. b4) by E8;

theorem :: BHSP_1:9
for b1 being Real
for b2 being RealUnitarySpace
for b3, b4 being Point of b2 holds (b1 * b3) .|. b4 = b3 .|. (b1 * b4)
proof
let c4 be Real;
let c5 be RealUnitarySpace;
let c6, c7 be Point of c5;
(c4 * c6) .|. c7 = c4 * (c6 .|. c7) by E8;
hence (c4 * c6) .|. c7 = c6 .|. (c4 * c7) by E8;
end;

theorem E9: :: BHSP_1:10
for b1, b2 being Real
for b3 being RealUnitarySpace
for b4, b5, b6 being Point of b3 holds ((b1 * b4) + (b2 * b5)) .|. b6 = (b1 * (b4 .|. b6)) + (b2 * (b5 .|. b6))
proof
let c4, c5 be Real;
let c6 be RealUnitarySpace;
let c7, c8, c9 be Point of c6;
((c4 * c7) + (c5 * c8)) .|. c9 = ((c4 * c7) .|. c9) + ((c5 * c8) .|. c9) by E8
.= (c4 * (c7 .|. c9)) + ((c5 * c8) .|. c9) by E8 ;
hence ((c4 * c7) + (c5 * c8)) .|. c9 = (c4 * (c7 .|. c9)) + (c5 * (c8 .|. c9)) by E8;
end;

theorem :: BHSP_1:11
for b1, b2 being Real
for b3 being RealUnitarySpace
for b4, b5, b6 being Point of b3 holds b4 .|. ((b1 * b5) + (b2 * b6)) = (b1 * (b4 .|. b5)) + (b2 * (b4 .|. b6)) by E9;

theorem :: BHSP_1:12
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds (- b2) .|. b3 = b2 .|. (- b3)
proof
let c4 be RealUnitarySpace;
let c5, c6 be Point of c4;
(- c5) .|. c6 = ((- 1) * c5) .|. c6 by RLVECT_1:29
.= (- 1) * (c5 .|. c6) by E8
.= c5 .|. ((- 1) * c6) by E8 ;
hence (- c5) .|. c6 = c5 .|. (- c6) by RLVECT_1:29;
end;

theorem E10: :: BHSP_1:13
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds (- b2) .|. b3 = - (b2 .|. b3)
proof
let c4 be RealUnitarySpace;
let c5, c6 be Point of c4;
(- c5) .|. c6 = ((- 1) * c5) .|. c6 by RLVECT_1:29
.= (- 1) * (c5 .|. c6) by E8 ;
hence (- c5) .|. c6 = - (c5 .|. c6) ;
end;

theorem :: BHSP_1:14
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds b2 .|. (- b3) = - (b2 .|. b3) by E10;

theorem E11: :: BHSP_1:15
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds (- b2) .|. (- b3) = b2 .|. b3
proof
let c4 be RealUnitarySpace;
let c5, c6 be Point of c4;
(- c5) .|. (- c6) = - (c5 .|. (- c6)) by E10
.= - (- (c5 .|. c6)) by E10 ;
hence (- c5) .|. (- c6) = c5 .|. c6 ;
end;

theorem E12: :: BHSP_1:16
for b1 being RealUnitarySpace
for b2, b3, b4 being Point of b1 holds (b2 - b3) .|. b4 = (b2 .|. b4) - (b3 .|. b4)
proof
let c4 be RealUnitarySpace;
let c5, c6, c7 be Point of c4;
(c5 - c6) .|. c7 = (c5 + (- c6)) .|. c7
.= (c5 .|. c7) + ((- c6) .|. c7) by E8
.= (c5 .|. c7) + (- (c6 .|. c7)) by E10 ;
hence (c5 - c6) .|. c7 = (c5 .|. c7) - (c6 .|. c7) ;
end;

theorem E13: :: BHSP_1:17
for b1 being RealUnitarySpace
for b2, b3, b4 being Point of b1 holds b2 .|. (b3 - b4) = (b2 .|. b3) - (b2 .|. b4)
proof
let c4 be RealUnitarySpace;
let c5, c6, c7 be Point of c4;
c5 .|. (c6 - c7) = c5 .|. (c6 + (- c7))
.= (c5 .|. c6) + (c5 .|. (- c7)) by E8
.= (c5 .|. c6) + (- (c5 .|. c7)) by E10 ;
hence c5 .|. (c6 - c7) = (c5 .|. c6) - (c5 .|. c7) ;
end;

theorem :: BHSP_1:18
for b1 being RealUnitarySpace
for b2, b3, b4, b5 being Point of b1 holds (b2 - b3) .|. (b4 - b5) = (((b2 .|. b4) - (b2 .|. b5)) - (b3 .|. b4)) + (b3 .|. b5)
proof
let c4 be RealUnitarySpace;
let c5, c6, c7, c8 be Point of c4;
(c5 - c6) .|. (c7 - c8) = (c5 .|. (c7 - c8)) - (c6 .|. (c7 - c8)) by E12
.= ((c5 .|. c7) - (c5 .|. c8)) - (c6 .|. (c7 - c8)) by E13
.= ((c5 .|. c7) - (c5 .|. c8)) - ((c6 .|. c7) - (c6 .|. c8)) by E13 ;
hence (c5 - c6) .|. (c7 - c8) = (((c5 .|. c7) - (c5 .|. c8)) - (c6 .|. c7)) + (c6 .|. c8) ;
end;

theorem E14: :: BHSP_1:19
for b1 being RealUnitarySpace
for b2 being Point of b1 holds (0. b1) .|. b2 = 0
proof
let c4 be RealUnitarySpace;
let c5 be Point of c4;
H1(c4) .|. c5 = (c5 + (- c5)) .|. c5 by RLVECT_1:16
.= (c5 .|. c5) + ((- c5) .|. c5) by E8
.= (c5 .|. c5) + (- (c5 .|. c5)) by E10 ;
hence (0. c4) .|. c5 = 0 ;
end;

theorem :: BHSP_1:20
for b1 being RealUnitarySpace
for b2 being Point of b1 holds b2 .|. (0. b1) = 0 by E14;

theorem E15: :: BHSP_1:21
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds (b2 + b3) .|. (b2 + b3) = ((b2 .|. b2) + (2 * (b2 .|. b3))) + (b3 .|. b3)
proof
let c4 be RealUnitarySpace;
let c5, c6 be Point of c4;
(c5 + c6) .|. (c5 + c6) = (c5 .|. (c5 + c6)) + (c6 .|. (c5 + c6)) by E8
.= ((c5 .|. c5) + (c5 .|. c6)) + (c6 .|. (c5 + c6)) by E8
.= ((c5 .|. c5) + (c5 .|. c6)) + ((c5 .|. c6) + (c6 .|. c6)) by E8
.= ((c5 .|. c5) + ((c5 .|. c6) + (c5 .|. c6))) + (c6 .|. c6) ;
hence (c5 + c6) .|. (c5 + c6) = ((c5 .|. c5) + (2 * (c5 .|. c6))) + (c6 .|. c6) ;
end;

theorem :: BHSP_1:22
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds (b2 + b3) .|. (b2 - b3) = (b2 .|. b2) - (b3 .|. b3)
proof
let c4 be RealUnitarySpace;
let c5, c6 be Point of c4;
(c5 + c6) .|. (c5 - c6) = (c5 .|. (c5 - c6)) + (c6 .|. (c5 - c6)) by E8
.= ((c5 .|. c5) - (c5 .|. c6)) + (c6 .|. (c5 - c6)) by E13
.= ((c5 .|. c5) - (c5 .|. c6)) + ((c5 .|. c6) - (c6 .|. c6)) by E13 ;
hence (c5 + c6) .|. (c5 - c6) = (c5 .|. c5) - (c6 .|. c6) ;
end;

theorem E16: :: BHSP_1:23
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds (b2 - b3) .|. (b2 - b3) = ((b2 .|. b2) - (2 * (b2 .|. b3))) + (b3 .|. b3)
proof
let c4 be RealUnitarySpace;
let c5, c6 be Point of c4;
(c5 - c6) .|. (c5 - c6) = (c5 .|. (c5 - c6)) - (c6 .|. (c5 - c6)) by E12
.= ((c5 .|. c5) - (c5 .|. c6)) - (c6 .|. (c5 - c6)) by E13
.= ((c5 .|. c5) - (c5 .|. c6)) - ((c5 .|. c6) - (c6 .|. c6)) by E13
.= ((c5 .|. c5) - ((c5 .|. c6) + (c5 .|. c6))) + (c6 .|. c6) ;
hence (c5 - c6) .|. (c5 - c6) = ((c5 .|. c5) - (2 * (c5 .|. c6))) + (c6 .|. c6) ;
end;

theorem E17: :: BHSP_1:24
for b1 being RealUnitarySpace
for b2, b3 being Point of b1 holds abs (b2 .|. b3) <= (sqrt (b2 .|. b2)) * (sqrt (b3 .|. b3))
proof
let c4 be RealUnitarySpace;
let c5, c6 be Point of c4;
E18: ( c5 = H1(c4) implies abs (c5 .|. c6) <= (sqrt (c5 .|. c5)) * (sqrt (c6 .|. c6)) )
proof
assume E19: c5 = H1(c4) ;
then E20: c5 .|. c6 = 0 by E14;
sqrt (c5 .|. c5) = 0 by E19, E8, SQUARE_1:82;
hence abs (c5 .|. c6) <= (sqrt (c5 .|. c5)) * (sqrt (c6 .|. c6)) by E20, ABSVALUE:7;
end;
( c5 <> H1(c4) implies abs (c5 .|. c6) <= (sqrt (c5 .|. c5)) * (sqrt (c6 .|. c6)) )
proof
assume c5 <> H1(c4) ;
then E19: c5 .|. c5 <> 0 by E8;
E20: c5 .|. c5 >= 0 by E8;
E21: for b1 being real number holds (((c5 .|. c5) * (b1 ^2 )) + ((2 * (c5 .|. c6)) * b1)) + (c6 .|. c6) >= 0
proof
let c7 be real number ;
reconsider c8 = c7 as Real by XREAL_0:def 1;
((c8 * c5) + c6) .|. ((c8 * c5) + c6) >= 0 by E8;
then (((c8 * c5) .|. (c8 * c5)) + (2 * ((c8 * c5) .|. c6))) + (c6 .|. c6) >= 0 by E15;
then ((c8 * (c5 .|. (c8 * c5))) + (2 * ((c8 * c5) .|. c6))) + (c6 .|. c6) >= 0 by E8;
then ((c8 * (c8 * (c5 .|. c5))) + (2 * ((c8 * c5) .|. c6))) + (c6 .|. c6) >= 0 by E8;
then (((c8 * c8) * (c5 .|. c5)) + (2 * ((c8 * c5) .|. c6))) + (c6 .|. c6) >= 0 ;
then (((c5 .|. c5) * (c8 ^2 )) + (2 * ((c8 * c5) .|. c6))) + (c6 .|. c6) >= 0 ;
then (((c5 .|. c5) * (c8 ^2 )) + (2 * ((c5 .|. c6) * c8))) + (c6 .|. c6) >= 0 by E8;
hence (((c5 .|. c5) * (c7 ^2 )) + ((2 * (c5 .|. c6)) * c7)) + (c6 .|. c6) >= 0 ;
end;
E22: (abs (c5 .|. c6)) ^2 >= 0 by XREAL_1:65;
E23: abs (c5 .|. c6) >= 0 by COMPLEX1:132;
E24: c6 .|. c6 >= 0 by E8;
delta (c5 .|. c5),(2 * (c5 .|. c6)),(c6 .|. c6) <= 0 by E19, E20, E21, QUIN_1:10;
then ((2 * (c5 .|. c6)) ^2 ) - ((4 * (c5 .|. c5)) * (c6 .|. c6)) <= 0 by QUIN_1:def 1;
then ((2 ^2 ) * ((c5 .|. c6) ^2 )) - ((4 * (c5 .|. c5)) * (c6 .|. c6)) <= 0 ;
then ((2 * 2) * ((c5 .|. c6) ^2 )) - ((4 * (c5 .|. c<