:: Directed Geometrical Bundles and Their Analytical Representation
:: by Grzegorz Lewandowski, Krzysztof Pra\.zmowski and Bo\.zena Lewandowska
::
:: Received September 24, 1990
:: Copyright (c) 1990 Association of Mizar Users
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 :
for
IT being non
empty AffinStruct holds
(
IT is
WeakAffVect-like iff ( ( 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 ) ) );
theorem :: AFVECT0:1
canceled;
theorem Th2: :: AFVECT0:2
theorem :: AFVECT0:3
theorem Th4: :: AFVECT0:4
theorem Th5: :: AFVECT0:5
theorem Th6: :: AFVECT0:6
theorem Th7: :: AFVECT0:7
theorem Th8: :: AFVECT0:8
theorem :: AFVECT0:9
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'
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'
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'
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'
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
for a being Element of AFV holds
( not a,a // a,a or not a <> a )
;
symmetry
for a, b being Element of AFV 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 :: AFVECT0:14
canceled;
theorem :: AFVECT0:15
canceled;
theorem :: AFVECT0:16
theorem :: AFVECT0:17
canceled;
theorem :: AFVECT0:18
theorem :: AFVECT0:19
:: deftheorem Def3 defines Mid AFVECT0:def 3 :
theorem :: AFVECT0:20
canceled;
theorem Th21: :: AFVECT0:21
theorem :: AFVECT0:22
theorem Th23: :: AFVECT0:23
theorem Th24: :: AFVECT0:24
theorem Th25: :: AFVECT0:25
theorem Th26: :: AFVECT0:26
theorem Th27: :: AFVECT0:27
theorem Th28: :: AFVECT0:28
theorem Th29: :: AFVECT0:29
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'
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'
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
existence
ex b1 being Element of AFV st Mid b,a,b1;
uniqueness
for b1, b2 being Element of AFV st Mid b,a,b1 & Mid b,a,b2 holds
b1 = b2;
by Th26, Th27;
end;
:: deftheorem Def4 defines PSym AFVECT0:def 4 :
theorem :: AFVECT0:32
canceled;
theorem :: AFVECT0:33
theorem :: AFVECT0:34
canceled;
theorem Th35: :: AFVECT0:35
theorem Th36: :: AFVECT0:36
theorem Th37: :: AFVECT0:37
theorem :: AFVECT0:38
theorem Th39: :: AFVECT0:39
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 )
theorem :: AFVECT0:41
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 )
theorem Th43: :: AFVECT0:43
theorem Th44: :: AFVECT0:44
theorem :: AFVECT0:45
theorem Th46: :: AFVECT0:46
theorem :: AFVECT0:47
theorem :: AFVECT0:48
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
existence
ex b1 being Element of AFV st o,a // b,b1;
uniqueness
for b1, b2 being Element of AFV 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 AFV holds
( Pcom o,a = b iff a,o // o,b )
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
ex b1 being BinOp of the carrier of AFV st
for a, b being Element of AFV 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 AFV holds b1 . a,b = Padd o,a,b ) & ( for a, b being Element of AFV 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 :: 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
theorem :: AFVECT0:56
canceled;
theorem :: AFVECT0:57
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
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)
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
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 )
Lm6:
for AFV being WeakAffVect
for o being Element of AFV holds GroupVect AFV,o is right_complementable
theorem Th58: :: AFVECT0:58
theorem :: AFVECT0:59
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
theorem Th67: :: AFVECT0:67
theorem :: AFVECT0:68
canceled;
theorem :: AFVECT0:69
theorem Th70: :: AFVECT0:70
theorem Th71: :: AFVECT0:71
theorem :: AFVECT0:72
:: deftheorem Def10 defines is_Iso_of AFVECT0:def 10 :
:: deftheorem Def11 defines are_Iso AFVECT0:def 11 :
theorem :: AFVECT0:73
canceled;
theorem :: AFVECT0:74
canceled;
theorem Th75: :: AFVECT0:75
theorem Th76: :: AFVECT0:76
theorem Th77: :: AFVECT0:77
theorem :: AFVECT0:78