:: MIDSP_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

registration
cluster non empty MidStr ;
existence
not for b1 being MidStr holds b1 is empty
proof end;
end;

definition
let MS be non empty MidStr ;
let a, b be Element of MS;
func a @ 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 op2 -> BinOp of {{} } means :: MIDSP_1:def 2
verum;
existence
ex b1 being BinOp of {{} } st verum
;
uniqueness
for b1, b2 being BinOp of {{} } holds b1 = b2
by FUNCT_2:66;
end;

:: deftheorem defines op2 MIDSP_1:def 2 :
for b1 being BinOp of {{} } holds
( b1 = op2 iff verum );

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

:: deftheorem defines Example MIDSP_1:def 3 :
Example = MidStr(# {{} },op2 #);

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

theorem :: MIDSP_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the carrier of Example = {{} } ;

theorem :: MIDSP_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the MIDPOINT of Example = op2 ;

theorem :: MIDSP_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Element of Example holds a = {} by TARSKI:def 1;

theorem :: MIDSP_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Element of Example holds a @ b = op2 . a,b ;

theorem :: MIDSP_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th10: :: MIDSP_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let IT be non empty MidStr ;
attr IT is MidSp-like means :Def4: :: MIDSP_1:def 4
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 Def4 defines MidSp-like MIDSP_1:def 4 :
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 MidStr ;
existence
ex b1 being non empty MidStr st
( b1 is strict & b1 is MidSp-like )
proof 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 func a @ b -> Element of M;
commutativity
for a, b being Element of M holds a @ b = b @ a
by Def4;
end;

theorem :: MIDSP_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th15: :: MIDSP_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c being Element of M holds (a @ b) @ c = (a @ c) @ (b @ c)
proof end;

theorem Th16: :: MIDSP_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c being Element of M holds a @ (b @ c) = (a @ b) @ (a @ c)
proof end;

theorem Th17: :: MIDSP_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b being Element of M st a @ b = a holds
a = b
proof end;

theorem Th18: :: MIDSP_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for x, a, x' being Element of M st x @ a = x' @ a holds
x = x'
proof end;

theorem :: MIDSP_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, x, x' being Element of M st a @ x = a @ x' holds
x = x' by Th18;

definition
let M be MidSp;
let a, b, c, d be Element of M;
pred a,b @@ c,d means :Def5: :: MIDSP_1:def 5
a @ d = b @ c;
end;

:: deftheorem Def5 defines @@ MIDSP_1:def 5 :
for M being MidSp
for a, b, c, d being Element of M holds
( a,b @@ c,d iff a @ d = b @ c );

theorem :: MIDSP_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: MIDSP_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b being Element of M holds a,a @@ b,b
proof end;

theorem Th22: :: MIDSP_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c, d being Element of M st a,b @@ c,d holds
c,d @@ a,b
proof end;

theorem Th23: :: MIDSP_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c being Element of M st a,a @@ b,c holds
b = c
proof end;

theorem Th24: :: MIDSP_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c being Element of M st a,b @@ c,c holds
a = b
proof end;

theorem Th25: :: MIDSP_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b being Element of M holds a,b @@ a,b
proof end;

theorem Th26: :: MIDSP_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c being Element of M ex d being Element of M st a,b @@ c,d
proof end;

theorem Th27: :: MIDSP_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c, d, d' being Element of M st a,b @@ c,d & a,b @@ c,d' holds
d = d'
proof end;

theorem Th28: :: MIDSP_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th29: :: MIDSP_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, a', b', c, c' being Element of M st a,b @@ a',b' & b,c @@ b',c' holds
a,c @@ a',c'
proof end;

definition
let M be MidSp;
let p be Element of [:the carrier of M,the carrier of M:];
:: original: `1
redefine func p `1 -> Element of M;
coherence
p `1 is Element of M
by MCART_1:10;
end;

definition
let M be MidSp;
let p be Element of [:the carrier of M,the carrier of M:];
:: original: `2
redefine func p `2 -> Element of M;
coherence
p `2 is Element of M
by MCART_1:10;
end;

definition
let M be MidSp;
let p, q be Element of [:the carrier of M,the carrier of M:];
pred p ## q means :Def6: :: MIDSP_1:def 6
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 Th25;
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 Th22;
end;

:: deftheorem Def6 defines ## MIDSP_1:def 6 :
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 );

definition
let M be MidSp;
let a, b be Element of M;
:: original: [
redefine func [a,b] -> Element of [:the carrier of M,the carrier of M:];
coherence
[a,b] is Element of [:the carrier of M,the carrier of M:]
by ZFMISC_1:def 2;
end;

theorem :: MIDSP_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th31: :: MIDSP_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c, d being Element of M st a,b @@ c,d holds
[a,b] ## [c,d]
proof end;

theorem Th32: :: MIDSP_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c, d being Element of M st [a,b] ## [c,d] holds
a,b @@ c,d
proof end;

theorem :: MIDSP_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th35: :: MIDSP_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: MIDSP_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th35;

theorem :: MIDSP_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th35;

theorem :: MIDSP_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th35;

theorem Th39: :: MIDSP_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let M be MidSp;
let p be Element of [:the carrier of M,the carrier of M:];
func p ~ -> Subset of [:the carrier of M,the carrier of M:] equals :: MIDSP_1:def 7
{ 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 Th39;
end;

:: deftheorem defines ~ MIDSP_1:def 7 :
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:];
cluster p ~ -> non empty ;
coherence
not p ~ is empty
by Th39;
end;

theorem :: MIDSP_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th41: :: MIDSP_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th42: :: MIDSP_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th43: :: MIDSP_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th44: :: MIDSP_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c, d being Element of M st [a,b] ~ = [c,d] ~ holds
a @ d = b @ c
proof end;

theorem :: MIDSP_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :Def8: :: MIDSP_1:def 8
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 end;
end;

:: deftheorem Def8 defines Vector MIDSP_1:def 8 :
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 func p ~ -> Vector of M;
coherence
p ~ is Vector of M
by Def8;
end;

theorem :: MIDSP_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th48: :: MIDSP_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let M be MidSp;
func ID M -> Vector of M equals :: MIDSP_1:def 9
{ 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 end;
end;

:: deftheorem defines ID MIDSP_1:def 9 :
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 :: MIDSP_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th50: :: MIDSP_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for b being Element of M holds ID M = [b,b] ~
proof end;

theorem Th51: :: MIDSP_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for u, v being Vector of M ex w 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 & w = [(p `1 ),(q `2 )] ~ )
proof end;

theorem Th52: :: MIDSP_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for u, v, w, w' 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 & w' = [(p `1 ),(q `2 )] ~ ) holds
w = w'
proof end;

definition
let M be MidSp;
let u, v be Vector of M;
func u + v -> Vector of M means :Def10: :: MIDSP_1:def 10
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 )] ~ )
by Th51;
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 Th52;
end;

:: deftheorem Def10 defines + MIDSP_1:def 10 :
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 Th53: :: MIDSP_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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

:: deftheorem defines vect MIDSP_1:def 11 :
for M being MidSp
for a, b being Element of M holds vect a,b = [a,b] ~ ;

theorem :: MIDSP_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th55: :: MIDSP_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th56: :: MIDSP_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th42;

theorem Th57: :: MIDSP_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th44;

theorem Th58: :: MIDSP_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for b being Element of M holds ID M = vect b,b by Th50;

theorem :: MIDSP_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c being Element of M st vect a,b = vect a,c holds
b = c
proof end;

theorem Th60: :: MIDSP_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b, c being Element of M holds (vect a,b) + (vect b,c) = vect a,c
proof end;

theorem Th61: :: MIDSP_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b being Element of M holds [a,(a @ b)] ## [(a @ b),b]
proof end;

theorem :: MIDSP_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for a, b being Element of M holds (vect a,(a @ b)) + (vect a,(a @ b)) = vect a,b
proof end;

theorem Th63: :: MIDSP_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for u, v, w being Vector of M holds (u + v) + w = u + (v + w)
proof end;

theorem Th64: :: MIDSP_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for u being Vector of M holds u + (ID M) = u
proof end;

theorem Th65: :: MIDSP_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for u being Vector of M ex v being Vector of M st u + v = ID M
proof end;

theorem Th66: :: MIDSP_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for u, v being Vector of M holds u + v = v + u
proof end;

theorem Th67: :: MIDSP_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for u, v, w being Vector of M st u + v = u + w holds
v = w
proof end;

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

:: deftheorem defines - MIDSP_1:def 12 :
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 13
{ 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 13 :
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 :: MIDSP_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th71: :: MIDSP_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for x being set holds
( x is Vector of M iff x in setvect M )
proof end;

registration
let M be MidSp;
cluster setvect M -> non empty ;
coherence
not setvect M is empty
proof end;
end;

definition
let M be MidSp;
let u1, v1 be Element of setvect M;
func u1 + v1 -> Element of setvect M means :Def14: :: MIDSP_1:def 14
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 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 end;
end;

:: deftheorem Def14 defines + MIDSP_1:def 14 :
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 :: MIDSP_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th74: :: MIDSP_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for u1, v1 being Element of setvect M holds u1 + v1 = v1 + u1
proof end;

theorem Th75: :: MIDSP_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for u1, v1, w1 being Element of setvect M holds (u1 + v1) + w1 = u1 + (v1 + w1)
proof end;

definition
let M be MidSp;
func addvect M -> BinOp of setvect M means :Def15: :: MIDSP_1:def 15
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 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 end;
end;

:: deftheorem Def15 defines addvect MIDSP_1:def 15 :
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 :: MIDSP_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th77: :: MIDSP_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp
for W being Element of setvect M ex T being Element of setvect M st W + T = ID M
proof end;

theorem Th78: :: MIDSP_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let M be MidSp;
func complvect M -> UnOp of setvect M means :Def16: :: MIDSP_1:def 16
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 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 end;
end;

:: deftheorem Def16 defines complvect MIDSP_1:def 16 :
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 17
ID M;
coherence
ID M is Element of setvect M
by Th71;
end;

:: deftheorem defines zerovect MIDSP_1:def 17 :
for M being MidSp holds zerovect M = ID M;

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

:: deftheorem defines vectgroup MIDSP_1:def 18 :
for M being MidSp holds vectgroup M = LoopStr(# (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 )
proof end;
end;

theorem :: MIDSP_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp holds the carrier of (vectgroup M) = setvect M ;

theorem :: MIDSP_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp holds the add of (vectgroup M) = addvect M ;

theorem :: MIDSP_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MIDSP_1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being MidSp holds the Zero of (vectgroup M) = zerovect M ;

theorem :: MIDSP_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;