let F be Field; :: thesis: for S being SymSp of F
for a, b, 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 a, b, x, y being Element of S st not a _|_ holds
ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))
let a, b, 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 3
.= ((x + y) + (- ((ProJ (a,b,x)) * b))) + (- ((ProJ (a,b,y)) * b)) by RLVECT_1:def 3
.= (x + y) + ((- ((ProJ (a,b,x)) * b)) + (- ((ProJ (a,b,y)) * b))) by RLVECT_1:def 3
.= (x + y) + (((1_ F) * (- ((ProJ (a,b,x)) * b))) + (- ((ProJ (a,b,y)) * b)))
.= (x + y) + (((1_ F) * (- ((ProJ (a,b,x)) * b))) + ((1_ F) * (- ((ProJ (a,b,y)) * b))))
.= (x + y) + (((1_ F) * ((- (ProJ (a,b,x))) * b)) + ((1_ F) * (- ((ProJ (a,b,y)) * b)))) by VECTSP_1:21
.= (x + y) + (((1_ F) * ((- (ProJ (a,b,x))) * b)) + ((1_ F) * ((- (ProJ (a,b,y))) * b))) by VECTSP_1:21
.= (x + y) + ((((1_ F) * (- (ProJ (a,b,x)))) * b) + ((1_ F) * ((- (ProJ (a,b,y))) * b)))
.= (x + y) + ((((- (ProJ (a,b,x))) * (1_ F)) * b) + (((1_ F) * (- (ProJ (a,b,y)))) * b))
.= (x + y) + (((- (ProJ (a,b,x))) * b) + (((- (ProJ (a,b,y))) * (1_ F)) * b))
.= (x + y) + (((- (ProJ (a,b,x))) * b) + ((- (ProJ (a,b,y))) * b))
.= (x + y) + (((- (ProJ (a,b,x))) + (- (ProJ (a,b,y)))) * b) by VECTSP_1:def 15
.= (x + y) + ((- ((ProJ (a,b,x)) + (ProJ (a,b,y)))) * b) by RLVECT_1:31
.= (x + y) - (((ProJ (a,b,x)) + (ProJ (a,b,y))) * b) by VECTSP_1:21 ;
assume A2: not a _|_ ; :: thesis: ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))
then ( a _|_ & a _|_ ) by Th14;
then A3: a _|_ by Def1;
a _|_ by A2, Th14;
hence ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y)) by A2, A3, A1, Th12; :: thesis: verum