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