let X be RealUnitarySpace; :: thesis: for x, y being Point of X st x,y are_orthogonal holds
||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)
let x, y be Point of X; :: thesis: ( x,y are_orthogonal implies ||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2) )
assume x,y are_orthogonal ; :: thesis: ||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)
then A1: x .|. y = 0 by BHSP_1:def 3;
A2: (x + y) .|. (x + y) >= 0 by BHSP_1:def 2;
A3: x .|. x >= 0 by BHSP_1:def 2;
A4: y .|. y >= 0 by BHSP_1:def 2;
||.(x + y).|| ^2 = (sqrt ((x + y) .|. (x + y))) ^2 by BHSP_1:def 4
.= (x + y) .|. (x + y) by A2, SQUARE_1:def 2
.= ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by BHSP_1:16
.= ((sqrt (x .|. x)) ^2) + (y .|. y) by A1, A3, SQUARE_1:def 2
.= ((sqrt (x .|. x)) ^2) + ((sqrt (y .|. y)) ^2) by A4, SQUARE_1:def 2
.= (||.x.|| ^2) + ((sqrt (y .|. y)) ^2) by BHSP_1:def 4
.= (||.x.|| ^2) + (||.y.|| ^2) by BHSP_1:def 4 ;
hence ||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2) ; :: thesis: verum