let V be RealUnitarySpace; :: thesis: for v being VECTOR of V ex W being Subspace of V st the carrier of W = { u where u is VECTOR of V : u .|. v = 0 }
let v be VECTOR of V; :: thesis: ex W being Subspace of V st the carrier of W = { u where u is VECTOR of V : u .|. v = 0 }
set M = { u where u is VECTOR of V : u .|. v = 0 } ;
for x being object st x in { u where u is VECTOR of V : u .|. v = 0 } holds
x in the carrier of V
proof
let x be object ; :: thesis: ( x in { u where u is VECTOR of V : u .|. v = 0 } implies x in the carrier of V )
assume x in { u where u is VECTOR of V : u .|. v = 0 } ; :: thesis: x in the carrier of V
then ex u being VECTOR of V st
( x = u & u .|. v = 0 ) ;
hence x in the carrier of V ; :: thesis: verum
end;
then reconsider M = { u where u is VECTOR of V : u .|. v = 0 } as Subset of V by TARSKI:def 3;
(0. V) .|. v = 0 by BHSP_1:14;
then A1: 0. V in M ;
then reconsider M = M as non empty Subset of V ;
for x, y being VECTOR of V
for a being Real st x in M & y in M holds
((1 - a) * x) + (a * y) in M
proof
let x, y be VECTOR of V; :: thesis: for a being Real st x in M & y in M holds
((1 - a) * x) + (a * y) in M
let a be Real; :: thesis: ( x in M & y in M implies ((1 - a) * x) + (a * y) in M )
assume that
A2: x in M and
A3: y in M ; :: thesis: ((1 - a) * x) + (a * y) in M
consider u2 being VECTOR of V such that
A4: y = u2 and
A5: u2 .|. v = 0 by A3;
consider u1 being VECTOR of V such that
A6: x = u1 and
A7: u1 .|. v = 0 by A2;
(((1 - a) * u1) + (a * u2)) .|. v = (((1 - a) * u1) .|. v) + ((a * u2) .|. v) by BHSP_1:def 2
.= ((1 - a) * (u1 .|. v)) + ((a * u2) .|. v) by BHSP_1:def 2
.= a * 0 by A7, A5, BHSP_1:def 2 ;
hence ((1 - a) * x) + (a * y) in M by A6, A4; :: thesis: verum
end;
then reconsider M = M as non empty Affine Subset of V by RUSUB_4:def 4;
take Lin M ; :: thesis: the carrier of (Lin M) = { u where u is VECTOR of V : u .|. v = 0 }
thus the carrier of (Lin M) = { u where u is VECTOR of V : u .|. v = 0 } by A1, RUSUB_4:28; :: thesis: verum