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 Def11;
then A2: |.(y .|. y).| <> 0 by COMPLEX1:45;
A3: (Re (x .|. y)) ^2 >= 0 by XREAL_1:63;
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:9
.= ((Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) - (0 * (Im ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) by COMPLEX1:12
.= (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:17
.= - (Re ((x .|. y) * ((x .|. y) *'))) by Def11 ;
A6: Im ((x .|. y) * ((x .|. y) *')) = 0 by COMPLEX1:40;
A7: Im (y .|. y) = 0 by Def11;
A8: Re (y .|. y) >= 0 by Def11;
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:13;
then A10: y .|. y = c1 by A7, COMPLEX1:13;
((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 Lm10
.= (((c1 * ((c1 *') * (x .|. x))) + (c1 * (((- (x .|. y)) *') * (x .|. y)))) + ((c1 *') * ((- (x .|. y)) * (y .|. x)))) + (c1 * ((- (x .|. y)) * ((- (x .|. y)) *'))) by A7, A9, COMPLEX1:13
.= ((c1 * (((c1 *') * (x .|. x)) + (((- (x .|. y)) *') * (x .|. y)))) + (c1 * ((- (x .|. y)) * (y .|. x)))) + (c1 * ((- (x .|. y)) * ((- (x .|. y)) *'))) by A10, Def11
.= 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, Def11
.= c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) ;
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, Def11;
then (Re (c1 * (x .|. x))) + (Re ((- (x .|. y)) * (y .|. x))) >= 0 by A8, A7, A9, A2, COMPLEX1:8, COMPLEX1:13;
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:19;
A12: Im (x .|. x) = 0 by Def11;
A13: (Im (x .|. y)) ^2 >= 0 by XREAL_1:63;
Im c1 = 0 by A7, A9, COMPLEX1:13;
then Im (c1 * (x .|. x)) = ((Re c1) * 0) + ((Re (x .|. x)) * 0) by A12, COMPLEX1:9;
then A14: |.(c1 * (x .|. x)).| = |.(Re (c1 * (x .|. x))).| by COMPLEX1:50;
Re ((x .|. y) * ((x .|. y) *')) = ((Re (x .|. y)) ^2) + ((Im (x .|. y)) ^2) by COMPLEX1:40;
then A15: Re ((x .|. y) * ((x .|. y) *')) >= 0 + 0 by A3, A13;
then |.(Re ((x .|. y) * ((x .|. y) *'))).| = Re ((x .|. y) * ((x .|. y) *')) by ABSVALUE:def 1;
then |.(Re (c1 * (x .|. x))).| >= |.(Re ((x .|. y) * ((x .|. y) *'))).| by A11, A15, ABSVALUE:def 1;
then |.(c1 * (x .|. x)).| >= |.((x .|. y) * ((x .|. y) *')).| by A6, A14, COMPLEX1:50;
then |.(x .|. x).| * |.(y .|. y).| >= |.((x .|. y) * ((x .|. y) *')).| by A10, COMPLEX1:65;
then |.(x .|. x).| * |.(y .|. y).| >= |.(x .|. y).| * |.((x .|. y) *').| by COMPLEX1:65;
then A16: |.(x .|. x).| * |.(y .|. y).| >= |.(x .|. y).| * |.(x .|. y).| by COMPLEX1:53;
|.(x .|. y).| ^2 >= 0 by XREAL_1:63;
then A17: sqrt (|.(x .|. x).| * |.(y .|. y).|) >= sqrt (|.(x .|. y).| ^2) by A16, SQUARE_1:26;
A18: |.(y .|. y).| >= 0 by COMPLEX1:46;
|.(x .|. x).| >= 0 by COMPLEX1:46;
then (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) >= sqrt (|.(x .|. y).| ^2) by A17, A18, SQUARE_1:29;
hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by COMPLEX1:46, SQUARE_1:22; :: 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 Def11;
hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by A19, Th25, COMPLEX1:44; :: thesis: verum

end;

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