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