begin
Lm1:
for n, i being Element of NAT
for D being non empty set
for d being Element of D
for p being Element of n -tuples_on D st i in Seg n holds
(p +* (i,d)) . i = d
Lm2:
for n, i being Element of NAT
for D being non empty set
for d being Element of D
for p being Element of n -tuples_on D
for l being Element of NAT st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l
begin
Lm3:
now for n being Element of NAT
for M being MidSp
for R being Function of ((n + 2) -tuples_on the carrier of M), the carrier of M holds ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) is MidSp-like
let n be
Element of
NAT ;
for M being MidSp
for R being Function of ((n + 2) -tuples_on the carrier of M), the carrier of M holds ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) is MidSp-like let M be
MidSp;
for R being Function of ((n + 2) -tuples_on the carrier of M), the carrier of M holds ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) is MidSp-like let R be
Function of
((n + 2) -tuples_on the carrier of M), the
carrier of
M;
ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) is MidSp-like set RA =
ReperAlgebraStr(# the
carrier of
M, the
MIDPOINT of
M,
R #);
thus
ReperAlgebraStr(# the
carrier of
M, the
MIDPOINT of
M,
R #) is
MidSp-like
verum
proof
let a,
b,
c,
d be
Element of
ReperAlgebraStr(# the
carrier of
M, the
MIDPOINT of
M,
R #);
MIDSP_1:def 3 ( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex b1 being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b1 @ a = b )
reconsider a9 =
a,
b9 =
b,
c9 =
c,
d9 =
d as
Element of
M ;
thus a @ a =
a9 @ a9
.=
a
by MIDSP_1:def 3
;
( a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex b1 being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b1 @ a = b )
consider x9 being
Element of
M such that A1:
x9 @ a9 = b9
by MIDSP_1:def 3;
for
a,
b being
Element of
ReperAlgebraStr(# the
carrier of
M, the
MIDPOINT of
M,
R #)
for
a9,
b9 being
Element of
M st
a = a9 &
b = b9 holds
a @ b = a9 @ b9
;
hence a @ b =
b9 @ a9
.=
b @ a
;
( (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex b1 being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b1 @ a = b )
reconsider x =
x9 as
Element of
ReperAlgebraStr(# the
carrier of
M, the
MIDPOINT of
M,
R #) ;
thus (a @ b) @ (c @ d) =
(a9 @ b9) @ (c9 @ d9)
.=
(a9 @ c9) @ (b9 @ d9)
by MIDSP_1:def 3
.=
(a @ c) @ (b @ d)
;
ex b1 being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b1 @ a = b
take
x
;
x @ a = b
thus
x @ a = b
by A1;
verum
end;
end;
definition
let n be
Element of
NAT ;
let RAS be non
empty MidSp-like ReperAlgebraStr over
n + 2;
let W be
ATLAS of
RAS;
let a be
Point of
RAS;
let x be
Tuple of
(n + 1),
W;
func (
a,
x)
. W -> Tuple of
(n + 1),
RAS means :
Def8:
for
m being
Nat of
n holds
it . m = (
a,
(x . m))
. W;
existence
ex b1 being Tuple of (n + 1),RAS st
for m being Nat of n holds b1 . m = (a,(x . m)) . W
uniqueness
for b1, b2 being Tuple of (n + 1),RAS st ( for m being Nat of n holds b1 . m = (a,(x . m)) . W ) & ( for m being Nat of n holds b2 . m = (a,(x . m)) . W ) holds
b1 = b2
end;
definition
let n be
Element of
NAT ;
let RAS be non
empty MidSp-like ReperAlgebraStr over
n + 2;
let W be
ATLAS of
RAS;
let a be
Point of
RAS;
let p be
Tuple of
(n + 1),
RAS;
func W . (
a,
p)
-> Tuple of
(n + 1),
W means :
Def9:
for
m being
Nat of
n holds
it . m = W . (
a,
(p . m));
existence
ex b1 being Tuple of (n + 1),W st
for m being Nat of n holds b1 . m = W . (a,(p . m))
uniqueness
for b1, b2 being Tuple of (n + 1),W st ( for m being Nat of n holds b1 . m = W . (a,(p . m)) ) & ( for m being Nat of n holds b2 . m = W . (a,(p . m)) ) holds
b1 = b2
end;
begin
Lm4:
for n being Element of NAT
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st W . (a,p) = x holds
Phi x = W . (a,(*' (a,p)))
Lm5:
for n being Element of NAT
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st (a,x) . W = p holds
Phi x = W . (a,(*' (a,p)))
Lm6:
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS is_semi_additive_in m holds
for a, p9m, p99m being Point of RAS
for p being Tuple of (n + 1),RAS st a @ p99m = (p . m) @ p9m holds
( *' (a,(p +* (m,((p . m) @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) iff W . (a,(*' (a,(p +* (m,p99m))))) = (W . (a,(*' (a,p)))) + (W . (a,(*' (a,(p +* (m,p9m)))))) )
Lm7:
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st ( 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))) ) holds
RAS is_semi_additive_in m