:: AFVECT0 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem Th2: :: AFVECT0:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th4: :: AFVECT0:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th5: :: AFVECT0:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th6: :: AFVECT0:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th7: :: AFVECT0:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th8: :: AFVECT0:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
:: deftheorem Def3 defines Mid AFVECT0:def 3 :
theorem :: AFVECT0:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem Th21: :: AFVECT0:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th23: :: AFVECT0:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th24: :: AFVECT0:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th25: :: AFVECT0:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th26: :: AFVECT0:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th27: :: AFVECT0:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th28: :: AFVECT0:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th29: :: AFVECT0:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th30: :: AFVECT0:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem Th35: :: AFVECT0:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th36: :: AFVECT0:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th37: :: AFVECT0:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th39: :: AFVECT0:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th40: :: AFVECT0:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th42: :: AFVECT0:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th44: :: AFVECT0:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th46: :: AFVECT0:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:48
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:50
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:51
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:52
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:53
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:54
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:55
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:56
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem Th57: :: AFVECT0:57
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:59
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:60
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:61
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:62
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:63
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:64
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:65
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem Th66: :: AFVECT0:66
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th67: :: AFVECT0:67
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:68
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem Th69: :: AFVECT0:69
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th70: :: AFVECT0:70
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th71: :: AFVECT0:71
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:72
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
:: deftheorem Def10 defines is_Iso_of AFVECT0:def 10 :
:: deftheorem Def11 defines are_Iso AFVECT0:def 11 :
theorem :: AFVECT0:73
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: AFVECT0:74
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem Th75: :: AFVECT0:75
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th76: :: AFVECT0:76
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th77: :: AFVECT0:77
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: AFVECT0:78
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)