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 4
.= ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by BHSP_1:21
.= ((sqrt (x .|. x)) ^2 ) + (y .|. y) by A1, A3, SQUARE_1:def 4
.= ((sqrt (x .|. x)) ^2 ) + ((sqrt (y .|. y)) ^2 ) by A4, SQUARE_1:def 4
.= (||.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