let F be Field; :: thesis: for S being SymSp of F
for a, b, c being Element of S st not a _|_ & c + a _|_ holds
ProJ (a,b,c) = ProJ (c,b,a)
let S be SymSp of F; :: thesis: for a, b, c being Element of S st not a _|_ & c + a _|_ holds
ProJ (a,b,c) = ProJ (c,b,a)
let a, b, c be Element of S; :: thesis: ( not a _|_ & c + a _|_ implies ProJ (a,b,c) = ProJ (c,b,a) )
assume that
A1: not a _|_ and
A2: c + a _|_ ; :: thesis: ProJ (a,b,c) = ProJ (c,b,a)
c + a _|_ by A2, Def1;
then A3: c + a _|_ by Th6;
a _|_ by A1, Th14;
then (- ((ProJ (a,b,c)) * b)) + c _|_ by Th2;
then a + (- ((ProJ (a,b,c)) * b)) _|_ by A3, Def1;
then A4: c _|_ by Th2;
( not b _|_ & b _|_ ) by A1, A2, Th2;
then not b _|_ by Th3;
then A5: not c _|_ by Th2;
then c _|_ by Th14;
hence ProJ (a,b,c) = ProJ (c,b,a) by A5, A4, Th12; :: thesis: verum