:: MIDSP_1 semantic presentation

begin

definition
attrc1 is strict ;
struct MidStr  ->  1-sorted ;
aggrMidStr(# carrier, MIDPOINT #) ->  MidStr ;
sel MIDPOINT c1 ->  BinOp of the carrier of c1;
end;

registration
cluster non empty for MidStr ;
existence
 not for b1 being MidStr holds b1 is empty
proof
set A = the non empty set ;
set m = the BinOp of the non empty set ;
take  MidStr(# the non empty set , the BinOp of the non empty set #) ; ::_thesis: not MidStr(# the non empty set , the BinOp of the non empty set #) is empty
thus  not the carrier of MidStr(# the non empty set , the BinOp of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;


definition
let MS be non empty MidStr ;
let a, b be Element of MS;
funca @ b ->  Element of MS equals :: MIDSP_1:def 1
 the MIDPOINT of MS . (a,b);
coherence
 the MIDPOINT of MS . (a,b) is Element of MS ;
end;

:: deftheorem  defines @ MIDSP_1:def_1_:_
 for MS being non empty MidStr
for a, b being Element of MS holds a @ b = the MIDPOINT of MS . (a,b);

definition
func Example  ->  MidStr  equals :: MIDSP_1:def 2
 MidStr(# 1,op2 #);
correctness
coherence
MidStr(# 1,op2 #) is MidStr ;
;
end;

:: deftheorem  defines Example MIDSP_1:def_2_:_
 Example = MidStr(# 1,op2 #);

registration
cluster Example  ->  non empty strict ;
coherence
 ( Example is strict & not Example is empty ) ;
end;

theorem :: MIDSP_1:1
the carrier of Example = 1 ;

theorem :: MIDSP_1:2
the MIDPOINT of Example = op2 ;

theorem :: MIDSP_1:3
for a, b being Element of Example holds a @ b = op2 . (a,b) ;

theorem Th4: :: MIDSP_1:4
for a, b, c, d being Element of Example holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )
proof
let a, b, c, d be Element of Example; ::_thesis: ( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )
thus a @ a = {} by CARD_1:49, TARSKI:def_1
.= a by CARD_1:49, TARSKI:def_1 ; ::_thesis: ( a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )
thus a @ b = {} by CARD_1:49, TARSKI:def_1
.= b @ a by CARD_1:49, TARSKI:def_1 ; ::_thesis: ( (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )
thus (a @ b) @ (c @ d) = {} by CARD_1:49, TARSKI:def_1
.= (a @ c) @ (b @ d) by CARD_1:49, TARSKI:def_1 ; ::_thesis: ex x being Element of Example st x @ a = b
take x = a; ::_thesis: x @ a = b
thus x @ a = {} by CARD_1:49, TARSKI:def_1
.= b by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum
end;

definition
let IT be non empty MidStr ;
attrIT is MidSp-like  means :Def3: :: MIDSP_1:def 3
 for a, b, c, d being Element of IT holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of IT st x @ a = b );
end;

:: deftheorem Def3 defines MidSp-like MIDSP_1:def_3_:_
 for IT being non empty MidStr holds
( IT is MidSp-like iff for a, b, c, d being Element of IT holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of IT st x @ a = b ) );

registration
cluster non empty strict MidSp-like for MidStr ;
existence
 ex b1 being non empty MidStr st
( b1 is strict & b1 is MidSp-like )
proof
 Example is MidSp-like by Def3, Th4;
hence  ex b1 being non empty MidStr st
( b1 is strict & b1 is MidSp-like ) ; ::_thesis: verum
end;
end;

definition
mode MidSp is non empty MidSp-like MidStr ;
end;

definition
let M be MidSp;
let a, b be Element of M;
:: original: @
redefine funca @ b ->  Element of M;
commutativity
 for a, b being Element of M holds a @ b = b @ a by Def3;
end;


theorem Th5: :: MIDSP_1:5
for M being MidSp
for a, b, c being Element of M holds (a @ b) @ c = (a @ c) @ (b @ c)
proof
let M be MidSp; ::_thesis: for a, b, c being Element of M holds (a @ b) @ c = (a @ c) @ (b @ c)
let a, b, c be Element of M; ::_thesis: (a @ b) @ c = (a @ c) @ (b @ c)
(a @ b) @ c = (a @ b) @ (c @ c) by Def3
.= (a @ c) @ (b @ c) by Def3 ;
hence  (a @ b) @ c = (a @ c) @ (b @ c) ; ::_thesis: verum
end;

theorem Th6: :: MIDSP_1:6
for M being MidSp
for a, b, c being Element of M holds a @ (b @ c) = (a @ b) @ (a @ c)
proof
let M be MidSp; ::_thesis: for a, b, c being Element of M holds a @ (b @ c) = (a @ b) @ (a @ c)
let a, b, c be Element of M; ::_thesis: a @ (b @ c) = (a @ b) @ (a @ c)
a @ (b @ c) = (a @ a) @ (b @ c) by Def3
.= (a @ b) @ (a @ c) by Def3 ;
hence  a @ (b @ c) = (a @ b) @ (a @ c) ; ::_thesis: verum
end;

theorem Th7: :: MIDSP_1:7
for M being MidSp
for a, b being Element of M st a @ b = a holds
a = b
proof
let M be MidSp; ::_thesis: for a, b being Element of M st a @ b = a holds
a = b
let a, b be Element of M; ::_thesis: ( a @ b = a implies a = b )
assume A1: a @ b = a ; ::_thesis: a = b
consider x being Element of M such that
A2: x @ a = b by Def3;
b = (x @ a) @ b by A2, Def3
.= (x @ b) @ a by A1, Th5
.= a by A1, A2, Th5 ;
hence  a = b ; ::_thesis: verum
end;

theorem Th8: :: MIDSP_1:8
for M being MidSp
for x, a, x9 being Element of M st x @ a = x9 @ a holds
x = x9
proof
let M be MidSp; ::_thesis: for x, a, x9 being Element of M st x @ a = x9 @ a holds
x = x9
let x, a, x9 be Element of M; ::_thesis: ( x @ a = x9 @ a implies x = x9 )
assume A1: x @ a = x9 @ a ; ::_thesis: x = x9
consider y being Element of M such that
A2: y @ a = x by Def3;
x = x @ (y @ a) by A2, Def3
.= (x @ y) @ (x9 @ a) by A1, Th6
.= x @ (x @ x9) by A2, Def3 ;
then  x = x @ x9 by Th7;
hence  x = x9 by Th7; ::_thesis: verum
end;

theorem :: MIDSP_1:9
for M being MidSp
for a, x, x9 being Element of M st a @ x = a @ x9 holds
x = x9 by Th8;

definition
let M be MidSp;
let a, b, c, d be Element of M;
preda,b @@ c,d means :Def4: :: MIDSP_1:def 4
a @ d = b @ c;
end;

:: deftheorem Def4 defines @@ MIDSP_1:def_4_:_
 for M being MidSp
for a, b, c, d being Element of M holds
( a,b @@ c,d iff a @ d = b @ c );

theorem Th10: :: MIDSP_1:10
for M being MidSp
for a, b being Element of M holds a,a @@ b,b
proof
let M be MidSp; ::_thesis: for a, b being Element of M holds a,a @@ b,b
let a, b be Element of M; ::_thesis: a,a @@ b,b
thus  a @ b = a @ b ; :: according to MIDSP_1:def_4 ::_thesis: verum
end;

theorem Th11: :: MIDSP_1:11
for M being MidSp
for a, b, c, d being Element of M st a,b @@ c,d holds
c,d @@ a,b
proof
let M be MidSp; ::_thesis: for a, b, c, d being Element of M st a,b @@ c,d holds
c,d @@ a,b
let a, b, c, d be Element of M; ::_thesis: ( a,b @@ c,d implies c,d @@ a,b )
assume  a @ d = b @ c ; :: according to MIDSP_1:def_4 ::_thesis: c,d @@ a,b
hence  c @ b = d @ a ; :: according to MIDSP_1:def_4 ::_thesis: verum
end;

theorem Th12: :: MIDSP_1:12
for M being MidSp
for a, b, c being Element of M st a,a @@ b,c holds
b = c
proof
let M be MidSp; ::_thesis: for a, b, c being Element of M st a,a @@ b,c holds
b = c
let a, b, c be Element of M; ::_thesis: ( a,a @@ b,c implies b = c )
assume  a,a @@ b,c ; ::_thesis: b = c
then  a @ c = a @ b by Def4;
hence  b = c by Th8; ::_thesis: verum
end;

theorem Th13: :: MIDSP_1:13
for M being MidSp
for a, b, c being Element of M st a,b @@ c,c holds
a = b by Th11, Th12;

theorem Th14: :: MIDSP_1:14
for M being MidSp
for a, b being Element of M holds a,b @@ a,b
proof
let M be MidSp; ::_thesis: for a, b being Element of M holds a,b @@ a,b
let a, b be Element of M; ::_thesis: a,b @@ a,b
thus  a @ b = b @ a ; :: according to MIDSP_1:def_4 ::_thesis: verum
end;

theorem Th15: :: MIDSP_1:15
for M being MidSp
for a, b, c being Element of M ex d being Element of M st a,b @@ c,d
proof
let M be MidSp; ::_thesis: for a, b, c being Element of M ex d being Element of M st a,b @@ c,d
let a, b, c be Element of M; ::_thesis: ex d being Element of M st a,b @@ c,d
consider d being Element of M such that
A1: d @ a = b @ c by Def3;
 a,b @@ c,d by A1, Def4;
hence  ex d being Element of M st a,b @@ c,d ; ::_thesis: verum
end;

theorem Th16: :: MIDSP_1:16
for M being MidSp
for a, b, c, d, d9 being Element of M st a,b @@ c,d & a,b @@ c,d9 holds
d = d9
proof
let M be MidSp; ::_thesis: for a, b, c, d, d9 being Element of M st a,b @@ c,d & a,b @@ c,d9 holds
d = d9
let a, b, c, d, d9 be Element of M; ::_thesis: ( a,b @@ c,d & a,b @@ c,d9 implies d = d9 )
assume A1: a,b @@ c,d ; ::_thesis: ( not a,b @@ c,d9 or d = d9 )
assume A2: a,b @@ c,d9 ; ::_thesis: d = d9
a @ d = b @ c by A1, Def4
.= a @ d9 by A2, Def4 ;
hence  d = d9 by Th8; ::_thesis: verum
end;

theorem Th17: :: MIDSP_1:17
for M being MidSp
for x, y, a, b, c, d being Element of M st x,y @@ a,b & x,y @@ c,d holds
a,b @@ c,d
proof
let M be MidSp; ::_thesis: for x, y, a, b, c, d being Element of M st x,y @@ a,b & x,y @@ c,d holds
a,b @@ c,d
let x, y, a, b, c, d be Element of M; ::_thesis: ( x,y @@ a,b & x,y @@ c,d implies a,b @@ c,d )
assume A1: x,y @@ a,b ; ::_thesis: ( not x,y @@ c,d or a,b @@ c,d )
assume A2: x,y @@ c,d ; ::_thesis: a,b @@ c,d
(y @ x) @ (a @ d) = (y @ a) @ (x @ d) by Def3
.= (x @ b) @ (x @ d) by A1, Def4
.= (x @ b) @ (y @ c) by A2, Def4
.= (y @ x) @ (b @ c) by Def3 ;
hence  a @ d = b @ c by Th8; :: according to MIDSP_1:def_4 ::_thesis: verum
end;

theorem Th18: :: MIDSP_1:18
for M being MidSp
for a, b, a9, b9, c, c9 being Element of M st a,b @@ a9,b9 & b,c @@ b9,c9 holds
a,c @@ a9,c9
proof
let M be MidSp; ::_thesis: for a, b, a9, b9, c, c9 being Element of M st a,b @@ a9,b9 & b,c @@ b9,c9 holds
a,c @@ a9,c9
let a, b, a9, b9, c, c9 be Element of M; ::_thesis: ( a,b @@ a9,b9 & b,c @@ b9,c9 implies a,c @@ a9,c9 )
assume A1: a,b @@ a9,b9 ; ::_thesis: ( not b,c @@ b9,c9 or a,c @@ a9,c9 )
assume A2: b,c @@ b9,c9 ; ::_thesis: a,c @@ a9,c9
(b9 @ b) @ (a @ c9) = (a @ b9) @ (b @ c9) by Def3
.= (b @ a9) @ (b @ c9) by A1, Def4
.= (c @ b9) @ (b @ a9) by A2, Def4
.= (b9 @ b) @ (c @ a9) by Def3 ;
hence  a @ c9 = c @ a9 by Th8; :: according to MIDSP_1:def_4 ::_thesis: verum
end;


definition
let M be MidSp;
let p, q be Element of [: the carrier of M, the carrier of M:];
predp ## q means :Def5: :: MIDSP_1:def 5
p `1 ,p `2 @@ q `1 ,q `2 ;
reflexivity
 for p being Element of [: the carrier of M, the carrier of M:] holds p `1 ,p `2 @@ p `1 ,p `2 by Th14;
symmetry
 for p, q being Element of [: the carrier of M, the carrier of M:] st p `1 ,p `2 @@ q `1 ,q `2 holds
q `1 ,q `2 @@ p `1 ,p `2 by Th11;
end;

:: deftheorem Def5 defines ## MIDSP_1:def_5_:_
 for M being MidSp
for p, q being Element of [: the carrier of M, the carrier of M:] holds
( p ## q iff p `1 ,p `2 @@ q `1 ,q `2 );

theorem Th19: :: MIDSP_1:19
for M being MidSp
for a, b, c, d being Element of M st a,b @@ c,d holds
[a,b] ## [c,d]
proof
let M be MidSp; ::_thesis: for a, b, c, d being Element of M st a,b @@ c,d holds
[a,b] ## [c,d]
let a, b, c, d be Element of M; ::_thesis: ( a,b @@ c,d implies [a,b] ## [c,d] )
set p = [a,b];
set q = [c,d];
A1: ( [a,b] `1 = a & [a,b] `2 = b ) by MCART_1:7;
A2: ( [c,d] `1 = c & [c,d] `2 = d ) by MCART_1:7;
assume  a,b @@ c,d ; ::_thesis: [a,b] ## [c,d]
hence  [a,b] ## [c,d] by A1, A2, Def5; ::_thesis: verum
end;

theorem Th20: :: MIDSP_1:20
for M being MidSp
for a, b, c, d being Element of M st [a,b] ## [c,d] holds
a,b @@ c,d
proof
let M be MidSp; ::_thesis: for a, b, c, d being Element of M st [a,b] ## [c,d] holds
a,b @@ c,d
let a, b, c, d be Element of M; ::_thesis: ( [a,b] ## [c,d] implies a,b @@ c,d )
set p = [a,b];
set q = [c,d];
A1: ( [a,b] `1 = a & [a,b] `2 = b ) by MCART_1:7;
A2: ( [c,d] `1 = c & [c,d] `2 = d ) by MCART_1:7;
assume  [a,b] ## [c,d] ; ::_thesis: a,b @@ c,d
hence  a,b @@ c,d by A1, A2, Def5; ::_thesis: verum
end;

theorem Th21: :: MIDSP_1:21
for M being MidSp
for p, q, r being Element of [: the carrier of M, the carrier of M:] st p ## q & p ## r holds
q ## r
proof
let M be MidSp; ::_thesis: for p, q, r being Element of [: the carrier of M, the carrier of M:] st p ## q & p ## r holds
q ## r
let p, q, r be Element of [: the carrier of M, the carrier of M:]; ::_thesis: ( p ## q & p ## r implies q ## r )
assume  ( p ## q & p ## r ) ; ::_thesis: q ## r
then  ( p `1 ,p `2 @@ q `1 ,q `2 & p `1 ,p `2 @@ r `1 ,r `2 ) by Def5;
hence  q `1 ,q `2 @@ r `1 ,r `2 by Th17; :: according to MIDSP_1:def_5 ::_thesis: verum
end;

theorem :: MIDSP_1:22
for M being MidSp
for p, r, q being Element of [: the carrier of M, the carrier of M:] st p ## r & q ## r holds
p ## q by Th21;

theorem :: MIDSP_1:23
for M being MidSp
for p, q, r being Element of [: the carrier of M, the carrier of M:] st p ## q & q ## r holds
p ## r by Th21;

theorem :: MIDSP_1:24
for M being MidSp
for p, q, r being Element of [: the carrier of M, the carrier of M:] st p ## q holds
( r ## p iff r ## q ) by Th21;

theorem Th25: :: MIDSP_1:25
for M being MidSp
for p being Element of [: the carrier of M, the carrier of M:] holds  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  is non empty Subset of [: the carrier of M, the carrier of M:]
proof
let M be MidSp; ::_thesis: for p being Element of [: the carrier of M, the carrier of M:] holds  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  is non empty Subset of [: the carrier of M, the carrier of M:]
let p be Element of [: the carrier of M, the carrier of M:]; ::_thesis:  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  is non empty Subset of [: the carrier of M, the carrier of M:]
set pp =  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  ;
A1: for x being set st x in  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  holds
x in [: the carrier of M, the carrier of M:]
proof
let x be set ; ::_thesis: ( x in  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  implies x in [: the carrier of M, the carrier of M:] )
assume  x in  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  ; ::_thesis: x in [: the carrier of M, the carrier of M:]
then  ex q being Element of [: the carrier of M, the carrier of M:] st
( x = q & q ## p ) ;
hence  x in [: the carrier of M, the carrier of M:] ; ::_thesis: verum
end;
 p in  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  ;
hence   {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  is non empty Subset of [: the carrier of M, the carrier of M:] by A1, TARSKI:def_3; ::_thesis: verum
end;

definition
let M be MidSp;
let p be Element of [: the carrier of M, the carrier of M:];
funcp ~  ->  Subset of [: the carrier of M, the carrier of M:] equals :: MIDSP_1:def 6
 {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  ;
coherence
  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  is Subset of [: the carrier of M, the carrier of M:] by Th25;
end;

:: deftheorem  defines ~ MIDSP_1:def_6_:_
 for M being MidSp
for p being Element of [: the carrier of M, the carrier of M:] holds p ~ =  {  q where q is Element of [: the carrier of M, the carrier of M:] : q ## p  }  ;

registration
let M be MidSp;
let p be Element of [: the carrier of M, the carrier of M:];
clusterp ~  ->  non empty ;
coherence
 not p ~ is empty by Th25;
end;

theorem Th26: :: MIDSP_1:26
for M being MidSp
for r, p being Element of [: the carrier of M, the carrier of M:] holds
( r in p ~ iff r ## p )
proof
let M be MidSp; ::_thesis: for r, p being Element of [: the carrier of M, the carrier of M:] holds
( r in p ~ iff r ## p )
let r, p be Element of [: the carrier of M, the carrier of M:]; ::_thesis: ( r in p ~ iff r ## p )
thus  ( r in p ~ implies r ## p ) ::_thesis: ( r ## p implies r in p ~ )
proof
assume  r in p ~ ; ::_thesis: r ## p
then  ex q being Element of [: the carrier of M, the carrier of M:] st
( r = q & q ## p ) ;
hence  r ## p ; ::_thesis: verum
end;
thus  ( r ## p implies r in p ~ ) ; ::_thesis: verum
end;

theorem Th27: :: MIDSP_1:27
for M being MidSp
for p, q being Element of [: the carrier of M, the carrier of M:] st p ## q holds
p ~ = q ~
proof
let M be MidSp; ::_thesis: for p, q being Element of [: the carrier of M, the carrier of M:] st p ## q holds
p ~ = q ~
let p, q be Element of [: the carrier of M, the carrier of M:]; ::_thesis: ( p ## q implies p ~ = q ~ )
assume A1: p ## q ; ::_thesis: p ~ = q ~
 for x being set holds
( x in p ~ iff x in q ~ )
proof
let x be set ; ::_thesis: ( x in p ~ iff x in q ~ )
thus  ( x in p ~ implies x in q ~ ) ::_thesis: ( x in q ~ implies x in p ~ )
proof
assume A2: x in p ~ ; ::_thesis: x in q ~
then reconsider r = x as Element of [: the carrier of M, the carrier of M:] ;
 r ## p by A2, Th26;
then  r ## q by A1, Th21;
hence  x in q ~ ; ::_thesis: verum
end;
thus  ( x in q ~ implies x in p ~ ) ::_thesis: verum
proof
assume A3: x in q ~ ; ::_thesis: x in p ~
then reconsider r = x as Element of [: the carrier of M, the carrier of M:] ;
 r ## q by A3, Th26;
then  r ## p by A1, Th21;
hence  x in p ~ ; ::_thesis: verum
end;
end;
hence  p ~ = q ~ by TARSKI:1; ::_thesis: verum
end;

theorem Th28: :: MIDSP_1:28
for M being MidSp
for p, q being Element of [: the carrier of M, the carrier of M:] st p ~ = q ~ holds
p ## q
proof
let M be MidSp; ::_thesis: for p, q being Element of [: the carrier of M, the carrier of M:] st p ~ = q ~ holds
p ## q
let p, q be Element of [: the carrier of M, the carrier of M:]; ::_thesis: ( p ~ = q ~ implies p ## q )
 p in p ~ ;
hence  ( p ~ = q ~ implies p ## q ) by Th26; ::_thesis: verum
end;

theorem Th29: :: MIDSP_1:29
for M being MidSp
for a, b, c, d being Element of M st [a,b] ~ = [c,d] ~ holds
a @ d = b @ c
proof
let M be MidSp; ::_thesis: for a, b, c, d being Element of M st [a,b] ~ = [c,d] ~ holds
a @ d = b @ c
let a, b, c, d be Element of M; ::_thesis: ( [a,b] ~ = [c,d] ~ implies a @ d = b @ c )
assume  [a,b] ~ = [c,d] ~ ; ::_thesis: a @ d = b @ c
then  a,b @@ c,d by Th20, Th28;
hence  a @ d = b @ c by Def4; ::_thesis: verum
end;

theorem :: MIDSP_1:30
for M being MidSp
for p being Element of [: the carrier of M, the carrier of M:] holds p in p ~ ;

definition
let M be MidSp;
mode Vector of M ->  non empty Subset of [: the carrier of M, the carrier of M:] means :Def7: :: MIDSP_1:def 7
 ex p being Element of [: the carrier of M, the carrier of M:] st it = p ~ ;
existence
 ex b1 being non empty Subset of [: the carrier of M, the carrier of M:] ex p being Element of [: the carrier of M, the carrier of M:] st b1 = p ~
proof
set p = the Element of [: the carrier of M, the carrier of M:];
take  the Element of [: the carrier of M, the carrier of M:] ~ ; ::_thesis: ex p being Element of [: the carrier of M, the carrier of M:] st the Element of [: the carrier of M, the carrier of M:] ~ = p ~
thus  ex p being Element of [: the carrier of M, the carrier of M:] st the Element of [: the carrier of M, the carrier of M:] ~ = p ~ ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Vector MIDSP_1:def_7_:_
 for M being MidSp
for b2 being non empty Subset of [: the carrier of M, the carrier of M:] holds
( b2 is Vector of M iff ex p being Element of [: the carrier of M, the carrier of M:] st b2 = p ~ );


definition
let M be MidSp;
let p be Element of [: the carrier of M, the carrier of M:];
:: original: ~
redefine funcp ~  ->  Vector of M;
coherence
 p ~ is Vector of M by Def7;
end;

theorem Th31: :: MIDSP_1:31
for M being MidSp ex u being Vector of M st
for p being Element of [: the carrier of M, the carrier of M:] holds
( p in u iff p `1 = p `2 )
proof
let M be MidSp; ::_thesis: ex u being Vector of M st
for p being Element of [: the carrier of M, the carrier of M:] holds
( p in u iff p `1 = p `2 )
set a = the Element of M;
take  [ the Element of M, the Element of M] ~ ; ::_thesis: for p being Element of [: the carrier of M, the carrier of M:] holds
( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 )
let p be Element of [: the carrier of M, the carrier of M:]; ::_thesis: ( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 )
 ( [ the Element of M, the Element of M] `1 = the Element of M & [ the Element of M, the Element of M] `2 = the Element of M ) by MCART_1:7;
then  ( p `1 ,p `2 @@ the Element of M, the Element of M iff p ## [ the Element of M, the Element of M] ) by Def5;
hence  ( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 ) by Th10, Th13, Th26; ::_thesis: verum
end;

definition
let M be MidSp;
func ID M ->  Vector of M equals :: MIDSP_1:def 8
 {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  ;
coherence
  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  is Vector of M
proof
consider u being Vector of M such that
A1: for p being Element of [: the carrier of M, the carrier of M:] holds
( p in u iff p `1 = p `2 ) by Th31;
 u =  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }
proof
 for x being set holds
( x in u iff x in  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  )
proof
let x be set ; ::_thesis: ( x in u iff x in  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  )
thus  ( x in u implies x in  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  ) ::_thesis: ( x in  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  implies x in u )
proof
assume A2: x in u ; ::_thesis: x in  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }
then reconsider r = x as Element of [: the carrier of M, the carrier of M:] ;
 r `1 = r `2 by A1, A2;
hence  x in  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  ; ::_thesis: verum
end;
thus  ( x in  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  implies x in u ) ::_thesis: verum
proof
assume  x in  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  ; ::_thesis: x in u
then  ex p being Element of [: the carrier of M, the carrier of M:] st
( x = p & p `1 = p `2 ) ;
hence  x in u by A1; ::_thesis: verum
end;
end;
hence  u =  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  by TARSKI:1; ::_thesis: verum
end;
hence   {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  is Vector of M ; ::_thesis: verum
end;
end;

:: deftheorem  defines ID MIDSP_1:def_8_:_
 for M being MidSp holds ID M =  {  p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2  }  ;

theorem Th32: :: MIDSP_1:32
for M being MidSp
for b being Element of M holds ID M = [b,b] ~
proof
let M be MidSp; ::_thesis: for b being Element of M holds ID M = [b,b] ~
let b be Element of M; ::_thesis: ID M = [b,b] ~
 for p being Element of [: the carrier of M, the carrier of M:] holds
( p in ID M iff p in [b,b] ~ )
proof
let p be Element of [: the carrier of M, the carrier of M:]; ::_thesis: ( p in ID M iff p in [b,b] ~ )
thus  ( p in ID M implies p in [b,b] ~ ) ::_thesis: ( p in [b,b] ~ implies p in ID M )
proof
assume  p in ID M ; ::_thesis: p in [b,b] ~
then  ex q being Element of [: the carrier of M, the carrier of M:] st
( p = q & q `1 = q `2 ) ;
then A1: p `1 ,p `2 @@ b,b by Th10;
 ( [b,b] `1 = b & [b,b] `2 = b ) by MCART_1:7;
then  p ## [b,b] by A1, Def5;
hence  p in [b,b] ~ ; ::_thesis: verum
end;
thus  ( p in [b,b] ~ implies p in ID M ) ::_thesis: verum
proof
assume  p in [b,b] ~ ; ::_thesis: p in ID M
then A2: p ## [b,b] by Th26;
 ( [b,b] `1 = b & [b,b] `2 = b ) by MCART_1:7;
then  p `1 ,p `2 @@ b,b by A2, Def5;
then  p `1 = p `2 by Th11, Th12;
hence  p in ID M ; ::_thesis: verum
end;
end;
then  for p being set holds
( p in ID M iff p in [b,b] ~ ) ;
hence  ID M = [b,b] ~ by TARSKI:1; ::_thesis: verum
end;

theorem Th33: :: MIDSP_1:33
for M being MidSp
for u, v, w, w9 being Vector of M st ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w = [(p `1),(q `2)] ~ ) & ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w9 = [(p `1),(q `2)] ~ ) holds
w = w9
proof
let M be MidSp; ::_thesis: for u, v, w, w9 being Vector of M st ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w = [(p `1),(q `2)] ~ ) & ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w9 = [(p `1),(q `2)] ~ ) holds
w = w9
let u, v, w, w9 be Vector of M; ::_thesis: ( ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w = [(p `1),(q `2)] ~ ) & ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w9 = [(p `1),(q `2)] ~ ) implies w = w9 )
given p, q being Element of [: the carrier of M, the carrier of M:] such that A1: u = p ~ and
A2: v = q ~ and
A3: p `2 = q `1 and
A4: w = [(p `1),(q `2)] ~ ; ::_thesis: ( for p, q being Element of [: the carrier of M, the carrier of M:] holds
( not u = p ~ or not v = q ~ or not p `2 = q `1 or not w9 = [(p `1),(q `2)] ~ ) or w = w9 )
given p9, q9 being Element of [: the carrier of M, the carrier of M:] such that A5: u = p9 ~ and
A6: v = q9 ~ and
A7: p9 `2 = q9 `1 and
A8: w9 = [(p9 `1),(q9 `2)] ~ ; ::_thesis: w = w9
 q ## q9 by A2, A6, Th28;
then A9: q `1 ,q `2 @@ q9 `1 ,q9 `2 by Def5;
 p ## p9 by A1, A5, Th28;
then  p `1 ,p `2 @@ p9 `1 ,p9 `2 by Def5;
then  p `1 ,q `2 @@ p9 `1 ,q9 `2 by A3, A7, A9, Th18;
hence  w = w9 by A4, A8, Th19, Th27; ::_thesis: verum
end;

definition
let M be MidSp;
let u, v be Vector of M;
funcu + v ->  Vector of M means :Def9: :: MIDSP_1:def 9
 ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & it = [(p `1),(q `2)] ~ );
existence
 ex b1 being Vector of M ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b1 = [(p `1),(q `2)] ~ )
proof
consider p being Element of [: the carrier of M, the carrier of M:] such that
A1: u = p ~ by Def7;
consider q being Element of [: the carrier of M, the carrier of M:] such that
A2: v = q ~ by Def7;
consider d being Element of M such that
A3: q `1 ,q `2 @@ p `2 ,d by Th15;
take  [(p `1),d] ~ ; ::_thesis: ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & [(p `1),d] ~ = [(p `1),(q `2)] ~ )
take p9 = p; ::_thesis: ex q being Element of [: the carrier of M, the carrier of M:] st
( u = p9 ~ & v = q ~ & p9 `2 = q `1 & [(p `1),d] ~ = [(p9 `1),(q `2)] ~ )
take q9 = [(p `2),d]; ::_thesis: ( u = p9 ~ & v = q9 ~ & p9 `2 = q9 `1 & [(p `1),d] ~ = [(p9 `1),(q9 `2)] ~ )
thus  u = p9 ~ by A1; ::_thesis: ( v = q9 ~ & p9 `2 = q9 `1 & [(p `1),d] ~ = [(p9 `1),(q9 `2)] ~ )
 ( q9 `1 = p `2 & q9 `2 = d ) by MCART_1:7;
then  q ## q9 by A3, Def5;
hence  v = q9 ~ by A2, Th27; ::_thesis: ( p9 `2 = q9 `1 & [(p `1),d] ~ = [(p9 `1),(q9 `2)] ~ )
thus  p9 `2 = q9 `1 by MCART_1:7; ::_thesis: [(p `1),d] ~ = [(p9 `1),(q9 `2)] ~
thus  [(p `1),d] ~ = [(p9 `1),(q9 `2)] ~ by MCART_1:7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Vector of M st ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b1 = [(p `1),(q `2)] ~ ) & ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b2 = [(p `1),(q `2)] ~ ) holds
b1 = b2 by Th33;
end;

:: deftheorem Def9 defines + MIDSP_1:def_9_:_
 for M being MidSp
for u, v, b4 being Vector of M holds
( b4 = u + v iff ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b4 = [(p `1),(q `2)] ~ ) );

theorem Th34: :: MIDSP_1:34
for M being MidSp
for a being Element of M
for u being Vector of M ex b being Element of M st u = [a,b] ~
proof
let M be MidSp; ::_thesis: for a being Element of M
for u being Vector of M ex b being Element of M st u = [a,b] ~
let a be Element of M; ::_thesis: for u being Vector of M ex b being Element of M st u = [a,b] ~
let u be Vector of M; ::_thesis: ex b being Element of M st u = [a,b] ~
consider p being Element of [: the carrier of M, the carrier of M:] such that
A1: u = p ~ by Def7;
consider b being Element of M such that
A2: p `1 ,p `2 @@ a,b by Th15;
 [(p `1),(p `2)] ## [a,b] by A2, Th19;
then  p ## [a,b] by MCART_1:21;
then  p ~ = [a,b] ~ by Th27;
hence  ex b being Element of M st u = [a,b] ~ by A1; ::_thesis: verum
end;

definition
let M be MidSp;
let a, b be Element of M;
func vect (a,b) ->  Vector of M equals :: MIDSP_1:def 10
[a,b] ~ ;
coherence
 [a,b] ~ is Vector of M ;
end;

:: deftheorem  defines vect MIDSP_1:def_10_:_
 for M being MidSp
for a, b being Element of M holds vect (a,b) = [a,b] ~ ;

theorem Th35: :: MIDSP_1:35
for M being MidSp
for a being Element of M
for u being Vector of M ex b being Element of M st u = vect (a,b)
proof
let M be MidSp; ::_thesis: for a being Element of M
for u being Vector of M ex b being Element of M st u = vect (a,b)
let a be Element of M; ::_thesis: for u being Vector of M ex b being Element of M st u = vect (a,b)
let u be Vector of M; ::_thesis: ex b being Element of M st u = vect (a,b)
consider b being Element of M such that
A1: u = [a,b] ~ by Th34;
 u = vect (a,b) by A1;
hence  ex b being Element of M st u = vect (a,b) ; ::_thesis: verum
end;

theorem :: MIDSP_1:36
for M being MidSp
for a, b, c, d being Element of M st [a,b] ## [c,d] holds
vect (a,b) = vect (c,d) by Th27;

theorem :: MIDSP_1:37
for M being MidSp
for a, b, c, d being Element of M st vect (a,b) = vect (c,d) holds
a @ d = b @ c by Th29;

theorem :: MIDSP_1:38
for M being MidSp
for b being Element of M holds ID M = vect (b,b) by Th32;

theorem :: MIDSP_1:39
for M being MidSp
for a, b, c being Element of M st vect (a,b) = vect (a,c) holds
b = c
proof
let M be MidSp; ::_thesis: for a, b, c being Element of M st vect (a,b) = vect (a,c) holds
b = c
let a, b, c be Element of M; ::_thesis: ( vect (a,b) = vect (a,c) implies b = c )
assume  vect (a,b) = vect (a,c) ; ::_thesis: b = c
then  ( a,b @@ a,b & a,b @@ a,c ) by Th20, Th28;
hence  b = c by Th16; ::_thesis: verum
end;

theorem Th40: :: MIDSP_1:40
for M being MidSp
for a, b, c being Element of M holds (vect (a,b)) + (vect (b,c)) = vect (a,c)
proof
let M be MidSp; ::_thesis: for a, b, c being Element of M holds (vect (a,b)) + (vect (b,c)) = vect (a,c)
let a, b, c be Element of M; ::_thesis: (vect (a,b)) + (vect (b,c)) = vect (a,c)
set p = [a,b];
set q = [b,c];
set u = [a,b] ~ ;
set v = [b,c] ~ ;
[a,b] `2 = b by MCART_1:7
.= [b,c] `1 by MCART_1:7 ;
then  ( [b,c] `2 = c & ([a,b] ~) + ([b,c] ~) = [([a,b] `1),([b,c] `2)] ~ ) by Def9, MCART_1:7;
hence  (vect (a,b)) + (vect (b,c)) = vect (a,c) by MCART_1:7; ::_thesis: verum
end;

theorem Th41: :: MIDSP_1:41
for M being MidSp
for a, b being Element of M holds [a,(a @ b)] ## [(a @ b),b]
proof
let M be MidSp; ::_thesis: for a, b being Element of M holds [a,(a @ b)] ## [(a @ b),b]
let a, b be Element of M; ::_thesis: [a,(a @ b)] ## [(a @ b),b]
 a @ b = (a @ b) @ (a @ b) by Def3;
then  a,a @ b @@ a @ b,b by Def4;
hence  [a,(a @ b)] ## [(a @ b),b] by Th19; ::_thesis: verum
end;

theorem :: MIDSP_1:42
for M being MidSp
for a, b being Element of M holds (vect (a,(a @ b))) + (vect (a,(a @ b))) = vect (a,b)
proof
let M be MidSp; ::_thesis: for a, b being Element of M holds (vect (a,(a @ b))) + (vect (a,(a @ b))) = vect (a,b)
let a, b be Element of M; ::_thesis: (vect (a,(a @ b))) + (vect (a,(a @ b))) = vect (a,b)
(vect (a,(a @ b))) + (vect (a,(a @ b))) = (vect (a,(a @ b))) + (vect ((a @ b),b)) by Th27, Th41
.= vect (a,b) by Th40 ;
hence  (vect (a,(a @ b))) + (vect (a,(a @ b))) = vect (a,b) ; ::_thesis: verum
end;

theorem Th43: :: MIDSP_1:43
for M being MidSp
for u, v, w being Vector of M holds (u + v) + w = u + (v + w)
proof
let M be MidSp; ::_thesis: for u, v, w being Vector of M holds (u + v) + w = u + (v + w)
let u, v, w be Vector of M; ::_thesis: (u + v) + w = u + (v + w)
set a = the Element of M;
consider b being Element of M such that
A1: u = vect ( the Element of M,b) by Th35;
consider c being Element of M such that
A2: v = vect (b,c) by Th35;
consider d being Element of M such that
A3: w = vect (c,d) by Th35;
(u + v) + w = (vect ( the Element of M,c)) + w by A1, A2, Th40
.= vect ( the Element of M,d) by A3, Th40
.= (vect ( the Element of M,b)) + (vect (b,d)) by Th40
.= u + (v + w) by A1, A2, A3, Th40 ;
hence  (u + v) + w = u + (v + w) ; ::_thesis: verum
end;

theorem Th44: :: MIDSP_1:44
for M being MidSp
for u being Vector of M holds u + (ID M) = u
proof
let M be MidSp; ::_thesis: for u being Vector of M holds u + (ID M) = u
let u be Vector of M; ::_thesis: u + (ID M) = u
set a = the Element of M;
consider b being Element of M such that
A1: u = vect ( the Element of M,b) by Th35;
u + (ID M) = (vect ( the Element of M,b)) + (vect (b,b)) by A1, Th32
.= u by A1, Th40 ;
hence  u + (ID M) = u ; ::_thesis: verum
end;

theorem Th45: :: MIDSP_1:45
for M being MidSp
for u being Vector of M ex v being Vector of M st u + v = ID M
proof
let M be MidSp; ::_thesis: for u being Vector of M ex v being Vector of M st u + v = ID M
let u be Vector of M; ::_thesis: ex v being Vector of M st u + v = ID M
set a = the Element of M;
consider b being Element of M such that
A1: u = vect ( the Element of M,b) by Th35;
u + (vect (b, the Element of M)) = vect ( the Element of M, the Element of M) by A1, Th40
.= ID M by Th32 ;
hence  ex v being Vector of M st u + v = ID M ; ::_thesis: verum
end;

theorem Th46: :: MIDSP_1:46
for M being MidSp
for u, v being Vector of M holds u + v = v + u
proof
let M be MidSp; ::_thesis: for u, v being Vector of M holds u + v = v + u
let u, v be Vector of M; ::_thesis: u + v = v + u
set a = the Element of M;
consider b being Element of M such that
A1: u = vect ( the Element of M,b) by Th35;
consider c being Element of M such that
A2: v = vect (b,c) by Th35;
consider d being Element of M such that
A3: v = vect ( the Element of M,d) by Th35;
consider c9 being Element of M such that
A4: u = vect (d,c9) by Th35;
A5: the Element of M @ c9 = b @ d by A1, A4, Th29
.= the Element of M @ c by A2, A3, Th29 ;
u + v = vect ( the Element of M,c) by A1, A2, Th40
.= vect ( the Element of M,c9) by A5, Th8
.= v + u by A3, A4, Th40 ;
hence  u + v = v + u ; ::_thesis: verum
end;

theorem Th47: :: MIDSP_1:47
for M being MidSp
for u, v, w being Vector of M st u + v = u + w holds
v = w
proof
let M be MidSp; ::_thesis: for u, v, w being Vector of M st u + v = u + w holds
v = w
let u, v, w be Vector of M; ::_thesis: ( u + v = u + w implies v = w )
assume A1: u + v = u + w ; ::_thesis: v = w
consider u9 being Vector of M such that
A2: u + u9 = ID M by Th45;
v = v + (ID M) by Th44
.= (u + u9) + v by A2, Th46
.= (u9 + u) + v by Th46
.= u9 + (u + w) by A1, Th43
.= (u9 + u) + w by Th43
.= (ID M) + w by A2, Th46
.= w + (ID M) by Th46 ;
hence  v = w by Th44; ::_thesis: verum
end;

definition
let M be MidSp;
let u be Vector of M;
func - u ->  Vector of M means :: MIDSP_1:def 11
u + it = ID M;
existence
 ex b1 being Vector of M st u + b1 = ID M by Th45;
uniqueness
 for b1, b2 being Vector of M st u + b1 = ID M & u + b2 = ID M holds
b1 = b2 by Th47;
end;

:: deftheorem  defines - MIDSP_1:def_11_:_
 for M being MidSp
for u, b3 being Vector of M holds
( b3 = - u iff u + b3 = ID M );

definition
let M be MidSp;
func setvect M ->  set  equals :: MIDSP_1:def 12
 {  X where X is Subset of [: the carrier of M, the carrier of M:] : X is Vector of M  }  ;
coherence
  {  X where X is Subset of [: the carrier of M, the carrier of M:] : X is Vector of M  }  is set ;
end;

:: deftheorem  defines setvect MIDSP_1:def_12_:_
 for M being MidSp holds setvect M =  {  X where X is Subset of [: the carrier of M, the carrier of M:] : X is Vector of M  }  ;

theorem Th48: :: MIDSP_1:48
for M being MidSp
for x being set holds
( x is Vector of M iff x in setvect M )
proof
let M be MidSp; ::_thesis: for x being set holds
( x is Vector of M iff x in setvect M )
let x be set ; ::_thesis: ( x is Vector of M iff x in setvect M )
thus  ( x is Vector of M implies x in setvect M ) ; ::_thesis: ( x in setvect M implies x is Vector of M )
thus  ( x in setvect M implies x is Vector of M ) ::_thesis: verum
proof
assume  x in setvect M ; ::_thesis: x is Vector of M
then  ex X being Subset of [: the carrier of M, the carrier of M:] st
( x = X & X is Vector of M ) ;
hence  x is Vector of M ; ::_thesis: verum
end;
end;

registration
let M be MidSp;
cluster setvect M ->  non empty ;
coherence
 not setvect M is empty
proof
 ID M in setvect M ;
hence  not setvect M is empty ; ::_thesis: verum
end;
end;


definition
let M be MidSp;
let u1, v1 be Element of setvect M;
funcu1 + v1 ->  Element of setvect M means :Def13: :: MIDSP_1:def 13
 for u, v being Vector of M st u1 = u & v1 = v holds
it = u + v;
existence
 ex b1 being Element of setvect M st
for u, v being Vector of M st u1 = u & v1 = v holds
b1 = u + v
proof
reconsider u2 = u1, v2 = v1 as Vector of M by Th48;
reconsider suma = u2 + v2 as Element of setvect M by Th48;
take  suma ; ::_thesis: for u, v being Vector of M st u1 = u & v1 = v holds
suma = u + v
thus  for u, v being Vector of M st u1 = u & v1 = v holds
suma = u + v ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of setvect M st ( for u, v being Vector of M st u1 = u & v1 = v holds
b1 = u + v ) & ( for u, v being Vector of M st u1 = u & v1 = v holds
b2 = u + v ) holds
b1 = b2
proof
reconsider u = u1, v = v1 as Vector of M by Th48;
let W1, W2 be Element of setvect M; ::_thesis: ( ( for u, v being Vector of M st u1 = u & v1 = v holds
W1 = u + v ) & ( for u, v being Vector of M st u1 = u & v1 = v holds
W2 = u + v ) implies W1 = W2 )
assume that
A1: for u, v being Vector of M st u1 = u & v1 = v holds
W1 = u + v and
A2: for u, v being Vector of M st u1 = u & v1 = v holds
W2 = u + v ; ::_thesis: W1 = W2
 W1 = u + v by A1;
hence  W1 = W2 by A2; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines + MIDSP_1:def_13_:_
 for M being MidSp
for u1, v1, b4 being Element of setvect M holds
( b4 = u1 + v1 iff for u, v being Vector of M st u1 = u & v1 = v holds
b4 = u + v );

theorem Th49: :: MIDSP_1:49
for M being MidSp
for u1, v1 being Element of setvect M holds u1 + v1 = v1 + u1
proof
let M be MidSp; ::_thesis: for u1, v1 being Element of setvect M holds u1 + v1 = v1 + u1
let u1, v1 be Element of setvect M; ::_thesis: u1 + v1 = v1 + u1
reconsider u = u1, v = v1 as Vector of M by Th48;
thus u1 + v1 = u + v by Def13
.= v + u by Th46
.= v1 + u1 by Def13 ; ::_thesis: verum
end;

theorem Th50: :: MIDSP_1:50
for M being MidSp
for u1, v1, w1 being Element of setvect M holds (u1 + v1) + w1 = u1 + (v1 + w1)
proof
let M be MidSp; ::_thesis: for u1, v1, w1 being Element of setvect M holds (u1 + v1) + w1 = u1 + (v1 + w1)
let u1, v1, w1 be Element of setvect M; ::_thesis: (u1 + v1) + w1 = u1 + (v1 + w1)
reconsider u = u1, v = v1, w = w1 as Vector of M by Th48;
A1: v1 + w1 = v + w by Def13;
 u1 + v1 = u + v by Def13;
hence (u1 + v1) + w1 = (u + v) + w by Def13
.= u + (v + w) by Th43
.= u1 + (v1 + w1) by A1, Def13 ;
::_thesis: verum
end;

definition
let M be MidSp;
func addvect M ->  BinOp of (setvect M) means :Def14: :: MIDSP_1:def 14
 for u1, v1 being Element of setvect M holds it . (u1,v1) = u1 + v1;
existence
 ex b1 being BinOp of (setvect M) st
for u1, v1 being Element of setvect M holds b1 . (u1,v1) = u1 + v1
proof
defpred S1[ Element of setvect M, Element of setvect M, Element of setvect M] means $3 = $1 + $2;
A1: for u1, v1 being Element of setvect M ex W being Element of setvect M st S1[u1,v1,W] ;
consider o being BinOp of (setvect M) such that
A2: for u1, v1 being Element of setvect M holds S1[u1,v1,o . (u1,v1)] from BINOP_1:sch_3(A1);
take  o ; ::_thesis: for u1, v1 being Element of setvect M holds o . (u1,v1) = u1 + v1
thus  for u1, v1 being Element of setvect M holds o . (u1,v1) = u1 + v1 by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (setvect M) st ( for u1, v1 being Element of setvect M holds b1 . (u1,v1) = u1 + v1 ) & ( for u1, v1 being Element of setvect M holds b2 . (u1,v1) = u1 + v1 ) holds
b1 = b2
proof
let f, g be BinOp of (setvect M); ::_thesis: ( ( for u1, v1 being Element of setvect M holds f . (u1,v1) = u1 + v1 ) & ( for u1, v1 being Element of setvect M holds g . (u1,v1) = u1 + v1 ) implies f = g )
assume that
A3: for u1, v1 being Element of setvect M holds f . (u1,v1) = u1 + v1 and
A4: for u1, v1 being Element of setvect M holds g . (u1,v1) = u1 + v1 ; ::_thesis: f = g
 for u1, v1 being Element of setvect M holds f . (u1,v1) = g . (u1,v1)
proof
let u1, v1 be Element of setvect M; ::_thesis: f . (u1,v1) = g . (u1,v1)
 f . (u1,v1) = u1 + v1 by A3;
hence  f . (u1,v1) = g . (u1,v1) by A4; ::_thesis: verum
end;
hence  f = g by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines addvect MIDSP_1:def_14_:_
 for M being MidSp
for b2 being BinOp of (setvect M) holds
( b2 = addvect M iff for u1, v1 being Element of setvect M holds b2 . (u1,v1) = u1 + v1 );

theorem Th51: :: MIDSP_1:51
for M being MidSp
for W being Element of setvect M ex T being Element of setvect M st W + T = ID M
proof
let M be MidSp; ::_thesis: for W being Element of setvect M ex T being Element of setvect M st W + T = ID M
let W be Element of setvect M; ::_thesis: ex T being Element of setvect M st W + T = ID M
reconsider x = W as Vector of M by Th48;
consider y being Vector of M such that
A1: x + y = ID M by Th45;
reconsider T = y as Element of setvect M by Th48;
 x + y = W + T by Def13;
hence  ex T being Element of setvect M st W + T = ID M by A1; ::_thesis: verum
end;

theorem Th52: :: MIDSP_1:52
for M being MidSp
for W, W1, W2 being Element of setvect M st W + W1 = ID M & W + W2 = ID M holds
W1 = W2
proof
let M be MidSp; ::_thesis: for W, W1, W2 being Element of setvect M st W + W1 = ID M & W + W2 = ID M holds
W1 = W2
let W, W1, W2 be Element of setvect M; ::_thesis: ( W + W1 = ID M & W + W2 = ID M implies W1 = W2 )
assume A1: ( W + W1 = ID M & W + W2 = ID M ) ; ::_thesis: W1 = W2
reconsider x = W, y1 = W1, y2 = W2 as Vector of M by Th48;
x + y1 = W + W2 by A1, Def13
.= x + y2 by Def13 ;
hence  W1 = W2 by Th47; ::_thesis: verum
end;

definition
let M be MidSp;
func complvect M ->  UnOp of (setvect M) means :Def15: :: MIDSP_1:def 15
 for W being Element of setvect M holds W + (it . W) = ID M;
existence
 ex b1 being UnOp of (setvect M) st
for W being Element of setvect M holds W + (b1 . W) = ID M
proof
defpred S1[ Element of setvect M, Element of setvect M] means $1 + $2 = ID M;
A1: for W being Element of setvect M ex T being Element of setvect M st S1[W,T] by Th51;
consider o being UnOp of (setvect M) such that
A2: for W being Element of setvect M holds S1[W,o . W] from FUNCT_2:sch_3(A1);
take  o ; ::_thesis: for W being Element of setvect M holds W + (o . W) = ID M
thus  for W being Element of setvect M holds W + (o . W) = ID M by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being UnOp of (setvect M) st ( for W being Element of setvect M holds W + (b1 . W) = ID M ) & ( for W being Element of setvect M holds W + (b2 . W) = ID M ) holds
b1 = b2
proof
let f, g be UnOp of (setvect M); ::_thesis: ( ( for W being Element of setvect M holds W + (f . W) = ID M ) & ( for W being Element of setvect M holds W + (g . W) = ID M ) implies f = g )
assume A3: ( ( for W being Element of setvect M holds W + (f . W) = ID M ) & ( for W being Element of setvect M holds W + (g . W) = ID M ) ) ; ::_thesis: f = g
 for W being Element of setvect M holds f . W = g . W
proof
let W be Element of setvect M; ::_thesis: f . W = g . W
 ( W + (f . W) = ID M & W + (g . W) = ID M ) by A3;
hence  f . W = g . W by Th52; ::_thesis: verum
end;
hence  f = g by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines complvect MIDSP_1:def_15_:_
 for M being MidSp
for b2 being UnOp of (setvect M) holds
( b2 = complvect M iff for W being Element of setvect M holds W + (b2 . W) = ID M );

definition
let M be MidSp;
func zerovect M ->  Element of setvect M equals :: MIDSP_1:def 16
 ID M;
coherence
 ID M is Element of setvect M by Th48;
end;

:: deftheorem  defines zerovect MIDSP_1:def_16_:_
 for M being MidSp holds zerovect M = ID M;

definition
let M be MidSp;
func vectgroup M ->  addLoopStr  equals :: MIDSP_1:def 17
 addLoopStr(# (setvect M),(addvect M),(zerovect M) #);
coherence
 addLoopStr(# (setvect M),(addvect M),(zerovect M) #) is addLoopStr ;
end;

:: deftheorem  defines vectgroup MIDSP_1:def_17_:_
 for M being MidSp holds vectgroup M = addLoopStr(# (setvect M),(addvect M),(zerovect M) #);

registration
let M be MidSp;
cluster vectgroup M ->  non empty strict ;
coherence
 ( vectgroup M is strict & not vectgroup M is empty ) ;
end;

theorem :: MIDSP_1:53
for M being MidSp holds the carrier of (vectgroup M) = setvect M ;

theorem :: MIDSP_1:54
for M being MidSp holds the addF of (vectgroup M) = addvect M ;

theorem :: MIDSP_1:55
for M being MidSp holds 0. (vectgroup M) = zerovect M ;

theorem :: MIDSP_1:56
for M being MidSp holds
( vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )
proof
let M be MidSp; ::_thesis: ( vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )
set GS = vectgroup M;
thus  vectgroup M is add-associative ::_thesis: ( vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )
proof
let x, y, z be Element of (vectgroup M); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider xx = x, yy = y, zz = z as Element of setvect M ;
thus (x + y) + z = (addvect M) . ((xx + yy),zz) by Def14
.= (xx + yy) + zz by Def14
.= xx + (yy + zz) by Th50
.= (addvect M) . (xx,(yy + zz)) by Def14
.= x + (y + z) by Def14 ; ::_thesis: verum
end;
thus  vectgroup M is right_zeroed ::_thesis: ( vectgroup M is right_complementable & vectgroup M is Abelian )
proof
let x be Element of (vectgroup M); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (vectgroup M)) = x
reconsider xx = x as Element of setvect M ;
thus  x + (0. (vectgroup M)) = x ::_thesis: verum
proof
reconsider xxx = xx as Vector of M by Th48;
xx + (zerovect M) = xxx + (ID M) by Def13
.= x by Th44 ;
hence  x + (0. (vectgroup M)) = x by Def14; ::_thesis: verum
end;
end;
thus  vectgroup M is right_complementable ::_thesis: vectgroup M is Abelian
proof
let x be Element of (vectgroup M); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider xx = x as Element of setvect M ;
reconsider w = (complvect M) . xx as Element of (vectgroup M) ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: x + w = 0. (vectgroup M)
thus x + w = xx + ((complvect M) . xx) by Def14
.= 0. (vectgroup M) by Def15 ; ::_thesis: verum
end;
thus  vectgroup M is Abelian ::_thesis: verum
proof
let x, y be Element of (vectgroup M); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider xx = x, yy = y as Element of setvect M ;
thus x + y = xx + yy by Def14
.= yy + xx by Th49
.= y + x by Def14 ; ::_thesis: verum
end;
end;