let F be Field; :: thesis: for S being SymSp 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 SymSp 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))
A3: ProJ (b,a,c) <> 0. F by A1, A2, Th23;
then A4: - ((ProJ (b,a,c)) ") <> 0. F by VECTSP_1:25;
(- (1_ F)) * (((ProJ (b,a,c)) ") * (ProJ (b,a,c))) = (- (1_ F)) * (1_ F) by A3, 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, Th15;
then b _|_ by A1, Th14;
then b _|_ by VECTSP_1:14;
then b _|_ by RLVECT_1:17;
then A5: ((- ((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 A5, Th26;
then ProJ (a,b,((- ((ProJ (b,a,c)) ")) * c)) = ProJ (c,b,a) by A2, A4, Th2, Th18;
hence ProJ (c,b,a) = (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c)) by A1, Th2, Th15; :: thesis: verum