let F be Field; :: thesis: for S being SymSp of F
for b, a, x, y, z being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ a,b,x,(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)
let S be SymSp of F; :: thesis: for b, a, x, y, z being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ a,b,x,(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)
let b, a, x, y, z be Element of S; :: thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ implies PProJ a,b,x,(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z) )
assume that
A1:
(1_ F) + (1_ F) <> 0. F
and
A2:
not a _|_
; :: thesis: PProJ a,b,x,(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)
set 0F = 0. F;
A3:
now assume
x = 0. S
;
:: thesis: PProJ a,b,x,(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)then
(
PProJ a,
b,
x,
(y + z) = 0. F &
PProJ a,
b,
x,
y = 0. F &
PProJ a,
b,
x,
z = 0. F )
by A1, A2, Th47;
hence
PProJ a,
b,
x,
(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)
by RLVECT_1:10;
:: thesis: verum end;
now assume
x <> 0. S
;
:: thesis: PProJ a,b,x,(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)then
(
a <> 0. S &
x <> 0. S )
by A2, Th11, Th12;
then consider p being
Element of
S such that A4:
( not
a _|_ & not
x _|_ )
by Th21;
A5:
PProJ a,
b,
x,
(y + z) = ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,(y + z))
by A1, A2, A4, Def6;
A6:
PProJ a,
b,
x,
y = ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y)
by A1, A2, A4, Def6;
A7:
PProJ a,
b,
x,
z = ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,z)
by A1, A2, A4, Def6;
ProJ x,
p,
(y + z) = (ProJ x,p,y) + (ProJ x,p,z)
by A4, Th29;
hence
PProJ a,
b,
x,
(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)
by A5, A6, A7, VECTSP_1:def 18;
:: thesis: verum end;
hence
PProJ a,b,x,(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)
by A3; :: thesis: verum