let F be Field; for S being OrtSp of F
for b, a, c being Element of S st not a _|_ & c + a _|_ holds
ProJ a,b,c = - (ProJ c,b,a)
let S be OrtSp of F; for b, a, c being Element of S st not a _|_ & c + a _|_ holds
ProJ a,b,c = - (ProJ c,b,a)
let b, a, c be Element of S; ( not a _|_ & c + a _|_ implies ProJ a,b,c = - (ProJ c,b,a) )
set 1F = 1_ F;
assume that
A1:
not a _|_
and
A2:
c + a _|_
; ProJ a,b,c = - (ProJ c,b,a)
a _|_
by A1, Th24;
then
a _|_
by VECTSP_1:68;
then
a _|_
by Def2;
then
a _|_
by VECTSP_1:def 26;
then
a _|_
by VECTSP_1:def 26;
then
a _|_
by VECTSP_1:42;
then
a _|_
by VECTSP_1:def 19;
then
a _|_
by VECTSP_1:59;
then
((ProJ a,b,c) * b) - c _|_
by Th12;
then A3:
((ProJ a,b,c) * b) - c _|_
by Th16;
c + a _|_
by A2, Def2;
then
c - (- a) _|_
by RLVECT_1:30;
then
(- a) - ((ProJ a,b,c) * b) _|_
by A3, Def2;
then A4:
c _|_
by Th12;
( not b _|_ & b _|_ )
by A1, A2, Th12;
then A5:
not b _|_
by Th13;
then A6:
not c _|_
by Th12;
then
c _|_
by Th24;
then ProJ a,b,c =
ProJ c,b,(- a)
by A6, A4, Th20
.=
ProJ c,b,((- (1_ F)) * a)
by VECTSP_1:59
.=
(- (1_ F)) * (ProJ c,b,a)
by A5, Th12, Th25
.=
- ((ProJ c,b,a) * (1_ F))
by VECTSP_1:41
;
hence
ProJ a,b,c = - (ProJ c,b,a)
by VECTSP_1:def 19; verum