let V be RealUnitarySpace; :: thesis: for W being Subspace of V

for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds

not v in W

let W be Subspace of V; :: thesis: for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds

not v in W

let v be VECTOR of V; :: thesis: ( v <> 0. V & v in Ort_Comp W implies not v in W )

assume A1: v <> 0. V ; :: thesis: ( not v in Ort_Comp W or not v in W )

( v in Ort_Comp W implies not v in W )

for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds

not v in W

let W be Subspace of V; :: thesis: for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds

not v in W

let v be VECTOR of V; :: thesis: ( v <> 0. V & v in Ort_Comp W implies not v in W )

assume A1: v <> 0. V ; :: thesis: ( not v in Ort_Comp W or not v in W )

( v in Ort_Comp W implies not v in W )

proof

hence
( not v in Ort_Comp W or not v in W )
; :: thesis: verum
assume A2:
v in Ort_Comp W
; :: thesis: not v in W

assume A3: v in W ; :: thesis: contradiction

v in { v1 where v1 is VECTOR of V : for w being VECTOR of V st w in W holds

w,v1 are_orthogonal } by A2, RUSUB_5:def 3;

then ex v1 being VECTOR of V st

( v = v1 & ( for w being VECTOR of V st w in W holds

w,v1 are_orthogonal ) ) ;

then v,v are_orthogonal by A3;

hence contradiction by A1, BHSP_1:def 2; :: thesis: verum

end;assume A3: v in W ; :: thesis: contradiction

v in { v1 where v1 is VECTOR of V : for w being VECTOR of V st w in W holds

w,v1 are_orthogonal } by A2, RUSUB_5:def 3;

then ex v1 being VECTOR of V st

( v = v1 & ( for w being VECTOR of V st w in W holds

w,v1 are_orthogonal ) ) ;

then v,v are_orthogonal by A3;

hence contradiction by A1, BHSP_1:def 2; :: thesis: verum