let F be Field; :: thesis: for S being OrtSp 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 OrtSp 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, Th2;

A5: not x _|_ by A2, Th2;

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 OrtSp 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, Th2;

A5: not x _|_ by A2, Th2;

A6: now :: thesis: ( not x _|_ implies (ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x)) )

A7:
ProJ (p,a,x) <> 0. F
by A1, A2, Th20;

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 Th2;

(ProJ (p,a,y)) * ((ProJ (p,a,x)) ") = ProJ (p,x,y) by A1, A2, Th21;

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, Th24;

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 3;

then (ProJ (p,a,y)) * (1_ F) = (((ProJ (x,y,p)) ") * (ProJ (y,x,p))) * (ProJ (p,a,x)) by A7, VECTSP_1:def 10;

then ProJ (p,a,y) = ((ProJ (y,x,p)) * ((ProJ (x,y,p)) ")) * (ProJ (p,a,x)) ;

then ProJ (p,a,y) = (ProJ (y,x,p)) * (((ProJ (x,y,p)) ") * (ProJ (p,a,x))) by GROUP_1:def 3;

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, Th22;

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 3;

ProJ (y,p,x) <> 0. F by A4, A9, Th20;

then (ProJ (y,p,x)) * (ProJ (p,a,y)) = (((ProJ (x,y,p)) ") * (ProJ (p,a,x))) * (1_ F) by A10, VECTSP_1:def 10

.= ((ProJ (x,y,p)) ") * (ProJ (p,a,x)) ;

hence (ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x)) by A5, A8, Th22; :: thesis: verum

end;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 Th2;

(ProJ (p,a,y)) * ((ProJ (p,a,x)) ") = ProJ (p,x,y) by A1, A2, Th21;

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, Th24;

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 3;

then (ProJ (p,a,y)) * (1_ F) = (((ProJ (x,y,p)) ") * (ProJ (y,x,p))) * (ProJ (p,a,x)) by A7, VECTSP_1:def 10;

then ProJ (p,a,y) = ((ProJ (y,x,p)) * ((ProJ (x,y,p)) ")) * (ProJ (p,a,x)) ;

then ProJ (p,a,y) = (ProJ (y,x,p)) * (((ProJ (x,y,p)) ") * (ProJ (p,a,x))) by GROUP_1:def 3;

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, Th22;

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 3;

ProJ (y,p,x) <> 0. F by A4, A9, Th20;

then (ProJ (y,p,x)) * (ProJ (p,a,y)) = (((ProJ (x,y,p)) ") * (ProJ (p,a,x))) * (1_ F) by A10, VECTSP_1:def 10

.= ((ProJ (x,y,p)) ") * (ProJ (p,a,x)) ;

hence (ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x)) by A5, A8, Th22; :: thesis: verum

now :: thesis: ( x _|_ implies (ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x)) )

hence
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))
by A6; :: thesis: verumassume 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, Th20;

then A12: (ProJ (p,a,x)) * (ProJ (x,p,y)) = 0. F ;

y _|_ by A11, Th2;

then ProJ (y,p,x) = 0. F by A4, Th20;

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

end;then ProJ (x,p,y) = 0. F by A5, Th20;

then A12: (ProJ (p,a,x)) * (ProJ (x,p,y)) = 0. F ;

y _|_ by A11, Th2;

then ProJ (y,p,x) = 0. F by A4, Th20;

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