let K be Field; :: thesis: for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)]
let V be VectSp of K; :: thesis: for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)]
let v be Vector of V; :: thesis: for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)]
let X be Subspace of V; :: thesis: for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)]
let y be Vector of (X + (Lin {v})); :: thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)]
let W be Subspace of X + (Lin {v}); :: thesis: ( v = y & X = W & not v in X implies for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)] )
assume A1: ( v = y & X = W & not v in X ) ; :: thesis: for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)]
let w be Vector of (X + (Lin {v})); :: thesis: ex x being Vector of X ex r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)]
A2: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, Th15;
consider v1, v2 being Vector of (X + (Lin {v})) such that
A3: w |-- W,(Lin {y}) = [v1,v2] by Th18;
v1 in W by A2, A3, Th8;
then reconsider x = v1 as Vector of X by A1, STRUCT_0:def 5;
v2 in Lin {y} by A2, A3, Th8;
then consider r being Element of K such that
A4: v2 = r * y by Th4;
take x ; :: thesis: ex r being Element of K st w |-- W,(Lin {y}) = [x,(r * v)]
take r ; :: thesis: w |-- W,(Lin {y}) = [x,(r * v)]
thus w |-- W,(Lin {y}) = [x,(r * v)] by A1, A3, A4, VECTSP_4:22; :: thesis: verum