:: Reper Algebras
:: by Micha{\l} Muzalewski
::
:: Received May 28, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem :: MIDSP_3:1
theorem :: MIDSP_3:2
theorem :: MIDSP_3:3
theorem Th4: :: MIDSP_3:4
theorem :: MIDSP_3:5
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
Lm3:
now
let n be
Element of
NAT ;
:: thesis: 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-likelet M be
MidSp;
:: thesis: 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-likelet R be
Function of
(n + 2) -tuples_on the
carrier of
M,the
carrier of
M;
:: thesis: ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) is MidSp-likeset 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
:: thesis: verum
proof
let a,
b,
c,
d be
Element of
ReperAlgebraStr(# the
carrier of
M,the
MIDPOINT of
M,
R #);
:: according to MIDSP_1:def 4 :: thesis: ( 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 a' =
a,
b' =
b,
c' =
c,
d' =
d as
Element of
M ;
A1:
for
a,
b being
Element of
ReperAlgebraStr(# the
carrier of
M,the
MIDPOINT of
M,
R #)
for
a',
b' being
Element of
M st
a = a' &
b = b' holds
a @ b = a' @ b'
;
thus a @ a =
a' @ a'
.=
a
by MIDSP_1:def 4
;
:: thesis: ( 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 )
thus a @ b =
b' @ a'
by A1
.=
b @ a
;
:: thesis: ( (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 )
thus (a @ b) @ (c @ d) =
(a' @ b') @ (c' @ d')
.=
(a' @ c') @ (b' @ d')
by MIDSP_1:def 4
.=
(a @ c) @ (b @ d)
;
:: thesis: ex b1 being Element of the carrier of ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) st b1 @ a = b
consider x' being
Element of
M such that A2:
x' @ a' = b'
by MIDSP_1:def 4;
reconsider x =
x' as
Element of
ReperAlgebraStr(# the
carrier of
M,the
MIDPOINT of
M,
R #) ;
take
x
;
:: thesis: x @ a = b
thus
x @ a = b
by A2;
:: thesis: verum
end;
end;
:: deftheorem MIDSP_3:def 1 :
canceled;
:: deftheorem defines *' MIDSP_3:def 2 :
theorem :: MIDSP_3:6
canceled;
theorem :: MIDSP_3:7
:: deftheorem MIDSP_3:def 3 :
canceled;
:: deftheorem Def4 defines Nat MIDSP_3:def 4 :
theorem Th8: :: MIDSP_3:8
theorem :: MIDSP_3:9
canceled;
theorem Th10: :: MIDSP_3:10
theorem Th11: :: MIDSP_3:11
theorem Th12: :: MIDSP_3:12
:: deftheorem Def5 defines being_invariance MIDSP_3:def 5 :
:: deftheorem Def6 defines has_property_of_zero_in MIDSP_3:def 6 :
:: deftheorem Def7 defines is_semi_additive_in MIDSP_3:def 7 :
theorem Th13: :: MIDSP_3:13
:: deftheorem Def8 defines is_additive_in MIDSP_3:def 8 :
:: deftheorem Def9 defines is_alternative_in MIDSP_3:def 9 :
theorem :: MIDSP_3:14
theorem Th15: :: MIDSP_3:15
theorem Th16: :: MIDSP_3:16
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:
:: MIDSP_3:def 11
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 :
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:
:: MIDSP_3:def 12
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 :
theorem Th17: :: MIDSP_3:17
theorem :: MIDSP_3:18
theorem :: MIDSP_3:19
:: deftheorem defines Phi MIDSP_3:def 13 :
theorem Th20: :: MIDSP_3:20
theorem Th21: :: MIDSP_3:21
theorem Th22: :: MIDSP_3:22
theorem :: MIDSP_3:23
canceled;
theorem Th24: :: MIDSP_3:24
:: deftheorem Def14 defines ReperAlgebra MIDSP_3:def 14 :
theorem Th25: :: MIDSP_3:25
:: deftheorem Def15 defines Phi MIDSP_3:def 15 :
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: :: MIDSP_3:26
theorem Th27: :: MIDSP_3:27
theorem Th28: :: MIDSP_3:28
theorem Th29: :: MIDSP_3:29
theorem :: MIDSP_3:30
theorem Th31: :: MIDSP_3:31
theorem Th32: :: MIDSP_3:32
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, p'm, p''m being Point of RAS
for p being Tuple of (n + 1),RAS st a @ p''m = (p . m) @ p'm holds
( *' a,(p +* m,((p . m) @ p'm)) = (*' a,p) @ (*' a,(p +* m,p'm)) iff W . a,(*' a,(p +* m,p''m)) = (W . a,(*' a,p)) + (W . a,(*' a,(p +* m,p'm))) )
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 :: MIDSP_3:33
theorem Th34: :: MIDSP_3:34
theorem Th35: :: MIDSP_3:35
theorem :: MIDSP_3:36