let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|)
let x, y be Point of X; :: thesis: |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|)
A1: ( y <> H₁(X) implies |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) )

proof

assume y <> H₁(X) ; :: thesis: |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|)
then y .|. y <> 0c by Def13;
then A2: |.(y .|. y).| <> 0 by COMPLEX1:131;
A3: (Re (x .|. y)) ^2 >= 0 by XREAL_1:65;
set c2 = - (x .|. y);
reconsider c1 = |.(y .|. y).| + (0 * <i> ) as Element of COMPLEX by XCMPLX_0:def 2;
A4: Re (c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) = ((Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) - ((Im c1) * (Im ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) by COMPLEX1:24
.= ((Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) - (0 * (Im ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) by COMPLEX1:28
.= (Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) ;
A5: Re ((- (x .|. y)) * (y .|. x)) = Re (- ((x .|. y) * (y .|. x)))
.= - (Re ((x .|. y) * (y .|. x))) by COMPLEX1:34
.= - (Re ((x .|. y) * ((x .|. y) *' ))) by Def13 ;
A6: Im ((x .|. y) * ((x .|. y) *' )) = 0 by COMPLEX1:126;
A7: Im (y .|. y) = 0 by Def13;
A8: Re (y .|. y) >= 0 by Def13;
then |.((Re (y .|. y)) + ((Im (y .|. y)) * <i> )).| = Re (y .|. y) by A7, ABSVALUE:def 1;
then A9: |.(y .|. y).| = Re (y .|. y) by COMPLEX1:29;
then A10: y .|. y = c1 by A7, COMPLEX1:29;
((c1 * x) + ((- (x .|. y)) * y)) .|. ((c1 * x) + ((- (x .|. y)) * y)) = ((((c1 * (c1 *' )) * (x .|. x)) + ((c1 * ((- (x .|. y)) *' )) * (x .|. y))) + (((c1 *' ) * (- (x .|. y))) * (y .|. x))) + (((- (x .|. y)) * ((- (x .|. y)) *' )) * (y .|. y)) by Lm9
.= (((c1 * ((c1 *' ) * (x .|. x))) + (c1 * (((- (x .|. y)) *' ) * (x .|. y)))) + ((c1 *' ) * ((- (x .|. y)) * (y .|. x)))) + (c1 * ((- (x .|. y)) * ((- (x .|. y)) *' ))) by A7, A9, COMPLEX1:29
.= ((c1 * (((c1 *' ) * (x .|. x)) + (((- (x .|. y)) *' ) * (x .|. y)))) + (c1 * ((- (x .|. y)) * (y .|. x)))) + (c1 * ((- (x .|. y)) * ((- (x .|. y)) *' ))) by A10, Def13
.= c1 * (((((c1 *' ) * (x .|. x)) + (((- (x .|. y)) *' ) * (x .|. y))) + ((- (x .|. y)) * (y .|. x))) + ((- (x .|. y)) * ((- (x .|. y)) *' )))
.= c1 * ((((c1 * (x .|. x)) + ((x .|. y) * ((- (x .|. y)) *' ))) + ((- (x .|. y)) * (y .|. x))) + ((- (x .|. y)) * ((- (x .|. y)) *' ))) by A10, Def13
.= c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) ;
then Re (c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) >= 0 by Def13;
then ( ( Re c1 >= 0 & Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) >= 0 ) or ( Re c1 <= 0 & Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) <= 0 ) ) by A4, XREAL_1:134;
then (Re (c1 * (x .|. x))) + (Re ((- (x .|. y)) * (y .|. x))) >= 0 by A8, A7, A9, A2, COMPLEX1:19, COMPLEX1:29;
then (Re (c1 * (x .|. x))) - (Re ((x .|. y) * ((x .|. y) *' ))) >= 0 by A5;
then A11: Re (c1 * (x .|. x)) >= (Re ((x .|. y) * ((x .|. y) *' ))) + 0 by XREAL_1:21;
A12: Im (x .|. x) = 0 by Def13;
A13: (Im (x .|. y)) ^2 >= 0 by XREAL_1:65;
Im c1 = 0 by A7, A9, COMPLEX1:29;
then Im (c1 * (x .|. x)) = ((Re c1) * 0 ) + ((Re (x .|. x)) * 0 ) by A12, COMPLEX1:24;
then A14: |.(c1 * (x .|. x)).| = abs (Re (c1 * (x .|. x))) by COMPLEX1:136;
Re ((x .|. y) * ((x .|. y) *' )) = ((Re (x .|. y)) ^2 ) + ((Im (x .|. y)) ^2 ) by COMPLEX1:126;
then A15: Re ((x .|. y) * ((x .|. y) *' )) >= 0 + 0 by A3, A13, XREAL_1:9;
then abs (Re ((x .|. y) * ((x .|. y) *' ))) = Re ((x .|. y) * ((x .|. y) *' )) by ABSVALUE:def 1;
then abs (Re (c1 * (x .|. x))) >= abs (Re ((x .|. y) * ((x .|. y) *' ))) by A11, A15, ABSVALUE:def 1;
then |.(c1 * (x .|. x)).| >= |.((x .|. y) * ((x .|. y) *' )).| by A6, A14, COMPLEX1:136;
then |.(x .|. x).| * |.(y .|. y).| >= |.((x .|. y) * ((x .|. y) *' )).| by A10, COMPLEX1:151;
then |.(x .|. x).| * |.(y .|. y).| >= |.(x .|. y).| * |.((x .|. y) *' ).| by COMPLEX1:151;
then A16: |.(x .|. x).| * |.(y .|. y).| >= |.(x .|. y).| * |.(x .|. y).| by COMPLEX1:139;
|.(x .|. y).| ^2 >= 0 by XREAL_1:65;
then A17: sqrt (|.(x .|. x).| * |.(y .|. y).|) >= sqrt (|.(x .|. y).| ^2 ) by A16, SQUARE_1:94;
A18: |.(y .|. y).| >= 0 by COMPLEX1:132;
|.(x .|. x).| >= 0 by COMPLEX1:132;
then (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) >= sqrt (|.(x .|. y).| ^2 ) by A17, A18, SQUARE_1:97;
hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by COMPLEX1:132, SQUARE_1:89; :: thesis: verum

end;

( y = H₁(X) implies |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) )

proof

assume A19: y = H₁(X) ; :: thesis: |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|)
then y .|. y = 0c by Def13;
hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by A19, Th32, COMPLEX1:130, SQUARE_1:82; :: thesis: verum

end;

hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by A1; :: thesis: verum