let X be ComplexUnitarySpace; for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.||
let x, y be Point of X; ||.(x + y).|| <= ||.x.|| + ||.y.||
A1:
||.(x + y).|| ^2 >= 0
by XREAL_1:63;
Re ((x + y) .|. (x + y)) >= 0
by Def11;
then A2:
|.((x + y) .|. (x + y)).| >= 0
by Th29;
sqrt (||.(x + y).|| ^2) = sqrt |.((x + y) .|. (x + y)).|
by Th39, SQUARE_1:22;
then A3:
||.(x + y).|| ^2 = |.((x + y) .|. (x + y)).|
by A2, A1, SQUARE_1:28;
|.(y .|. y).| >= 0
by COMPLEX1:46;
then A4:
|.(y .|. y).| = ||.y.|| ^2
by SQUARE_1:def 2;
A5: - (Im (x .|. y)) =
Im ((x .|. y) *')
by COMPLEX1:27
.=
Im (y .|. x)
by Def11
;
Im ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) =
(Im (((x .|. x) + (x .|. y)) + (y .|. x))) + (Im (y .|. y))
by COMPLEX1:8
.=
((Im ((x .|. x) + (x .|. y))) + (Im (y .|. x))) + (Im (y .|. y))
by COMPLEX1:8
.=
(((Im (x .|. x)) + (Im (x .|. y))) + (Im (y .|. x))) + (Im (y .|. y))
by COMPLEX1:8
.=
((0 + (Im (x .|. y))) + (Im (y .|. x))) + (Im (y .|. y))
by Def11
.=
((Im (x .|. y)) + (Im (y .|. x))) + 0
by Def11
;
then A6:
(((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) = (Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))) + (0 * <i>)
by A5, COMPLEX1:13;
A7: Re (x .|. y) =
Re ((x .|. y) *')
by COMPLEX1:27
.=
Re (y .|. x)
by Def11
;
A8:
Re (x .|. y) <= |.(x .|. y).|
by COMPLEX1:54;
|.(x .|. y).| <= ||.x.|| * ||.y.||
by Th30;
then
Re (x .|. y) <= ||.x.|| * ||.y.||
by A8, XXREAL_0:2;
then A9:
2 * (Re (x .|. y)) <= 2 * (||.x.|| * ||.y.||)
by XREAL_1:64;
Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) = Re ((x + y) .|. (x + y))
by Th26;
then A10:
Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) >= 0
by Def11;
Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) =
(Re (((x .|. x) + (x .|. y)) + (y .|. x))) + (Re (y .|. y))
by COMPLEX1:8
.=
((Re ((x .|. x) + (x .|. y))) + (Re (y .|. x))) + (Re (y .|. y))
by COMPLEX1:8
.=
(((Re (x .|. x)) + (Re (x .|. y))) + (Re (y .|. x))) + (Re (y .|. y))
by COMPLEX1:8
.=
((|.(x .|. x).| + (Re (x .|. y))) + (Re (y .|. x))) + (Re (y .|. y))
by Th29
.=
((|.(x .|. x).| + (Re (x .|. y))) + (Re (y .|. x))) + |.(y .|. y).|
by Th29
;
then
|.((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)).| = (|.(x .|. x).| + (2 * (Re (x .|. y)))) + |.(y .|. y).|
by A7, A10, A6, ABSVALUE:def 1;
then A11:
||.(x + y).|| ^2 = (2 * (Re (x .|. y))) + (|.(x .|. x).| + |.(y .|. y).|)
by A3, Th26;
A12:
||.y.|| >= 0
by Th39;
|.(x .|. x).| >= 0
by COMPLEX1:46;
then
(sqrt |.(x .|. x).|) ^2 = |.(x .|. x).|
by SQUARE_1:def 2;
then
||.(x + y).|| ^2 <= (2 * (||.x.|| * ||.y.||)) + ((||.x.|| ^2) + |.(y .|. y).|)
by A11, A9, XREAL_1:6;
then A13:
||.(x + y).|| ^2 <= (||.x.|| + ||.y.||) ^2
by A4;
||.x.|| >= 0
by Th39;
hence
||.(x + y).|| <= ||.x.|| + ||.y.||
by A12, A13, SQUARE_1:16; verum