let F be Field; for S being OrtSp of F
for a, b, x being Element of S
for l being Element of F st not a _|_ holds
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
let S be OrtSp of F; for a, b, x being Element of S
for l being Element of F st not a _|_ holds
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
let a, b, x be Element of S; for l being Element of F st not a _|_ holds
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
let l be Element of F; ( not a _|_ implies ProJ (a,b,(l * x)) = l * (ProJ (a,b,x)) )
set L = x - ((ProJ (a,b,x)) * b);
A1: l * (x - ((ProJ (a,b,x)) * b)) =
(l * x) - (l * ((ProJ (a,b,x)) * b))
by VECTSP_1:23
.=
(l * x) - ((l * (ProJ (a,b,x))) * b)
by VECTSP_1:def 16
;
assume A2:
not a _|_
; ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
then A3:
a _|_
by Th11;
a _|_
by A2, Th11;
then
a _|_
by A1, Def1;
hence
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
by A2, A3, Th8; verum