let V be RealUnitarySpace; :: thesis: Ort_Comp ((Omega). V) = (0). V
for x being object st x in the carrier of (Ort_Comp ((Omega). V)) holds
x in the carrier of ((0). V)
proof
let x be object ; :: thesis: ( x in the carrier of (Ort_Comp ((Omega). V)) implies x in the carrier of ((0). V) )
assume x in the carrier of (Ort_Comp ((Omega). V)) ; :: thesis: x in the carrier of ((0). V)
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in (Omega). V holds
w,v are_orthogonal } by Def3;
then A1: ex v being VECTOR of V st
( x = v & ( for w being VECTOR of V st w in (Omega). V holds
w,v are_orthogonal ) ) ;
then reconsider x = x as VECTOR of V ;
x in UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ;
then x in (Omega). V by RUSUB_1:def 3;
then x,x are_orthogonal by A1;
then 0 = x .|. x by BHSP_1:def 3;
then x = 0. V by BHSP_1:def 2;
then x in {(0. V)} by TARSKI:def 1;
hence x in the carrier of ((0). V) by RUSUB_1:def 2; :: thesis: verum
end;
then A2: the carrier of (Ort_Comp ((Omega). V)) c= the carrier of ((0). V) ;
for x being object st x in the carrier of ((0). V) holds
x in the carrier of (Ort_Comp ((Omega). V))
proof
let x be object ; :: thesis: ( x in the carrier of ((0). V) implies x in the carrier of (Ort_Comp ((Omega). V)) )
assume x in the carrier of ((0). V) ; :: thesis: x in the carrier of (Ort_Comp ((Omega). V))
then A3: x in {(0. V)} by RUSUB_1:def 2;
then reconsider x = x as VECTOR of V ;
for w being VECTOR of V st w in (Omega). V holds
w,x are_orthogonal
proof
let w be VECTOR of V; :: thesis: ( w in (Omega). V implies w,x are_orthogonal )
assume w in (Omega). V ; :: thesis: w,x are_orthogonal
w .|. x = w .|. (0. V) by A3, TARSKI:def 1
.= 0 by BHSP_1:15 ;
hence w,x are_orthogonal by BHSP_1:def 3; :: thesis: verum
end;
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in (Omega). V holds
w,v are_orthogonal } ;
hence x in the carrier of (Ort_Comp ((Omega). V)) by Def3; :: thesis: verum
end;
then the carrier of ((0). V) c= the carrier of (Ort_Comp ((Omega). V)) ;
then the carrier of (Ort_Comp ((Omega). V)) = the carrier of ((0). V) by A2;
hence Ort_Comp ((Omega). V) = (0). V by RUSUB_1:24; :: thesis: verum