:: by Micha{\l} Muzalewski

::

:: Received May 28, 1992

:: Copyright (c) 1992-2021 Association of Mizar Users

theorem :: MIDSP_3:1

for j, k being Nat

for D being non empty set

for p being FinSequence of D st len p = (j + 1) + k holds

ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

for D being non empty set

for p being FinSequence of D st len p = (j + 1) + k holds

ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

proof end;

theorem :: MIDSP_3:3

for i being Nat

for D being non empty set

for c being Element of D

for p, q, r being FinSequence of D st p = (q ^ <*c*>) ^ r & i = (len q) + 1 holds

( ( for l being Nat st 1 <= l & l <= len q holds

p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds

p . l = r . (l - i) ) )

for D being non empty set

for c being Element of D

for p, q, r being FinSequence of D st p = (q ^ <*c*>) ^ r & i = (len q) + 1 holds

( ( for l being Nat st 1 <= l & l <= len q holds

p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds

p . l = r . (l - i) ) )

proof end;

theorem :: MIDSP_3:5

for n, i, j, l being Nat st l in (Seg n) \ {i} & i = j + 1 & not ( 1 <= l & l <= j ) holds

( i + 1 <= l & l <= n )

( i + 1 <= l & l <= n )

proof end;

definition

let D be non empty set ;

let n be Nat;

let p be Element of n -tuples_on D;

let i be Nat;

let d be Element of D;

:: original: +*

redefine func p +* (i,d) -> Element of n -tuples_on D;

coherence

p +* (i,d) is Element of n -tuples_on D

end;
let n be Nat;

let p be Element of n -tuples_on D;

let i be Nat;

let d be Element of D;

:: original: +*

redefine func p +* (i,d) -> Element of n -tuples_on D;

coherence

p +* (i,d) is Element of n -tuples_on D

proof end;

Lm1: for n, i being 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

proof end;

Lm2: for n, i being 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 Nat st l in (dom p) \ {i} holds

(p +* (i,d)) . l = p . l

proof end;

definition

let n be Nat;

attr c_{2} is strict ;

struct ReperAlgebraStr over n -> MidStr ;

aggr ReperAlgebraStr(# carrier, MIDPOINT, reper #) -> ReperAlgebraStr over n;

sel reper c_{2} -> Function of (n -tuples_on the carrier of c_{2}), the carrier of c_{2};

end;
attr c

struct ReperAlgebraStr over n -> MidStr ;

aggr ReperAlgebraStr(# carrier, MIDPOINT, reper #) -> ReperAlgebraStr over n;

sel reper c

registration

let n be Nat;

let A be non empty set ;

let m be BinOp of A;

let r be Function of (n -tuples_on A),A;

coherence

not ReperAlgebraStr(# A,m,r #) is empty ;

end;
let A be non empty set ;

let m be BinOp of A;

let r be Function of (n -tuples_on A),A;

coherence

not ReperAlgebraStr(# A,m,r #) is empty ;

Lm3: now :: thesis: for n being 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

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 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-like

let 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-like

let 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-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 :: thesis: verum

end;
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; :: 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-like

let 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-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 :: 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 3 :: thesis: ( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex b_{1} being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b_{1} @ 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 ; :: thesis: ( a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex b_{1} being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b_{1} @ 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 ;

:: thesis: ( (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex b_{1} being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b_{1} @ 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) ; :: thesis: ex b_{1} being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b_{1} @ a = b

take x ; :: thesis: x @ a = b

thus x @ a = b by A1; :: thesis: verum

end;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of M ;

thus a @ a = a9 @ a9

.= a by MIDSP_1:def 3 ; :: thesis: ( a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex 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 ;

:: thesis: ( (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex 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) ; :: thesis: ex b

take x ; :: thesis: x @ a = b

thus x @ a = b by A1; :: thesis: verum

registration
end;

registration

let n be Nat;

existence

ex b_{1} being non empty ReperAlgebraStr over n + 2 st b_{1} is MidSp-like

end;
existence

ex b

proof end;

definition

let n be Nat;

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let i be Nat;

mode Tuple of i,RAS is Element of i -tuples_on the carrier of RAS;

end;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let i be Nat;

mode Tuple of i,RAS is Element of i -tuples_on the carrier of RAS;

definition

let n be Nat;

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let a be Point of RAS;

:: original: <*

redefine func <*a*> -> Tuple of 1,RAS;

coherence

<*a*> is Tuple of 1,RAS by FINSEQ_2:98;

end;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let a be Point of RAS;

:: original: <*

redefine func <*a*> -> Tuple of 1,RAS;

coherence

<*a*> is Tuple of 1,RAS by FINSEQ_2:98;

definition

let n be Nat;

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let i, j be Nat;

let p be Tuple of i,RAS;

let q be Tuple of j,RAS;

:: original: ^

redefine func p ^ q -> Tuple of (i + j),RAS;

coherence

p ^ q is Tuple of (i + j),RAS

end;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let i, j be Nat;

let p be Tuple of i,RAS;

let q be Tuple of j,RAS;

:: original: ^

redefine func p ^ q -> Tuple of (i + j),RAS;

coherence

p ^ q is Tuple of (i + j),RAS

proof end;

definition

let n be Nat;

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let a be Point of RAS;

let p be Tuple of (n + 1),RAS;

coherence

the reper of RAS . (<*a*> ^ p) is Point of RAS

end;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let a be Point of RAS;

let p be Tuple of (n + 1),RAS;

coherence

the reper of RAS . (<*a*> ^ p) is Point of RAS

proof end;

:: deftheorem defines *' MIDSP_3:def 1 :

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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);

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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 :: MIDSP_3:6

definition
end;

:: deftheorem Def2 defines Nat MIDSP_3:def 2 :

for n, b_{2} being Nat holds

( b_{2} is Nat of n iff ( 1 <= b_{2} & b_{2} <= n + 1 ) );

for n, b

( b

theorem Th9: :: MIDSP_3:9

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds p . m = q . m ) holds

p = q

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds p . m = q . m ) holds

p = q

proof end;

theorem Th10: :: MIDSP_3:10

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for d being Point of RAS

for p being Tuple of (n + 1),RAS

for l being Nat of n st l = i holds

(p +* (i,d)) . l = d

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for d being Point of RAS

for p being Tuple of (n + 1),RAS

for l being Nat of n st l = i holds

(p +* (i,d)) . l = d

proof end;

definition

let n be Nat;

let D be non empty set ;

let p be Element of (n + 1) -tuples_on D;

let m be Nat of n;

:: original: .

redefine func p . m -> Element of D;

coherence

p . m is Element of D

end;
let D be non empty set ;

let p be Element of (n + 1) -tuples_on D;

let m be Nat of n;

:: original: .

redefine func p . m -> Element of D;

coherence

p . m is Element of D

proof end;

:: deftheorem defines being_invariance MIDSP_3:def 3 :

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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)) );

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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)) );

definition

let n be Nat;

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let p be Tuple of (n + 1),RAS;

let i be Nat;

let a be Point of RAS;

:: original: +*

redefine func p +* (i,a) -> Tuple of (n + 1),RAS;

coherence

p +* (i,a) is Tuple of (n + 1),RAS

end;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let p be Tuple of (n + 1),RAS;

let i be Nat;

let a be Point of RAS;

:: original: +*

redefine func p +* (i,a) -> Tuple of (n + 1),RAS;

coherence

p +* (i,a) is Tuple of (n + 1),RAS

proof end;

definition

let n, i be Nat;

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

end;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

pred RAS has_property_of_zero_in i means :: MIDSP_3:def 4

for a being Point of RAS

for p being Tuple of (n + 1),RAS holds *' (a,(p +* (i,a))) = a;

for a being Point of RAS

for p being Tuple of (n + 1),RAS holds *' (a,(p +* (i,a))) = a;

:: deftheorem defines has_property_of_zero_in MIDSP_3:def 4 :

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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 );

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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 defines is_semi_additive_in MIDSP_3:def 5 :

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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)) );

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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 Th11: :: MIDSP_3:11

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for m being Nat of n st RAS is_semi_additive_in m holds

for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for m being Nat of n st RAS is_semi_additive_in m holds

for a, d being Point of RAS

for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds

*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))

proof end;

:: deftheorem defines is_additive_in MIDSP_3:def 6 :

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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)))) );

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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 defines is_alternative_in MIDSP_3:def 7 :

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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 );

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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 );

definition

let n be Nat;

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let W be ATLAS of RAS;

let i be Nat;

mode Tuple of i,W is Element of i -tuples_on the carrier of the algebra of W;

end;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;

let W be ATLAS of RAS;

let i be Nat;

mode Tuple of i,W is Element of i -tuples_on the carrier of the algebra of W;

theorem :: MIDSP_3:12

theorem Th13: :: MIDSP_3:13

for n, i being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W holds

( ( for l being Nat of n st l = i holds

(x +* (i,v)) . l = v ) & ( for l, i being Nat of n st l <> i holds

(x +* (i,v)) . l = x . l ) )

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W holds

( ( for l being Nat of n st l = i holds

(x +* (i,v)) . l = v ) & ( for l, i being Nat of n st l <> i holds

(x +* (i,v)) . l = x . l ) )

proof end;

theorem Th14: :: MIDSP_3:14

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS

for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds

x = y

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS

for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds

x = y

proof end;

definition

let n be 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;

ex b_{1} being Tuple of (n + 1),RAS st

for m being Nat of n holds b_{1} . m = (a,(x . m)) . W

for b_{1}, b_{2} being Tuple of (n + 1),RAS st ( for m being Nat of n holds b_{1} . m = (a,(x . m)) . W ) & ( for m being Nat of n holds b_{2} . m = (a,(x . m)) . W ) holds

b_{1} = b_{2}

end;
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: :: MIDSP_3:def 8

for m being Nat of n holds it . m = (a,(x . m)) . W;

existence for m being Nat of n holds it . m = (a,(x . m)) . W;

ex b

for m being Nat of n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines . MIDSP_3:def 8 :

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS

for a being Point of RAS

for x being Tuple of (n + 1),W

for b_{6} being Tuple of (n + 1),RAS holds

( b_{6} = (a,x) . W iff for m being Nat of n holds b_{6} . m = (a,(x . m)) . W );

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS

for a being Point of RAS

for x being Tuple of (n + 1),W

for b

( b

definition

let n be 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;

ex b_{1} being Tuple of (n + 1),W st

for m being Nat of n holds b_{1} . m = W . (a,(p . m))

for b_{1}, b_{2} being Tuple of (n + 1),W st ( for m being Nat of n holds b_{1} . m = W . (a,(p . m)) ) & ( for m being Nat of n holds b_{2} . m = W . (a,(p . m)) ) holds

b_{1} = b_{2}

end;
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: :: MIDSP_3:def 9

for m being Nat of n holds it . m = W . (a,(p . m));

existence for m being Nat of n holds it . m = W . (a,(p . m));

ex b

for m being Nat of n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines . MIDSP_3:def 9 :

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS

for a being Point of RAS

for p being Tuple of (n + 1),RAS

for b_{6} being Tuple of (n + 1),W holds

( b_{6} = W . (a,p) iff for m being Nat of n holds b_{6} . m = W . (a,(p . m)) );

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS

for a being Point of RAS

for p being Tuple of (n + 1),RAS

for b

( b

theorem Th15: :: MIDSP_3:15

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

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 holds

( W . (a,p) = x iff (a,x) . W = p )

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

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 holds

( W . (a,p) = x iff (a,x) . W = p )

proof end;

theorem :: MIDSP_3:16

theorem :: MIDSP_3:17

definition

let n be 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;

coherence

W . (a,(*' (a,((a,x) . W)))) is Vector of W ;

end;
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;

coherence

W . (a,(*' (a,((a,x) . W)))) is Vector of W ;

:: deftheorem defines Phi MIDSP_3:def 10 :

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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))));

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over 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 Th18: :: MIDSP_3:18

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v holds

( *' (a,p) = b iff Phi (a,x) = v )

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v holds

( *' (a,p) = b iff Phi (a,x) = v )

proof end;

theorem Th19: :: MIDSP_3:19

for n being Nat

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS holds

( RAS is being_invariance iff for a, b being Point of RAS

for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )

for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

for W being ATLAS of RAS holds

( RAS is being_invariance iff for a, b being Point of RAS

for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )

proof end;

definition

let n be Nat;

ex b_{1} being non empty MidSp-like ReperAlgebraStr over n + 2 st b_{1} is being_invariance

end;
mode ReperAlgebra of n -> non empty MidSp-like ReperAlgebraStr over n + 2 means :Def11: :: MIDSP_3:def 11

it is being_invariance ;

existence it is being_invariance ;

ex b

proof end;

:: deftheorem Def11 defines ReperAlgebra MIDSP_3:def 11 :

for n being Nat

for b_{2} being non empty MidSp-like ReperAlgebraStr over n + 2 holds

( b_{2} is ReperAlgebra of n iff b_{2} is being_invariance );

for n being Nat

for b

( b

definition

let n be Nat;

let RAS be ReperAlgebra of n;

let W be ATLAS of RAS;

let x be Tuple of (n + 1),W;

ex b_{1} being Vector of W st

for a being Point of RAS holds b_{1} = Phi (a,x)

for b_{1}, b_{2} being Vector of W st ( for a being Point of RAS holds b_{1} = Phi (a,x) ) & ( for a being Point of RAS holds b_{2} = Phi (a,x) ) holds

b_{1} = b_{2}

end;
let RAS be ReperAlgebra of n;

let W be ATLAS of RAS;

let x be Tuple of (n + 1),W;

func Phi x -> Vector of W means :Def12: :: MIDSP_3:def 12

for a being Point of RAS holds it = Phi (a,x);

existence for a being Point of RAS holds it = Phi (a,x);

ex b

for a being Point of RAS holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines Phi MIDSP_3:def 12 :

for n being Nat

for RAS being ReperAlgebra of n

for W being ATLAS of RAS

for x being Tuple of (n + 1),W

for b_{5} being Vector of W holds

( b_{5} = Phi x iff for a being Point of RAS holds b_{5} = Phi (a,x) );

for n being Nat

for RAS being ReperAlgebra of n

for W being ATLAS of RAS

for x being Tuple of (n + 1),W

for b

( b

Lm4: for n being 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)))

proof end;

Lm5: for n being 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)))

proof end;

theorem Th23: :: MIDSP_3:23

for n being Nat

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

proof end;

theorem Th24: :: MIDSP_3:24

for n being Nat

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds

Phi x = v

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds

Phi x = v

proof end;

theorem Th25: :: MIDSP_3:25

for n being Nat

for m being Nat of n

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v holds

W . (a,(p +* (m,b))) = x +* (m,v)

for m being Nat of n

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v holds

W . (a,(p +* (m,b))) = x +* (m,v)

proof end;

theorem Th26: :: MIDSP_3:26

for n being Nat

for m being Nat of n

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

for m being Nat of n

for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b holds

(a,(x +* (m,v))) . W = p +* (m,b)

proof end;

theorem :: MIDSP_3:27

for n being Nat

for m being Nat of n

for RAS being ReperAlgebra of n

for W being ATLAS of RAS holds

( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W )

for m being Nat of n

for RAS being ReperAlgebra of n

for W being ATLAS of RAS holds

( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W )

proof end;

theorem Th28: :: MIDSP_3:28

for n being Nat

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) )

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) )

proof end;

theorem Th29: :: MIDSP_3:29

for n being Nat

for m being Nat of n

for RAS being ReperAlgebra of n st RAS has_property_of_zero_in m & RAS is_additive_in m holds

RAS is_semi_additive_in m

for m being Nat of n

for RAS being ReperAlgebra of n st RAS has_property_of_zero_in m & RAS is_additive_in m holds

RAS is_semi_additive_in m

proof end;

Lm6: for n being 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)))))) )

proof end;

Lm7: for n being 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

proof end;

theorem :: MIDSP_3:30

for n being 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))) )

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))) )

proof end;

theorem Th31: :: MIDSP_3:31

for n being Nat

for m being Nat of n

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 & m <= n holds

W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m))

for m being Nat of n

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 & m <= n holds

W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m))

proof end;

theorem Th32: :: MIDSP_3:32

for n being Nat

for m being Nat of n

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 & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

for m being Nat of n

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 & m <= n holds

(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))

proof end;

theorem :: MIDSP_3:33

for n being Nat

for m being Nat of n

for RAS being ReperAlgebra of n

for W being ATLAS of RAS st m <= n holds

( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

for m being Nat of n

for RAS being ReperAlgebra of n

for W being ATLAS of RAS st m <= n holds

( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

proof end;