let n be Nat; :: thesis: for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS holds
( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) )
let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n
for W being ATLAS of RAS holds
( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) )
let RAS be ReperAlgebra of n; :: thesis: for W being ATLAS of RAS holds
( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) )
let W be ATLAS of RAS; :: thesis: ( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) )
thus ( RAS is_semi_additive_in m implies for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) ) :: thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) ) implies RAS is_semi_additive_in m )

proof

set a = the Point of RAS;
assume A1: RAS is_semi_additive_in m ; :: thesis: for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x)
let x be Tuple of (n + 1),W; :: thesis: Phi (x +* (m,(Double (x . m)))) = Double (Phi x)
set x9 = x +* (m,(Double (x . m)));
set p = ( the Point of RAS,x) . W;
set p9 = ( the Point of RAS,(x +* (m,(Double (x . m))))) . W;
set q = (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)));
for i being Nat of n holds (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i

proof

let i be Nat of n; :: thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i

now :: thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i

per cases ( i = m or i <> m ) ;

suppose A2: i = m ; :: thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i

W . ( the Point of RAS,(( the Point of RAS,x) . W)) = x by Th15;
then A3: W . ( the Point of RAS,((( the Point of RAS,x) . W) . m)) = x . m by Def9;
W . ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)) = x +* (m,(Double (x . m))) by Th15;
then A4: W . ( the Point of RAS,((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)) = (x +* (m,(Double (x . m)))) . m by Def9;
(x +* (m,(Double (x . m)))) . m = Double (x . m) by Th13;
then (( the Point of RAS,x) . W) . m = the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m) by A3, A4, MIDSP_2:31
.= ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . m by Th10 ;
hence (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A2; :: thesis: verum

end;

suppose A5: i <> m ; :: thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i

thus (( the Point of RAS,x) . W) . i = ( the Point of RAS,(x . i)) . W by Def8
.= ( the Point of RAS,((x +* (m,(Double (x . m)))) . i)) . W by A5, FUNCT_7:32
.= (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . i by Def8
.= ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A5, FUNCT_7:32 ; :: thesis: verum

end;

end;

end;

hence (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i ; :: thesis: verum

end;

then ( the Point of RAS,x) . W = (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m))) by Th9;
then *' ( the Point of RAS,(( the Point of RAS,x) . W)) = the Point of RAS @ (*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W))) by A1;
then A6: W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)))) = Double (W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W))))) by MIDSP_2:31;
Phi (x +* (m,(Double (x . m)))) = W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)))) by Lm5;
hence Phi (x +* (m,(Double (x . m)))) = Double (Phi x) by A6, Lm5; :: thesis: verum

end;

thus ( ( for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) ) implies RAS is_semi_additive_in m ) :: thesis: verum

proof

assume A7: for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) ; :: thesis: RAS is_semi_additive_in m
let a be Point of RAS; :: according to MIDSP_3:def 5 :: thesis: for pii being Point of RAS
for p being Tuple of (n + 1),RAS st p . m = pii holds
*' (a,(p +* (m,(a @ pii)))) = a @ (*' (a,p))
let p9m be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS st p . m = p9m holds
*' (a,(p +* (m,(a @ p9m)))) = a @ (*' (a,p))
let p9 be Tuple of (n + 1),RAS; :: thesis: ( p9 . m = p9m implies *' (a,(p9 +* (m,(a @ p9m)))) = a @ (*' (a,p9)) )
assume A8: p9 . m = p9m ; :: thesis: *' (a,(p9 +* (m,(a @ p9m)))) = a @ (*' (a,p9))
set p = p9 +* (m,(a @ (p9 . m)));
set x = W . (a,(p9 +* (m,(a @ (p9 . m)))));
set x9 = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)));
W . (a,p9) = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))

proof

set y = W . (a,p9);
for i being Nat of n holds ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i

proof

let i be Nat of n; :: thesis: ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i

now :: thesis: ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i

per cases ( i = m or i <> m ) ;

suppose A9: i = m ; :: thesis: ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i

A10: ( W . (a,((p9 +* (m,(a @ (p9 . m)))) . m)) = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m & (p9 +* (m,(a @ (p9 . m)))) . m = a @ (p9 . m) ) by Def9, Th10;
( ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . m = Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m) & W . (a,(p9 . m)) = (W . (a,p9)) . m ) by Def9, Th13;
hence ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i by A9, A10, MIDSP_2:31; :: thesis: verum

end;

suppose A11: i <> m ; :: thesis: ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i

hence ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) . i by FUNCT_7:32
.= W . (a,((p9 +* (m,(a @ (p9 . m)))) . i)) by Def9
.= W . (a,(p9 . i)) by A11, FUNCT_7:32
.= (W . (a,p9)) . i by Def9 ;
:: thesis: verum

end;

end;

end;

hence ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i ; :: thesis: verum

end;

hence W . (a,p9) = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m))) by Th14; :: thesis: verum

end;

then A12: Phi ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) = W . (a,(*' (a,p9))) by Lm4;
Phi (W . (a,(p9 +* (m,(a @ (p9 . m)))))) = W . (a,(*' (a,(p9 +* (m,(a @ (p9 . m))))))) by Lm4;
then W . (a,(*' (a,p9))) = Double (W . (a,(*' (a,(p9 +* (m,(a @ (p9 . m)))))))) by A7, A12;
hence *' (a,(p9 +* (m,(a @ p9m)))) = a @ (*' (a,p9)) by A8, MIDSP_2:31; :: thesis: verum

end;