let F be Field; :: thesis: for S being OrtSp of F

for a, b, x, y, z being Element of S st not a _|_ holds

PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

let S be OrtSp of F; :: thesis: for a, b, x, y, z being Element of S st not a _|_ holds

PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

let a, b, x, y, z be Element of S; :: thesis: ( not a _|_ implies PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) )

set 0F = 0. F;

assume A1: not a _|_ ; :: thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

for a, b, x, y, z being Element of S st not a _|_ holds

PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

let S be OrtSp of F; :: thesis: for a, b, x, y, z being Element of S st not a _|_ holds

PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

let a, b, x, y, z be Element of S; :: thesis: ( not a _|_ implies PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) )

set 0F = 0. F;

assume A1: not a _|_ ; :: thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

A2: now :: thesis: ( x <> 0. S implies PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) )

assume A3:
x <> 0. S
; :: thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

a <> 0. S by A1, Th1, Th2;

then ex p being Element of S st

( not a _|_ & not x _|_ & not a _|_ & not x _|_ ) by A3, Def1;

then consider p being Element of S such that

A4: ( not a _|_ & not x _|_ ) ;

A5: ( PProJ (a,b,x,(y + z)) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,(y + z))) & PProJ (a,b,x,y) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) ) by A1, A4, Def3;

( PProJ (a,b,x,z) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,z)) & ProJ (x,p,(y + z)) = (ProJ (x,p,y)) + (ProJ (x,p,z)) ) by A1, A4, Def3, Th13;

hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A5, VECTSP_1:def 7; :: thesis: verum

end;a <> 0. S by A1, Th1, Th2;

then ex p being Element of S st

( not a _|_ & not x _|_ & not a _|_ & not x _|_ ) by A3, Def1;

then consider p being Element of S such that

A4: ( not a _|_ & not x _|_ ) ;

A5: ( PProJ (a,b,x,(y + z)) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,(y + z))) & PProJ (a,b,x,y) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) ) by A1, A4, Def3;

( PProJ (a,b,x,z) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,z)) & ProJ (x,p,(y + z)) = (ProJ (x,p,y)) + (ProJ (x,p,z)) ) by A1, A4, Def3, Th13;

hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A5, VECTSP_1:def 7; :: thesis: verum

now :: thesis: ( x = 0. S implies PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) )

hence
PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
by A2; :: thesis: verumassume A6:
x = 0. S
; :: thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

then A7: PProJ (a,b,x,z) = 0. F by A1, Th28;

( PProJ (a,b,x,(y + z)) = 0. F & PProJ (a,b,x,y) = 0. F ) by A1, A6, Th28;

hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A7, RLVECT_1:4; :: thesis: verum

end;then A7: PProJ (a,b,x,z) = 0. F by A1, Th28;

( PProJ (a,b,x,(y + z)) = 0. F & PProJ (a,b,x,y) = 0. F ) by A1, A6, Th28;

hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A7, RLVECT_1:4; :: thesis: verum