begin
definition
let IT be non
empty AffinStruct ;
attr IT is
WeakAffVect-like means :
Def1:
( ( for
a,
b,
c being
Element of st
a,
b // c,
c holds
a = b ) & ( for
a,
b,
c,
d,
p,
q being
Element of st
a,
b // p,
q &
c,
d // p,
q holds
a,
b // c,
d ) & ( for
a,
b,
c being
Element of ex
d being
Element of st
a,
b // c,
d ) & ( for
a,
b,
c,
a',
b',
c' being
Element of st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of ex
b being
Element of st
a,
b // b,
c ) & ( for
a,
b,
c,
d being
Element of st
a,
b // c,
d holds
a,
c // b,
d ) );
end;
:: deftheorem Def1 defines WeakAffVect-like AFVECT0:def 1 :
for
IT being non
empty AffinStruct holds
(
IT is
WeakAffVect-like iff ( ( for
a,
b,
c being
Element of st
a,
b // c,
c holds
a = b ) & ( for
a,
b,
c,
d,
p,
q being
Element of st
a,
b // p,
q &
c,
d // p,
q holds
a,
b // c,
d ) & ( for
a,
b,
c being
Element of ex
d being
Element of st
a,
b // c,
d ) & ( for
a,
b,
c,
a',
b',
c' being
Element of st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of ex
b being
Element of st
a,
b // b,
c ) & ( for
a,
b,
c,
d being
Element of st
a,
b // c,
d holds
a,
c // b,
d ) ) );
theorem
canceled;
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem
for
AFV being
WeakAffVect for
b,
c,
b',
c',
a,
d,
d' being
Element of st
b,
c // b',
c' &
a,
d // b,
c &
a,
d' // b',
c' holds
d = d'
theorem
for
AFV being
WeakAffVect for
a,
b,
a',
b',
c,
d,
d' being
Element of st
a,
b // a',
b' &
c,
d // b,
a &
c,
d' // b',
a' holds
d = d'
theorem
for
AFV being
WeakAffVect for
a,
b,
a',
b',
c,
d,
c',
d',
f,
f' being
Element of st
a,
b // a',
b' &
c,
d // c',
d' &
b,
f // c,
d &
b',
f' // c',
d' holds
a,
f // a',
f'
theorem Th13:
for
AFV being
WeakAffVect for
a,
b,
a',
b',
c,
c' being
Element of st
a,
b // a',
b' &
a,
c // c',
b' holds
b,
c // c',
a'
definition
let AFV be
WeakAffVect;
let a,
b be
Element of ;
pred MDist a,
b means :
Def2:
(
a,
b // b,
a &
a <> b );
irreflexivity
for a being Element of holds
( not a,a // a,a or not a <> a )
;
symmetry
for a, b being Element of st a,b // b,a & a <> b holds
( b,a // a,b & b <> a )
by Th4;
end;
:: deftheorem Def2 defines MDist AFVECT0:def 2 :
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
:: deftheorem Def3 defines Mid AFVECT0:def 3 :
theorem
canceled;
theorem Th21:
theorem
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
for
AFV being
WeakAffVect for
a,
p,
a',
b,
b' being
Element of st
Mid a,
p,
a' &
Mid b,
p,
b' holds
a,
b // b',
a'
theorem
for
AFV being
WeakAffVect for
a,
p,
a',
b,
q,
b' being
Element of st
Mid a,
p,
a' &
Mid b,
q,
b' &
MDist p,
q holds
a,
b // b',
a'
definition
let AFV be
WeakAffVect;
let a,
b be
Element of ;
func PSym a,
b -> Element of
means :
Def4:
Mid b,
a,
it;
correctness
existence
ex b1 being Element of st Mid b,a,b1;
uniqueness
for b1, b2 being Element of st Mid b,a,b1 & Mid b,a,b2 holds
b1 = b2;
by Th26, Th27;
end;
:: deftheorem Def4 defines PSym AFVECT0:def 4 :
theorem
canceled;
theorem
theorem
canceled;
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
for
AFV being
WeakAffVect for
a,
b,
c,
d,
p being
Element of holds
(
a,
b // c,
d iff
PSym p,
a,
PSym p,
b // PSym p,
c,
PSym p,
d )
theorem
theorem Th42:
for
AFV being
WeakAffVect for
a,
b,
c,
p being
Element of holds
(
Mid a,
b,
c iff
Mid PSym p,
a,
PSym p,
b,
PSym p,
c )
theorem Th43:
theorem Th44:
theorem
theorem Th46:
theorem
theorem
definition
let AFV be
WeakAffVect;
let o,
a,
b be
Element of ;
func Padd o,
a,
b -> Element of
means :
Def5:
o,
a // b,
it;
correctness
existence
ex b1 being Element of st o,a // b,b1;
uniqueness
for b1, b2 being Element of st o,a // b,b1 & o,a // b,b2 holds
b1 = b2;
by Def1, Th6;
end;
:: deftheorem Def5 defines Padd AFVECT0:def 5 :
Lm1:
for AFV being WeakAffVect
for o, a, b being Element of holds
( Pcom o,a = b iff a,o // o,b )
definition
let AFV be
WeakAffVect;
let o be
Element of ;
canceled;func Padd o -> BinOp of the
carrier of
AFV means :
Def7:
for
a,
b being
Element of holds
it . a,
b = Padd o,
a,
b;
existence
ex b1 being BinOp of the carrier of AFV st
for a, b being Element of holds b1 . a,b = Padd o,a,b
uniqueness
for b1, b2 being BinOp of the carrier of AFV st ( for a, b being Element of holds b1 . a,b = Padd o,a,b ) & ( for a, b being Element of holds b2 . a,b = Padd o,a,b ) holds
b1 = b2
end;
:: deftheorem AFVECT0:def 6 :
canceled;
:: deftheorem Def7 defines Padd AFVECT0:def 7 :
:: deftheorem Def8 defines Pcom AFVECT0:def 8 :
:: deftheorem defines GroupVect AFVECT0:def 9 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
Lm2:
for AFV being WeakAffVect
for o being Element of
for a, b being Element of holds a + b = b + a
Lm3:
for AFV being WeakAffVect
for o being Element of
for a, b, c being Element of holds (a + b) + c = a + (b + c)
Lm4:
for AFV being WeakAffVect
for o being Element of
for a being Element of holds a + (0. (GroupVect AFV,o)) = a
Lm5:
for AFV being WeakAffVect
for o being Element of holds
( GroupVect AFV,o is Abelian & GroupVect AFV,o is add-associative & GroupVect AFV,o is right_zeroed )
Lm6:
for AFV being WeakAffVect
for o being Element of holds GroupVect AFV,o is right_complementable
theorem Th58:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th66:
theorem Th67:
theorem
canceled;
theorem
theorem Th70:
theorem Th71:
theorem
:: deftheorem Def10 defines is_Iso_of AFVECT0:def 10 :
:: deftheorem Def11 defines are_Iso AFVECT0:def 11 :
theorem
canceled;
theorem
canceled;
theorem Th75:
theorem Th76:
theorem Th77:
theorem