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, Th33;
then A3: - ((ProJ b,a,c) " ) <> 0. F by VECTSP_1:74;
ProJ b,a,c <> 0. F by A1, A2, Th33;
then (- (1_ F)) * (((ProJ b,a,c) " ) * (ProJ b,a,c)) = (- (1_ F)) * (1_ F) by VECTSP_1:def 22;
then ((- (1_ F)) * ((ProJ b,a,c) " )) * (ProJ b,a,c) = (- (1_ F)) * (1_ F) by GROUP_1:def 4;
then ((- (1_ F)) * ((ProJ b,a,c) " )) * (ProJ b,a,c) = - (1_ F) by VECTSP_1:def 19;
then (- (((ProJ b,a,c) " ) * (1_ F))) * (ProJ b,a,c) = - (1_ F) by VECTSP_1:41;
then (- ((ProJ b,a,c) " )) * (ProJ b,a,c) = - (1_ F) by VECTSP_1:def 19;
then ProJ b,a,((- ((ProJ b,a,c) " )) * c) = - (1_ F) by A1, Th25;
then b _|_ by A1, Th24;
then b _|_ by VECTSP_1:59;
then b _|_ by RLVECT_1:30;
then A4: ((- ((ProJ b,a,c) " )) * c) + a _|_ by Th12;
not a _|_ by A1, Th12;
then ProJ a,b,((- ((ProJ b,a,c) " )) * c) = - (ProJ ((- ((ProJ b,a,c) " )) * c),b,a) by A4, Th36;
then ProJ a,b,((- ((ProJ b,a,c) " )) * c) = - (ProJ c,b,a) by A2, A3, Th12, Th28;
then (- ((ProJ b,a,c) " )) * (ProJ a,b,c) = - (ProJ c,b,a) by A1, Th12, Th25;
then (- (((ProJ b,a,c) " ) * (ProJ a,b,c))) * (- (1_ F)) = (- (ProJ c,b,a)) * (- (1_ F)) by VECTSP_1:41;
then (((ProJ b,a,c) " ) * (ProJ a,b,c)) * (1_ F) = (- (ProJ c,b,a)) * (- (1_ F)) by VECTSP_1:42;
then (((ProJ b,a,c) " ) * (ProJ a,b,c)) * (1_ F) = (ProJ c,b,a) * (1_ F) by VECTSP_1:42;
then ((ProJ b,a,c) " ) * (ProJ a,b,c) = (ProJ c,b,a) * (1_ F) by VECTSP_1:def 19;
hence ProJ c,b,a = ((ProJ b,a,c) " ) * (ProJ a,b,c) by VECTSP_1:def 19; :: thesis: verum