let F be Field; :: thesis: for S being OrtSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ a,(l * b),x = (l " ) * (ProJ a,b,x)
let S be OrtSp of F; :: thesis: for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ a,(l * b),x = (l " ) * (ProJ a,b,x)
let b, a, x be Element of S; :: thesis: for l being Element of F st not a _|_ & l <> 0. F holds
ProJ a,(l * b),x = (l " ) * (ProJ a,b,x)
let l be Element of F; :: thesis: ( not a _|_ & l <> 0. F implies ProJ a,(l * b),x = (l " ) * (ProJ a,b,x) )
assume that
A1: not a _|_ and
A2: l <> 0. F ; :: thesis: ProJ a,(l * b),x = (l " ) * (ProJ a,b,x)
set L = x - ((ProJ a,(l * b),x) * (l * b));
not a _|_ by A1, A2, Th15;
then A3: a _|_ by Th24;
A4: x - ((ProJ a,(l * b),x) * (l * b)) = x - (((ProJ a,(l * b),x) * l) * b) by VECTSP_1:def 28;
a _|_ by A1, Th24;
then (ProJ a,b,x) * (l " ) = ((ProJ a,(l * b),x) * l) * (l " ) by A1, A3, A4, Th20;
then (ProJ a,b,x) * (l " ) = (ProJ a,(l * b),x) * (l * (l " )) by GROUP_1:def 4;
then (l " ) * (ProJ a,b,x) = (ProJ a,(l * b),x) * (1_ F) by A2, VECTSP_1:def 22;
hence ProJ a,(l * b),x = (l " ) * (ProJ a,b,x) by VECTSP_1:def 19; :: thesis: verum