let F be Field; :: thesis: for S being OrtSp of F

for a, b, c being Element of S st not b _|_ & not b _|_ holds

ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))

let S be OrtSp of F; :: thesis: for a, b, c being Element of S st not b _|_ & not b _|_ holds

ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))

let a, b, c be Element of S; :: thesis: ( not b _|_ & not b _|_ implies ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c)) )

set 1F = 1_ F;

assume that

A1: not b _|_ and

A2: not b _|_ ; :: thesis: ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))

ProJ (b,a,c) <> 0. F by A1, A2, Th20;

then A3: - ((ProJ (b,a,c)) ") <> 0. F by VECTSP_1:25;

ProJ (b,a,c) <> 0. F by A1, A2, Th20;

then (- (1_ F)) * (((ProJ (b,a,c)) ") * (ProJ (b,a,c))) = (- (1_ F)) * (1_ F) by VECTSP_1:def 10;

then ((- (1_ F)) * ((ProJ (b,a,c)) ")) * (ProJ (b,a,c)) = (- (1_ F)) * (1_ F) by GROUP_1:def 3;

then ((- (1_ F)) * ((ProJ (b,a,c)) ")) * (ProJ (b,a,c)) = - (1_ F) ;

then (- (((ProJ (b,a,c)) ") * (1_ F))) * (ProJ (b,a,c)) = - (1_ F) by VECTSP_1:9;

then (- ((ProJ (b,a,c)) ")) * (ProJ (b,a,c)) = - (1_ F) ;

then ProJ (b,a,((- ((ProJ (b,a,c)) ")) * c)) = - (1_ F) by A1, Th12;

then b _|_ by A1, Th11;

then b _|_ by VECTSP_1:14;

then b _|_ by RLVECT_1:17;

then A4: ((- ((ProJ (b,a,c)) ")) * c) + a _|_ by Th2;

not a _|_ by A1, Th2;

then ProJ (a,b,((- ((ProJ (b,a,c)) ")) * c)) = - (ProJ (((- ((ProJ (b,a,c)) ")) * c),b,a)) by A4, Th23;

then ProJ (a,b,((- ((ProJ (b,a,c)) ")) * c)) = - (ProJ (c,b,a)) by A2, A3, Th2, Th15;

then (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c)) = - (ProJ (c,b,a)) by A1, Th2, Th12;

then (- (((ProJ (b,a,c)) ") * (ProJ (a,b,c)))) * (- (1_ F)) = (- (ProJ (c,b,a))) * (- (1_ F)) by VECTSP_1:9;

then (((ProJ (b,a,c)) ") * (ProJ (a,b,c))) * (1_ F) = (- (ProJ (c,b,a))) * (- (1_ F)) by VECTSP_1:10;

then (((ProJ (b,a,c)) ") * (ProJ (a,b,c))) * (1_ F) = (ProJ (c,b,a)) * (1_ F) by VECTSP_1:10;

then ((ProJ (b,a,c)) ") * (ProJ (a,b,c)) = (ProJ (c,b,a)) * (1_ F) ;

hence ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c)) ; :: thesis: verum

for a, b, c being Element of S st not b _|_ & not b _|_ holds

ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))

let S be OrtSp of F; :: thesis: for a, b, c being Element of S st not b _|_ & not b _|_ holds

ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))

let a, b, c be Element of S; :: thesis: ( not b _|_ & not b _|_ implies ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c)) )

set 1F = 1_ F;

assume that

A1: not b _|_ and

A2: not b _|_ ; :: thesis: ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))

ProJ (b,a,c) <> 0. F by A1, A2, Th20;

then A3: - ((ProJ (b,a,c)) ") <> 0. F by VECTSP_1:25;

ProJ (b,a,c) <> 0. F by A1, A2, Th20;

then (- (1_ F)) * (((ProJ (b,a,c)) ") * (ProJ (b,a,c))) = (- (1_ F)) * (1_ F) by VECTSP_1:def 10;

then ((- (1_ F)) * ((ProJ (b,a,c)) ")) * (ProJ (b,a,c)) = (- (1_ F)) * (1_ F) by GROUP_1:def 3;

then ((- (1_ F)) * ((ProJ (b,a,c)) ")) * (ProJ (b,a,c)) = - (1_ F) ;

then (- (((ProJ (b,a,c)) ") * (1_ F))) * (ProJ (b,a,c)) = - (1_ F) by VECTSP_1:9;

then (- ((ProJ (b,a,c)) ")) * (ProJ (b,a,c)) = - (1_ F) ;

then ProJ (b,a,((- ((ProJ (b,a,c)) ")) * c)) = - (1_ F) by A1, Th12;

then b _|_ by A1, Th11;

then b _|_ by VECTSP_1:14;

then b _|_ by RLVECT_1:17;

then A4: ((- ((ProJ (b,a,c)) ")) * c) + a _|_ by Th2;

not a _|_ by A1, Th2;

then ProJ (a,b,((- ((ProJ (b,a,c)) ")) * c)) = - (ProJ (((- ((ProJ (b,a,c)) ")) * c),b,a)) by A4, Th23;

then ProJ (a,b,((- ((ProJ (b,a,c)) ")) * c)) = - (ProJ (c,b,a)) by A2, A3, Th2, Th15;

then (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c)) = - (ProJ (c,b,a)) by A1, Th2, Th12;

then (- (((ProJ (b,a,c)) ") * (ProJ (a,b,c)))) * (- (1_ F)) = (- (ProJ (c,b,a))) * (- (1_ F)) by VECTSP_1:9;

then (((ProJ (b,a,c)) ") * (ProJ (a,b,c))) * (1_ F) = (- (ProJ (c,b,a))) * (- (1_ F)) by VECTSP_1:10;

then (((ProJ (b,a,c)) ") * (ProJ (a,b,c))) * (1_ F) = (ProJ (c,b,a)) * (1_ F) by VECTSP_1:10;

then ((ProJ (b,a,c)) ") * (ProJ (a,b,c)) = (ProJ (c,b,a)) * (1_ F) ;

hence ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c)) ; :: thesis: verum