let F be Field; :: thesis: for S being SymSp of F
for b, a, x, y being Element of S st not a _|_ holds
ProJ a,b,(x + y) = (ProJ a,b,x) + (ProJ a,b,y)
let S be SymSp of F; :: thesis: for b, a, x, y being Element of S st not a _|_ holds
ProJ a,b,(x + y) = (ProJ a,b,x) + (ProJ a,b,y)
let b, a, x, y be Element of S; :: thesis: ( not a _|_ implies ProJ a,b,(x + y) = (ProJ a,b,x) + (ProJ a,b,y) )
set 1F = 1_ F;
set L = (x - ((ProJ a,b,x) * b)) + (y - ((ProJ a,b,y) * b));
A1: (x - ((ProJ a,b,x) * b)) + (y - ((ProJ a,b,y) * b)) = (((- ((ProJ a,b,x) * b)) + x) + y) + (- ((ProJ a,b,y) * b)) by RLVECT_1:def 6
.= ((x + y) + (- ((ProJ a,b,x) * b))) + (- ((ProJ a,b,y) * b)) by RLVECT_1:def 6
.= (x + y) + ((- ((ProJ a,b,x) * b)) + (- ((ProJ a,b,y) * b))) by RLVECT_1:def 6
.= (x + y) + (((1_ F) * (- ((ProJ a,b,x) * b))) + (- ((ProJ a,b,y) * b))) by VECTSP_1:def 26
.= (x + y) + (((1_ F) * (- ((ProJ a,b,x) * b))) + ((1_ F) * (- ((ProJ a,b,y) * b)))) by VECTSP_1:def 26
.= (x + y) + (((1_ F) * ((- (ProJ a,b,x)) * b)) + ((1_ F) * (- ((ProJ a,b,y) * b)))) by VECTSP_1:68
.= (x + y) + (((1_ F) * ((- (ProJ a,b,x)) * b)) + ((1_ F) * ((- (ProJ a,b,y)) * b))) by VECTSP_1:68
.= (x + y) + ((((1_ F) * (- (ProJ a,b,x))) * b) + ((1_ F) * ((- (ProJ a,b,y)) * b))) by VECTSP_1:def 26
.= (x + y) + ((((- (ProJ a,b,x)) * (1_ F)) * b) + (((1_ F) * (- (ProJ a,b,y))) * b)) by VECTSP_1:def 26
.= (x + y) + (((- (ProJ a,b,x)) * b) + (((- (ProJ a,b,y)) * (1_ F)) * b)) by VECTSP_1:def 19
.= (x + y) + (((- (ProJ a,b,x)) * b) + ((- (ProJ a,b,y)) * b)) by VECTSP_1:def 19
.= (x + y) + (((- (ProJ a,b,x)) + (- (ProJ a,b,y))) * b) by VECTSP_1:def 26
.= (x + y) + ((- ((ProJ a,b,x) + (ProJ a,b,y))) * b) by RLVECT_1:45
.= (x + y) - (((ProJ a,b,x) + (ProJ a,b,y)) * b) by VECTSP_1:68 ;
assume A2: not a _|_ ; :: thesis: ProJ a,b,(x + y) = (ProJ a,b,x) + (ProJ a,b,y)
then ( a _|_ & a _|_ ) by Th27;
then A3: a _|_ by Def1;
a _|_ by A2, Th27;
hence ProJ a,b,(x + y) = (ProJ a,b,x) + (ProJ a,b,y) by A2, A3, A1, Th24; :: thesis: verum