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