let V be RealUnitarySpace; :: thesis: for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds
Lin {v} = Lin {w}
let v, w be VECTOR of V; :: thesis: ( v in Lin {w} & v <> 0. V implies Lin {v} = Lin {w} )
assume that
A1: v in Lin {w} and
A2: v <> 0. V ; :: thesis: Lin {v} = Lin {w}
consider a being Real such that
A3: v = a * w by A1, Th29;
now :: thesis: for u being VECTOR of V holds
( ( u in Lin {v} implies u in Lin {w} ) & ( u in Lin {w} implies u in Lin {v} ) )
let u be VECTOR of V; :: thesis: ( ( u in Lin {v} implies u in Lin {w} ) & ( u in Lin {w} implies u in Lin {v} ) )
A4: a <> 0 by A2, A3, RLVECT_1:10;
thus ( u in Lin {v} implies u in Lin {w} ) :: thesis: ( u in Lin {w} implies u in Lin {v} )
proof
assume u in Lin {v} ; :: thesis: u in Lin {w}
then consider b being Real such that
A5: u = b * v by Th29;
u = (b * a) * w by A3, A5, RLVECT_1:def 7;
hence u in Lin {w} by Th29; :: thesis: verum
end;
assume u in Lin {w} ; :: thesis: u in Lin {v}
then consider b being Real such that
A6: u = b * w by Th29;
(a ") * v = ((a ") * a) * w by A3, RLVECT_1:def 7
.= 1 * w by A4, XCMPLX_0:def 7
.= w by RLVECT_1:def 8 ;
then u = (b * (a ")) * v by A6, RLVECT_1:def 7;
hence u in Lin {v} by Th29; :: thesis: verum
end;
hence Lin {v} = Lin {w} by RUSUB_1:25; :: thesis: verum