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 _|_ & l <> 0. F holds
ProJ (a,(l * b),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 _|_ & l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
let a, b, x be 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 l be Element of F; ( 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
; 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, Th5;
then A3:
a _|_
by Th11;
A4:
x - ((ProJ (a,(l * b),x)) * (l * b)) = x - (((ProJ (a,(l * b),x)) * l) * b)
by VECTSP_1:def 16;
a _|_
by A1, Th11;
then
(ProJ (a,b,x)) * (l ") = ((ProJ (a,(l * b),x)) * l) * (l ")
by A1, A3, A4, Th8;
then
(ProJ (a,b,x)) * (l ") = (ProJ (a,(l * b),x)) * (l * (l "))
by GROUP_1:def 3;
then
(l ") * (ProJ (a,b,x)) = (ProJ (a,(l * b),x)) * (1_ F)
by A2, VECTSP_1:def 10;
hence
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
; verum