let F be Field; 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; 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; ( 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 _|_
; (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 ( 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, Th23;
assume A8:
not
x _|_
;
(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, 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 A5, A8, Th27;
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, Th25;
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, Th23;
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;
then
(ProJ (p,a,y)) * (ProJ (y,p,x)) = (- ((ProJ (x,y,p)) ")) * (ProJ (p,a,x))
;
then
- ((ProJ (p,a,y)) * (ProJ (y,p,x))) = - (- (((ProJ (x,y,p)) ") * (ProJ (p,a,x))))
by VECTSP_1:9;
then
- ((ProJ (p,a,y)) * (ProJ (y,p,x))) = ((ProJ (x,y,p)) ") * (ProJ (p,a,x))
by RLVECT_1:17;
then
(- (ProJ (p,a,y))) * (ProJ (y,p,x)) = ((ProJ (x,y,p)) ") * (ProJ (p,a,x))
by VECTSP_1:9;
hence
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))
by A5, A8, Th25;
verum end;
now ( x _|_ implies (ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x)) )assume A11:
x _|_
;
(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, Th23;
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, Th23;
hence
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))
by A12;
verum end;
hence
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))
by A6; verum