let n be Nat; for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS has_property_of_zero_in m holds
( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
let m be Nat of n; for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS has_property_of_zero_in m holds
( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
let RAS be ReperAlgebra of n; for W being ATLAS of RAS st RAS has_property_of_zero_in m holds
( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
let W be ATLAS of RAS; ( RAS has_property_of_zero_in m implies ( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) )
assume A1:
RAS has_property_of_zero_in m
; ( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
thus
( RAS is_additive_in m implies for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
( ( for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) implies RAS is_additive_in m )proof
set a = the
Point of
RAS;
assume A2:
RAS is_additive_in m
;
for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))
let x be
Tuple of
(n + 1),
W;
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))let v be
Vector of
W;
Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))
set p = ( the
Point of
RAS,
x)
. W;
set p9m = ( the
Point of
RAS,
v)
. W;
consider p99m being
Point of
RAS such that A3:
p99m @ the
Point of
RAS = ((( the Point of RAS,x) . W) . m) @ (( the Point of RAS,v) . W)
by MIDSP_1:def 3;
A4:
(
W . ( the
Point of
RAS,
(( the Point of RAS,x) . W))
= x &
W . ( the
Point of
RAS,
(( the Point of RAS,v) . W))
= v )
by Th15, MIDSP_2:33;
A5:
W . ( the
Point of
RAS,
p99m) =
(W . ( the Point of RAS,((( the Point of RAS,x) . W) . m))) + (W . ( the Point of RAS,(( the Point of RAS,v) . W)))
by A3, MIDSP_2:30
.=
(x . m) + v
by A4, Def9
;
(( the Point of RAS,x) . W) +* (
m,
p99m)
= ( the
Point of
RAS,
(x +* (m,((x . m) + v))))
. W
proof
set pp =
(( the Point of RAS,x) . W) +* (
m,
p99m);
set xx =
x +* (
m,
((x . m) + v));
set qq = ( the
Point of
RAS,
(x +* (m,((x . m) + v))))
. W;
for
i being
Nat of
n holds
((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i
hence
(( the Point of RAS,x) . W) +* (
m,
p99m)
= ( the
Point of
RAS,
(x +* (m,((x . m) + v))))
. W
by Th9;
verum
end;
then A8:
Phi (x +* (m,((x . m) + v))) = W . ( the
Point of
RAS,
(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,p99m)))))
by Lm5;
A9:
(( the Point of RAS,x) . W) +* (
m,
(( the Point of RAS,v) . W))
= ( the
Point of
RAS,
(x +* (m,v)))
. W
proof
set pp =
(( the Point of RAS,x) . W) +* (
m,
(( the Point of RAS,v) . W));
set qq = ( the
Point of
RAS,
(x +* (m,v)))
. W;
for
i being
Nat of
n holds
((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i
proof
let i be
Nat of
n;
((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i
per cases
( i = m or i <> m )
;
suppose A11:
i <> m
;
((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . ihence ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i =
(( the Point of RAS,x) . W) . i
by FUNCT_7:32
.=
( the
Point of
RAS,
(x . i))
. W
by Def8
.=
( the
Point of
RAS,
((x +* (m,v)) . i))
. W
by A11, FUNCT_7:32
.=
(( the Point of RAS,(x +* (m,v))) . W) . i
by Def8
;
verum end; end;
end;
hence
(( the Point of RAS,x) . W) +* (
m,
(( the Point of RAS,v) . W))
= ( the
Point of
RAS,
(x +* (m,v)))
. W
by Th9;
verum
end;
(
RAS is_semi_additive_in m &
*' ( the
Point of
RAS,
((( the Point of RAS,x) . W) +* (m,(((( the Point of RAS,x) . W) . m) @ (( the Point of RAS,v) . W)))))
= (*' ( the Point of RAS,(( the Point of RAS,x) . W))) @ (*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))))) )
by A1, A2, Th29;
then A12:
W . ( the
Point of
RAS,
(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,p99m)))))
= (W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W))))) + (W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W)))))))
by A3, Lm6;
Phi x = W . ( the
Point of
RAS,
(*' ( the Point of RAS,(( the Point of RAS,x) . W))))
by Lm5;
hence
Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))
by A12, A8, A9, Lm5;
verum
end;
thus
( ( for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) implies RAS is_additive_in m )
verumproof
assume A13:
for
x being
Tuple of
(n + 1),
W for
v being
Vector of
W holds
Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))
;
RAS is_additive_in m
then A14:
RAS is_semi_additive_in m
by Lm7;
for
a,
pm,
p9m being
Point of
RAS for
p being
Tuple of
(n + 1),
RAS st
p . m = pm holds
*' (
a,
(p +* (m,(pm @ p9m))))
= (*' (a,p)) @ (*' (a,(p +* (m,p9m))))
proof
let a,
pm,
p9m be
Point of
RAS;
for p being Tuple of (n + 1),RAS st p . m = pm holds
*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))let p be
Tuple of
(n + 1),
RAS;
( p . m = pm implies *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) )
assume A15:
p . m = pm
;
*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))
set x =
W . (
a,
p);
set v =
W . (
a,
p9m);
consider p99m being
Point of
RAS such that A16:
p99m @ a = (p . m) @ p9m
by MIDSP_1:def 3;
A17:
(
a,
(W . (a,p)))
. W = p
by Th15;
A18:
W . (
a,
p99m) =
(W . (a,(p . m))) + (W . (a,p9m))
by A16, MIDSP_2:30
.=
((W . (a,p)) . m) + (W . (a,p9m))
by Def9
;
p +* (
m,
p99m)
= (
a,
((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))))
. W
proof
set pp =
p +* (
m,
p99m);
set xx =
(W . (a,p)) +* (
m,
(((W . (a,p)) . m) + (W . (a,p9m))));
set qq = (
a,
((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))))
. W;
for
i being
Nat of
n holds
(p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i
proof
let i be
Nat of
n;
(p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i
per cases
( i = m or i <> m )
;
suppose A19:
i = m
;
(p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . ihence (p +* (m,p99m)) . i =
p99m
by Th10
.=
(
a,
(((W . (a,p)) . m) + (W . (a,p9m))))
. W
by A18, MIDSP_2:33
.=
(
a,
(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . m))
. W
by Th13
.=
((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i
by A19, Def8
;
verum end; suppose A20:
i <> m
;
(p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . ihence (p +* (m,p99m)) . i =
p . i
by FUNCT_7:32
.=
(
a,
((W . (a,p)) . i))
. W
by A17, Def8
.=
(
a,
(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . i))
. W
by A20, FUNCT_7:32
.=
((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i
by Def8
;
verum end; end;
end;
hence
p +* (
m,
p99m)
= (
a,
((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))))
. W
by Th9;
verum
end;
then A21:
Phi ((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) = W . (
a,
(*' (a,(p +* (m,p99m)))))
by Lm5;
A22:
(
a,
(W . (a,p9m)))
. W = p9m
by MIDSP_2:33;
p +* (
m,
p9m)
= (
a,
((W . (a,p)) +* (m,(W . (a,p9m)))))
. W
proof
set pp =
p +* (
m,
p9m);
set qq = (
a,
((W . (a,p)) +* (m,(W . (a,p9m)))))
. W;
for
i being
Nat of
n holds
(p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i
proof
let i be
Nat of
n;
(p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i
per cases
( i = m or i <> m )
;
suppose A23:
i = m
;
(p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . ihence (p +* (m,p9m)) . i =
p9m
by Th10
.=
(
a,
(((W . (a,p)) +* (m,(W . (a,p9m)))) . m))
. W
by A22, Th13
.=
((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i
by A23, Def8
;
verum end; suppose A24:
i <> m
;
(p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . ihence (p +* (m,p9m)) . i =
p . i
by FUNCT_7:32
.=
(
a,
((W . (a,p)) . i))
. W
by A17, Def8
.=
(
a,
(((W . (a,p)) +* (m,(W . (a,p9m)))) . i))
. W
by A24, FUNCT_7:32
.=
((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i
by Def8
;
verum end; end;
end;
hence
p +* (
m,
p9m)
= (
a,
((W . (a,p)) +* (m,(W . (a,p9m)))))
. W
by Th9;
verum
end;
then A25:
Phi ((W . (a,p)) +* (m,(W . (a,p9m)))) = W . (
a,
(*' (a,(p +* (m,p9m)))))
by Lm5;
Phi (W . (a,p)) = W . (
a,
(*' (a,p)))
by Lm4;
then
W . (
a,
(*' (a,(p +* (m,p99m)))))
= (W . (a,(*' (a,p)))) + (W . (a,(*' (a,(p +* (m,p9m))))))
by A13, A21, A25;
hence
*' (
a,
(p +* (m,(pm @ p9m))))
= (*' (a,p)) @ (*' (a,(p +* (m,p9m))))
by A14, A15, A16, Lm6;
verum
end;
hence
RAS is_additive_in m
;
verum
end;