:: BHSP_1 semantic presentation

definition
attr a1 is strict;
struct UNITSTR -> RLSStruct ;
aggr UNITSTR(# carrier, Zero, add, Mult, scalar #) -> UNITSTR ;
sel scalar a1 -> 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 ; :: uses 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 ; :: uses 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 a2 .|. a3 -> 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
proof
reconsider c8 = c4 as VECTOR of ((0). c1) ;
c4 .|. c4 = c2 . [c8,c8] ;
hence 0 <= c4 .|. c4 by FUNCOP_1:13;
end;
thus c4 .|. c5 = c5 .|. c4
proof
reconsider c8 = c4, c9 = c5 as VECTOR of ((0). c1) ;
( c4 .|. c5 = c2 . [c8,c9] & c5 .|. c4 = c2 . [c9,c8] ) ;
hence c4 .|. c5 = c5 .|. c4 by E4;
end;
thus (c4 + c5) .|. c6 = (c4 .|. c6) + (c5 .|. c6)
proof
reconsider c8 = c4, c9 = c5, c10 = c6 as VECTOR of ((0). c1) ;
c4 + c5 = the add of (UNITSTR the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2) . [c4,c5]
.= c8 + c9 ;
then ( (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 = the Mult of (UNITSTR the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2) . [c7,c8]
.= c7 * c8 ;
then ( (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: now
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);
let c6, c7 be VECTOR of ((0). c1);
assume E10: ( c4 = c6 & c5 = c7 ) ;
hence c4 + c5 = the add of (UNITSTR the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2) . [c6,c7]
.= c6 + c7 ;

let c8 be Real;
thus c8 * c4 = the Mult of (UNITSTR the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2) . [c8,c6] by E10
.= c8 * c6 ;
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 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) :: uses 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) ;
c5 + c6 = c7 + c8 ;
hence 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 :: uses 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) :: uses 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 :: uses 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) :: uses 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 a2 .|. a3 -> 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)))