begin
theorem
theorem
theorem
theorem Th4:
theorem
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
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 4 ( 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 4
;
( 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 4;
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 4
.=
(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;
:: deftheorem MIDSP_3:def 1 :
canceled;
:: deftheorem defines *' MIDSP_3:def 2 :
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' (a,p) = the reper of RAS . (<*a*> ^ p);
theorem
canceled;
theorem
:: deftheorem MIDSP_3:def 3 :
canceled;
:: deftheorem Def4 defines Nat MIDSP_3:def 4 :
for n, b2 being Element of NAT holds
( b2 is Nat of n iff ( 1 <= b2 & b2 <= n + 1 ) );
theorem Th8:
theorem
canceled;
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem Def5 defines being_invariance MIDSP_3:def 5 :
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2 holds
( RAS is being_invariance iff for a, b being Point of RAS
for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds
a @ (*' (b,q)) = b @ (*' (a,p)) );
:: deftheorem Def6 defines has_property_of_zero_in MIDSP_3:def 6 :
for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2 holds
( RAS has_property_of_zero_in i iff for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' (a,(p +* (i,a))) = a );
:: deftheorem Def7 defines is_semi_additive_in MIDSP_3:def 7 :
for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2 holds
( RAS is_semi_additive_in i iff for a, pii being Point of RAS
for p being Tuple of (n + 1),RAS st p . i = pii holds
*' (a,(p +* (i,(a @ pii)))) = a @ (*' (a,p)) );
theorem Th13:
:: deftheorem Def8 defines is_additive_in MIDSP_3:def 8 :
for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2 holds
( RAS is_additive_in i iff for a, pii, p9i being Point of RAS
for p being Tuple of (n + 1),RAS st p . i = pii holds
*' (a,(p +* (i,(pii @ p9i)))) = (*' (a,p)) @ (*' (a,(p +* (i,p9i)))) );
:: deftheorem Def9 defines is_alternative_in MIDSP_3:def 9 :
for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2 holds
( RAS is_alternative_in i iff for a being Point of RAS
for p being Tuple of (n + 1),RAS
for pii being Point of RAS st p . i = pii holds
*' (a,(p +* ((i + 1),pii))) = a );
theorem
theorem Th15:
theorem Th16:
definition
let n be
Element of
NAT ;
let RAS be non
empty MidSp-like ReperAlgebraStr of
n + 2;
let W be
ATLAS of
RAS;
let a be
Point of
RAS;
let x be
Tuple of
(n + 1),
W;
canceled;func (
a,
x)
. W -> Tuple of
(n + 1),
RAS means :
Def11:
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;
:: deftheorem MIDSP_3:def 10 :
canceled;
:: deftheorem Def11 defines . MIDSP_3:def 11 :
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of RAS
for a being Point of RAS
for x being Tuple of (n + 1),W
for b6 being Tuple of (n + 1),RAS holds
( b6 = (a,x) . W iff for m being Nat of n holds b6 . m = (a,(x . m)) . W );
definition
let n be
Element of
NAT ;
let RAS be non
empty MidSp-like ReperAlgebraStr of
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 :
Def12:
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;
:: deftheorem Def12 defines . MIDSP_3:def 12 :
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of RAS
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for b6 being Tuple of (n + 1),W holds
( b6 = W . (a,p) iff for m being Nat of n holds b6 . m = W . (a,(p . m)) );
theorem Th17:
theorem
theorem
:: deftheorem defines Phi MIDSP_3:def 13 :
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of RAS
for a being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = W . (a,(*' (a,((a,x) . W))));
theorem Th20:
theorem Th21:
theorem Th22:
theorem
canceled;
theorem Th24:
begin
:: deftheorem Def14 defines ReperAlgebra MIDSP_3:def 14 :
for n being Element of NAT
for b2 being non empty MidSp-like ReperAlgebraStr of n + 2 holds
( b2 is ReperAlgebra of n iff b2 is being_invariance );
theorem Th25:
:: deftheorem Def15 defines Phi MIDSP_3:def 15 :
for n being Element of NAT
for RAS being ReperAlgebra of n
for W being ATLAS of RAS
for x being Tuple of (n + 1),W
for b5 being Vector of W holds
( b5 = Phi x iff for a being Point of RAS holds b5 = Phi (a,x) );
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)))
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
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
theorem
theorem Th34:
theorem Th35:
theorem