let F be Field; :: thesis: for S being SymSp of F
for a, p, x, y being Element of S st not p _|_ & not p _|_ & not p _|_ holds
(ProJ p,a,x) * (ProJ x,p,y) = (- (ProJ p,a,y)) * (ProJ y,p,x)
let S be SymSp of F; :: thesis: for a, p, x, y being Element of S st not p _|_ & not p _|_ & not p _|_ holds
(ProJ p,a,x) * (ProJ x,p,y) = (- (ProJ p,a,y)) * (ProJ y,p,x)
let a, p, x, y be Element of S; :: thesis: ( not p _|_ & not p _|_ & not p _|_ implies (ProJ p,a,x) * (ProJ x,p,y) = (- (ProJ p,a,y)) * (ProJ y,p,x) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1: not p _|_ and
A2: not p _|_ and
A3: not p _|_ ; :: thesis: (ProJ p,a,x) * (ProJ x,p,y) = (- (ProJ p,a,y)) * (ProJ y,p,x)
A4: not y _|_ by A3, Th12;
A5: not x _|_ by A2, Th12;

A6: now

A7: ProJ p,a,x <> 0. F by A1, A2, Th36;
assume A8: not x _|_ ; :: thesis: (ProJ p,a,x) * (ProJ x,p,y) = (- (ProJ p,a,y)) * (ProJ y,p,x)
then A9: not y _|_ by Th12;
(ProJ p,a,y) * ((ProJ p,a,x) " ) = ProJ p,x,y by A1, A2, Th37;
then ((ProJ p,a,y) * ((ProJ p,a,x) " )) * (ProJ p,a,x) = ((- ((ProJ x,y,p) " )) * (ProJ y,x,p)) * (ProJ p,a,x) by A5, A8, Th40;
then (ProJ p,a,y) * (((ProJ p,a,x) " ) * (ProJ p,a,x)) = ((- ((ProJ x,y,p) " )) * (ProJ y,x,p)) * (ProJ p,a,x) by GROUP_1:def 4;
then (ProJ p,a,y) * (1_ F) = ((- ((ProJ x,y,p) " )) * (ProJ y,x,p)) * (ProJ p,a,x) by A7, VECTSP_1:def 22;
then ProJ p,a,y = ((ProJ y,x,p) * (- ((ProJ x,y,p) " ))) * (ProJ p,a,x) by VECTSP_1:def 19;
then ProJ p,a,y = (ProJ y,x,p) * ((- ((ProJ x,y,p) " )) * (ProJ p,a,x)) by GROUP_1:def 4;
then (ProJ y,p,x) * (ProJ p,a,y) = (ProJ y,p,x) * (((ProJ y,p,x) " ) * ((- ((ProJ x,y,p) " )) * (ProJ p,a,x))) by A4, A9, Th38;
then A10: (ProJ y,p,x) * (ProJ p,a,y) = ((ProJ y,p,x) * ((ProJ y,p,x) " )) * ((- ((ProJ x,y,p) " )) * (ProJ p,a,x)) by GROUP_1:def 4;
ProJ y,p,x <> 0. F by A4, A9, Th36;
then (ProJ y,p,x) * (ProJ p,a,y) = ((- ((ProJ x,y,p) " )) * (ProJ p,a,x)) * (1_ F) by A10, VECTSP_1:def 22;
then (ProJ p,a,y) * (ProJ y,p,x) = (- ((ProJ x,y,p) " )) * (ProJ p,a,x) by VECTSP_1:def 19;
then - ((ProJ p,a,y) * (ProJ y,p,x)) = - (- (((ProJ x,y,p) " ) * (ProJ p,a,x))) by VECTSP_1:41;
then - ((ProJ p,a,y) * (ProJ y,p,x)) = ((ProJ x,y,p) " ) * (ProJ p,a,x) by RLVECT_1:30;
then (- (ProJ p,a,y)) * (ProJ y,p,x) = ((ProJ x,y,p) " ) * (ProJ p,a,x) by VECTSP_1:41;
hence (ProJ p,a,x) * (ProJ x,p,y) = (- (ProJ p,a,y)) * (ProJ y,p,x) by A5, A8, Th38; :: thesis: verum

end;

now

assume A11: x _|_ ; :: thesis: (ProJ p,a,x) * (ProJ x,p,y) = (- (ProJ p,a,y)) * (ProJ y,p,x)
then ProJ x,p,y = 0. F by A5, Th36;
then A12: (ProJ p,a,x) * (ProJ x,p,y) = 0. F by VECTSP_1:39;
y _|_ by A11, Th12;
then ProJ y,p,x = 0. F by A4, Th36;
hence (ProJ p,a,x) * (ProJ x,p,y) = (- (ProJ p,a,y)) * (ProJ y,p,x) by A12, VECTSP_1:39; :: thesis: verum

end;

hence (ProJ p,a,x) * (ProJ x,p,y) = (- (ProJ p,a,y)) * (ProJ y,p,x) by A6; :: thesis: verum