:: AFVECT0 semantic presentation

definition

let IT be non empty AffinStruct ;
attr IT is WeakAffVect-like means :Def1: :: AFVECT0:def 1
( ( for a, b, c being Element of IT st a,b // c,c holds
a = b ) & ( for a, b, c, d, p, q being Element of IT st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, b, c being Element of IT ex d being Element of IT st a,b // c,d ) & ( for a, b, c, a', b', c' being Element of IT st a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, b, c, d being Element of IT st a,b // c,d holds
a,c // b,d ) );

end;

:: deftheorem Def1 defines WeakAffVect-like AFVECT0:def 1 :

registration

cluster non empty non trivial strict WeakAffVect-like AffinStruct ;
existence

proof end;

end;

definition

mode WeakAffVect is non empty non trivial WeakAffVect-like AffinStruct ;

end;

registration

cluster non empty AffVect-like -> non empty WeakAffVect-like AffinStruct ;
coherence

proof end;

end;

theorem :: AFVECT0:1

canceled;

theorem Th2: :: AFVECT0:2

for AFV being WeakAffVect
for a, b being Element of AFV holds a,b // a,b

proof end;

theorem :: AFVECT0:3

for AFV being WeakAffVect
for a being Element of AFV holds a,a // a,a by Th2;

theorem Th4: :: AFVECT0:4

for AFV being WeakAffVect
for a, b, c, d being Element of AFV st a,b // c,d holds
c,d // a,b

proof end;

theorem Th5: :: AFVECT0:5

for AFV being WeakAffVect
for a, b, c being Element of AFV st a,b // a,c holds
b = c

proof end;

theorem Th6: :: AFVECT0:6

for AFV being WeakAffVect
for a, b, c, d, d' being Element of AFV st a,b // c,d & a,b // c,d' holds
d = d'

proof end;

theorem Th7: :: AFVECT0:7

for AFV being WeakAffVect
for a, b being Element of AFV holds a,a // b,b

proof end;

theorem Th8: :: AFVECT0:8

for AFV being WeakAffVect
for a, b, c, d being Element of AFV st a,b // c,d holds
b,a // d,c

proof end;

theorem :: AFVECT0:9

for AFV being WeakAffVect
for a, b, c, d, b' being Element of AFV st a,b // c,d & a,c // b',d holds
b = b'

proof end;

theorem :: AFVECT0:10

for AFV being WeakAffVect
for b, c, b', c', a, d, d' being Element of AFV st b,c // b',c' & a,d // b,c & a,d' // b',c' holds
d = d'

proof end;

theorem :: AFVECT0:11

for AFV being WeakAffVect
for a, b, a', b', c, d, d' being Element of AFV st a,b // a',b' & c,d // b,a & c,d' // b',a' holds
d = d'

proof end;

theorem :: AFVECT0:12

for AFV being WeakAffVect
for a, b, a', b', c, d, c', d', f, f' being Element of AFV st a,b // a',b' & c,d // c',d' & b,f // c,d & b',f' // c',d' holds
a,f // a',f'

proof end;

theorem Th13: :: AFVECT0:13

for AFV being WeakAffVect
for a, b, a', b', c, c' being Element of AFV st a,b // a',b' & a,c // c',b' holds
b,c // c',a'

proof end;

definition

let AFV be WeakAffVect;
let a, b be Element of AFV;
pred MDist a,b means :Def2: :: AFVECT0:def 2
( a,b // b,a & a <> b );
irreflexivity ;
symmetry by Th4;

end;

:: deftheorem Def2 defines MDist AFVECT0:def 2 :

theorem :: AFVECT0:14

canceled;

theorem :: AFVECT0:15

canceled;

theorem :: AFVECT0:16

for AFV being WeakAffVect ex a, b being Element of AFV st
( a <> b & not MDist a,b )

proof end;

theorem :: AFVECT0:17

canceled;

theorem :: AFVECT0:18

for AFV being WeakAffVect
for a, b, c being Element of AFV st MDist a,b & MDist a,c & not b = c holds
MDist b,c

proof end;

theorem :: AFVECT0:19

for AFV being WeakAffVect
for a, b, c, d being Element of AFV st MDist a,b & a,b // c,d holds
MDist c,d

proof end;

definition

let AFV be WeakAffVect;
let a, b, c be Element of AFV;
pred Mid a,b,c means :Def3: :: AFVECT0:def 3
a,b // b,c;

end;

:: deftheorem Def3 defines Mid AFVECT0:def 3 :

theorem :: AFVECT0:20

canceled;

theorem Th21: :: AFVECT0:21

for AFV being WeakAffVect
for a, b, c being Element of AFV st Mid a,b,c holds
Mid c,b,a

proof end;

theorem :: AFVECT0:22

for AFV being WeakAffVect
for a, b being Element of AFV holds
( Mid a,b,b iff a = b )

proof end;

theorem Th23: :: AFVECT0:23

for AFV being WeakAffVect
for a, b being Element of AFV holds
( Mid a,b,a iff ( a = b or MDist a,b ) )

proof end;

theorem Th24: :: AFVECT0:24

for AFV being WeakAffVect
for a, c being Element of AFV ex b being Element of AFV st Mid a,b,c

proof end;

theorem Th25: :: AFVECT0:25

for AFV being WeakAffVect
for a, b, c, b' being Element of AFV st Mid a,b,c & Mid a,b',c & not b = b' holds
MDist b,b'

proof end;

theorem Th26: :: AFVECT0:26

for AFV being WeakAffVect
for a, b being Element of AFV ex c being Element of AFV st Mid a,b,c

proof end;

theorem Th27: :: AFVECT0:27

for AFV being WeakAffVect
for a, b, c, c' being Element of AFV st Mid a,b,c & Mid a,b,c' holds
c = c'

proof end;

theorem Th28: :: AFVECT0:28

for AFV being WeakAffVect
for a, b, c, b' being Element of AFV st Mid a,b,c & MDist b,b' holds
Mid a,b',c

proof end;

theorem Th29: :: AFVECT0:29

for AFV being WeakAffVect
for a, b, c, b', c' being Element of AFV st Mid a,b,c & Mid a,b',c' & MDist b,b' holds
c = c'

proof end;

theorem Th30: :: AFVECT0:30

for AFV being WeakAffVect
for a, p, a', b, b' being Element of AFV st Mid a,p,a' & Mid b,p,b' holds
a,b // b',a'

proof end;

theorem :: AFVECT0:31

for AFV being WeakAffVect
for a, p, a', b, q, b' being Element of AFV st Mid a,p,a' & Mid b,q,b' & MDist p,q holds
a,b // b',a'

proof end;

definition

let AFV be WeakAffVect;
let a, b be Element of AFV;
func PSym a,b -> Element of AFV means :Def4: :: AFVECT0:def 4
Mid b,a,it;
correctness by Th26, Th27;

end;

:: deftheorem Def4 defines PSym AFVECT0:def 4 :

theorem :: AFVECT0:32

canceled;

theorem :: AFVECT0:33

for AFV being WeakAffVect
for p, a, b being Element of AFV holds
( PSym p,a = b iff a,p // p,b )

proof end;

theorem :: AFVECT0:34

canceled;

theorem Th35: :: AFVECT0:35

for AFV being WeakAffVect
for p, a being Element of AFV holds
( PSym p,a = a iff ( a = p or MDist a,p ) )

proof end;

theorem Th36: :: AFVECT0:36

for AFV being WeakAffVect
for p, a being Element of AFV holds PSym p,(PSym p,a) = a

proof end;

theorem Th37: :: AFVECT0:37

for AFV being WeakAffVect
for p, a, b being Element of AFV st PSym p,a = PSym p,b holds
a = b

proof end;

theorem :: AFVECT0:38

for AFV being WeakAffVect
for p, b being Element of AFV ex a being Element of AFV st PSym p,a = b

proof end;

theorem Th39: :: AFVECT0:39

for AFV being WeakAffVect
for a, b, p being Element of AFV holds a,b // PSym p,b, PSym p,a

proof end;

theorem Th40: :: AFVECT0:40

for AFV being WeakAffVect
for a, b, c, d, p being Element of AFV holds
( a,b // c,d iff PSym p,a, PSym p,b // PSym p,c, PSym p,d )

proof end;

theorem :: AFVECT0:41

for AFV being WeakAffVect
for a, b, p being Element of AFV holds
( MDist a,b iff MDist PSym p,a, PSym p,b )

proof end;

theorem Th42: :: AFVECT0:42

for AFV being WeakAffVect
for a, b, c, p being Element of AFV holds
( Mid a,b,c iff Mid PSym p,a, PSym p,b, PSym p,c )

proof end;

theorem Th43: :: AFVECT0:43

for AFV being WeakAffVect
for p, a, q being Element of AFV holds
( PSym p,a = PSym q,a iff ( p = q or MDist p,q ) )

proof end;

theorem Th44: :: AFVECT0:44

for AFV being WeakAffVect
for q, p, a being Element of AFV holds PSym q,(PSym p,(PSym q,a)) = PSym (PSym q,p),a

proof end;

theorem :: AFVECT0:45

for AFV being WeakAffVect
for p, q, a being Element of AFV holds
( PSym p,(PSym q,a) = PSym q,(PSym p,a) iff ( p = q or MDist p,q or MDist q, PSym p,q ) )

proof end;

theorem Th46: :: AFVECT0:46

for AFV being WeakAffVect
for p, q, r, a being Element of AFV holds PSym p,(PSym q,(PSym r,a)) = PSym r,(PSym q,(PSym p,a))

proof end;

theorem :: AFVECT0:47

for AFV being WeakAffVect
for a, b, c, p being Element of AFV ex d being Element of AFV st PSym a,(PSym b,(PSym c,p)) = PSym d,p

proof end;

theorem :: AFVECT0:48

for AFV being WeakAffVect
for a, p, b being Element of AFV ex c being Element of AFV st PSym a,(PSym c,p) = PSym c,(PSym b,p)

proof end;

definition

let AFV be WeakAffVect;
let o, a, b be Element of AFV;
func Padd o,a,b -> Element of AFV means :Def5: :: AFVECT0:def 5
o,a // b,it;
correctness by Def1, Th6;

end;

:: deftheorem Def5 defines Padd AFVECT0:def 5 :

notation

let AFV be WeakAffVect;
let o, a be Element of AFV;
synonym Pcom o,a for PSym o,a;

end;

Lm1: for AFV being WeakAffVect
for o, a, b being Element of AFV holds
( Pcom o,a = b iff a,o // o,b )

proof end;

definition

let AFV be WeakAffVect;
let o be Element of AFV;
canceled;
func Padd o -> BinOp of the carrier of AFV means :Def7: :: AFVECT0:def 7
for a, b being Element of AFV holds it . a,b = Padd o,a,b;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem AFVECT0:def 6 :

:: deftheorem Def7 defines Padd AFVECT0:def 7 :

definition

let AFV be WeakAffVect;
let o be Element of AFV;
func Pcom o -> UnOp of the carrier of AFV means :Def8: :: AFVECT0:def 8
for a being Element of AFV holds it . a = Pcom o,a;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Pcom AFVECT0:def 8 :

definition

let AFV be WeakAffVect;
let o be Element of AFV;
func GroupVect AFV,o -> strict LoopStr equals :: AFVECT0:def 9
LoopStr(# the carrier of AFV,(Padd o),o #);
correctness ;

end;

:: deftheorem defines GroupVect AFVECT0:def 9 :

registration

let AFV be WeakAffVect;
let o be Element of AFV;
cluster GroupVect AFV,o -> non empty strict ;
coherence

proof end;

end;

theorem :: AFVECT0:49

canceled;

theorem :: AFVECT0:50

canceled;

theorem :: AFVECT0:51

canceled;

theorem :: AFVECT0:52

canceled;

theorem :: AFVECT0:53

canceled;

theorem :: AFVECT0:54

canceled;

theorem :: AFVECT0:55

for AFV being WeakAffVect
for o being Element of AFV holds
( the carrier of (GroupVect AFV,o) = the carrier of AFV & the add of (GroupVect AFV,o) = Padd o & the Zero of (GroupVect AFV,o) = o ) ;

theorem :: AFVECT0:56

canceled;

theorem Th57: :: AFVECT0:57

for AFV being WeakAffVect
for o being Element of AFV
for a, b being Element of (GroupVect AFV,o)
for a', b' being Element of AFV st a = a' & b = b' holds
a + b = (Padd o) . a',b' ;

Lm2: for AFV being WeakAffVect
for o being Element of AFV
for a, b being Element of (GroupVect AFV,o) holds a + b = b + a

proof end;

Lm3: for AFV being WeakAffVect
for o being Element of AFV
for a, b, c being Element of (GroupVect AFV,o) holds (a + b) + c = a + (b + c)

proof end;

Lm4: for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect AFV,o) holds a + (0. (GroupVect AFV,o)) = a

proof end;

Lm5: for AFV being WeakAffVect
for o being Element of AFV holds
( GroupVect AFV,o is Abelian & GroupVect AFV,o is add-associative & GroupVect AFV,o is right_zeroed )

proof end;

Lm6: for AFV being WeakAffVect
for o being Element of AFV holds GroupVect AFV,o is right_complementable

proof end;

registration

let AFV be WeakAffVect;
let o be Element of AFV;
cluster GroupVect AFV,o -> non empty strict Abelian add-associative right_zeroed right_complementable ;
coherence by Lm5, Lm6;

end;

theorem Th58: :: AFVECT0:58

for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect AFV,o)
for a' being Element of AFV st a = a' holds
- a = (Pcom o) . a'

proof end;

theorem :: AFVECT0:59

for AFV being WeakAffVect
for o being Element of AFV holds 0. (GroupVect AFV,o) = o ;

theorem :: AFVECT0:60

canceled;

theorem :: AFVECT0:61

canceled;

theorem :: AFVECT0:62

canceled;

theorem :: AFVECT0:63

canceled;

theorem :: AFVECT0:64

canceled;

theorem :: AFVECT0:65

canceled;

theorem Th66: :: AFVECT0:66

for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect AFV,o) ex b being Element of (GroupVect AFV,o) st b + b = a

proof end;

registration

let AFV be WeakAffVect;
let o be Element of AFV;
cluster GroupVect AFV,o -> non empty strict Abelian add-associative right_zeroed right_complementable Two_Divisible ;
coherence

proof end;

end;

theorem Th67: :: AFVECT0:67

for AFV being AffVect
for o being Element of AFV
for a being Element of (GroupVect AFV,o) st a + a = 0. (GroupVect AFV,o) holds
a = 0. (GroupVect AFV,o)

proof end;

registration

let AFV be AffVect;
let o be Element of AFV;
cluster GroupVect AFV,o -> non empty strict Abelian add-associative right_zeroed right_complementable Fanoian Two_Divisible ;
coherence

proof end;

end;

registration

cluster strict non trivial LoopStr ;
existence

proof end;

end;

definition

mode Proper_Uniquely_Two_Divisible_Group is non trivial Uniquely_Two_Divisible_Group;

end;

theorem :: AFVECT0:68

canceled;

theorem Th69: :: AFVECT0:69

for AFV being AffVect
for o being Element of AFV holds GroupVect AFV,o is Proper_Uniquely_Two_Divisible_Group

proof end;

registration

let AFV be AffVect;
let o be Element of AFV;
cluster GroupVect AFV,o -> non empty strict Abelian add-associative right_zeroed right_complementable Fanoian non trivial Two_Divisible ;
coherence by Th69;

end;

theorem Th70: :: AFVECT0:70

for ADG being Proper_Uniquely_Two_Divisible_Group holds AV ADG is AffVect

proof end;

registration

let ADG be Proper_Uniquely_Two_Divisible_Group;
cluster AV ADG -> non trivial AffVect-like WeakAffVect-like ;
coherence by Th70;

end;

theorem Th71: :: AFVECT0:71

for AFV being strict AffVect
for o being Element of AFV holds AFV = AV (GroupVect AFV,o)

proof end;

theorem :: AFVECT0:72

for AS being strict AffinStruct holds
( AS is AffVect iff ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG )

proof end;

definition

let X, Y be non empty LoopStr ;
let f be Function of the carrier of X,the carrier of Y;
pred f is_Iso_of X,Y means :Def10: :: AFVECT0:def 10
( f is one-to-one & rng f = the carrier of Y & ( for a, b being Element of X holds
( f . (a + b) = (f . a) + (f . b) & f . (0. X) = 0. Y & f . (- a) = - (f . a) ) ) );

end;

:: deftheorem Def10 defines is_Iso_of AFVECT0:def 10 :

definition

let X, Y be non empty LoopStr ;
pred X,Y are_Iso means :Def11: :: AFVECT0:def 11
ex f being Function of the carrier of X,the carrier of Y st f is_Iso_of X,Y;

end;

:: deftheorem Def11 defines are_Iso AFVECT0:def 11 :

theorem :: AFVECT0:73

canceled;

theorem :: AFVECT0:74

canceled;

theorem Th75: :: AFVECT0:75

for ADG being Proper_Uniquely_Two_Divisible_Group
for f being Function of the carrier of ADG,the carrier of ADG
for o' being Element of ADG
for o being Element of (AV ADG) st ( for x being Element of ADG holds f . x = o' + x ) & o = o' holds
for a, b being Element of ADG holds
( f . (a + b) = (Padd o) . (f . a),(f . b) & f . (0. ADG) = 0. (GroupVect (AV ADG),o) & f . (- a) = (Pcom o) . (f . a) )

proof end;

theorem Th76: :: AFVECT0:76

for ADG being Proper_Uniquely_Two_Divisible_Group
for f being Function of the carrier of ADG,the carrier of ADG
for o' being Element of ADG st ( for b being Element of ADG holds f . b = o' + b ) holds
f is one-to-one

proof end;

theorem Th77: :: AFVECT0:77

for ADG being Proper_Uniquely_Two_Divisible_Group
for f being Function of the carrier of ADG,the carrier of ADG
for o' being Element of ADG
for o being Element of (AV ADG) st ( for b being Element of ADG holds f . b = o' + b ) holds
rng f = the carrier of (GroupVect (AV ADG),o)

proof end;

theorem :: AFVECT0:78

for ADG being Proper_Uniquely_Two_Divisible_Group
for o' being Element of ADG
for o being Element of (AV ADG) st o = o' holds
ADG, GroupVect (AV ADG),o are_Iso

proof end;