let n be Element of 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

consider a being 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 = (a,x) . W;
set p9 = (a,(x +* (m,(Double (x . m))))) . W;
set q = ((a,(x +* (m,(Double (x . m))))) . W) +* (m,(a @ (((a,(x +* (m,(Double (x . m))))) . W) . m)));
for i being Nat of n holds ((a,x) . W) . i = (((a,(x +* (m,(Double (x . m))))) . W) +* (m,(a @ (((a,(x +* (m,(Double (x . m))))) . W) . m)))) . i

proof

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

now

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

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

W . (a,((a,x) . W)) = x by Th17;
then A3: W . (a,(((a,x) . W) . m)) = x . m by Def12;
W . (a,((a,(x +* (m,(Double (x . m))))) . W)) = x +* (m,(Double (x . m))) by Th17;
then A4: W . (a,(((a,(x +* (m,(Double (x . m))))) . W) . m)) = (x +* (m,(Double (x . m)))) . m by Def12;
(x +* (m,(Double (x . m)))) . m = Double (x . m) by Th15;
then ((a,x) . W) . m = a @ (((a,(x +* (m,(Double (x . m))))) . W) . m) by A3, A4, MIDSP_2:37
.= (((a,(x +* (m,(Double (x . m))))) . W) +* (m,(a @ (((a,(x +* (m,(Double (x . m))))) . W) . m)))) . m by Th12 ;
hence ((a,x) . W) . i = (((a,(x +* (m,(Double (x . m))))) . W) +* (m,(a @ (((a,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A2; :: thesis: verum

end;

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

thus ((a,x) . W) . i = (a,(x . i)) . W by Def11
.= (a,((x +* (m,(Double (x . m)))) . i)) . W by A5, FUNCT_7:34
.= ((a,(x +* (m,(Double (x . m))))) . W) . i by Def11
.= (((a,(x +* (m,(Double (x . m))))) . W) +* (m,(a @ (((a,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A5, FUNCT_7:34 ; :: thesis: verum

end;

end;

end;

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

end;

then (a,x) . W = ((a,(x +* (m,(Double (x . m))))) . W) +* (m,(a @ (((a,(x +* (m,(Double (x . m))))) . W) . m))) by Th11;
then *' (a,((a,x) . W)) = a @ (*' (a,((a,(x +* (m,(Double (x . m))))) . W))) by A1, Def7;
then A6: W . (a,(*' (a,((a,(x +* (m,(Double (x . m))))) . W)))) = Double (W . (a,(*' (a,((a,x) . W))))) by MIDSP_2:37;
Phi (x +* (m,(Double (x . m)))) = W . (a,(*' (a,((a,(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 7 :: 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

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 Def12, Th12;
( ((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 Def12, Th15;
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:37; :: 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:34
.= W . (a,((p9 +* (m,(a @ (p9 . m)))) . i)) by Def12
.= W . (a,(p9 . i)) by A11, FUNCT_7:34
.= (W . (a,p9)) . i by Def12 ;
:: 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 Th16; :: 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:37; :: thesis: verum

end;