let F be Field; for S being OrtSp of F
for a, b, 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 a, b, c being Element of S st not a _|_ & c + a _|_ holds
ProJ (a,b,c) = - (ProJ (c,b,a))
let a, b, 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, Th11;
then
a _|_
by VECTSP_1:21;
then
a _|_
by Def1;
then
a _|_
by VECTSP_1:def 14;
then
a _|_
by VECTSP_1:def 16;
then
a _|_
by VECTSP_1:10;
then
a _|_
;
then
a _|_
by VECTSP_1:14;
then
((ProJ (a,b,c)) * b) - c _|_
by Th2;
then A3:
((ProJ (a,b,c)) * b) - c _|_
by Th6;
c + a _|_
by A2, Def1;
then
c - (- a) _|_
by RLVECT_1:17;
then
(- a) - ((ProJ (a,b,c)) * b) _|_
by A3, Def1;
then A4:
c _|_
by Th2;
( not b _|_ & b _|_ )
by A1, A2, Th2;
then A5:
not b _|_
by Th3;
then A6:
not c _|_
by Th2;
then
c _|_
by Th11;
then ProJ (a,b,c) =
ProJ (c,b,(- a))
by A6, A4, Th8
.=
ProJ (c,b,((- (1_ F)) * a))
by VECTSP_1:14
.=
(- (1_ F)) * (ProJ (c,b,a))
by A5, Th2, Th12
.=
- ((ProJ (c,b,a)) * (1_ F))
by VECTSP_1:9
;
hence
ProJ (a,b,c) = - (ProJ (c,b,a))
; verum