let F be Field; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 _|_ ; :: thesis: 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)) ; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 _|_ ; :: thesis: 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)) ; :: thesis: verum