:: AFVECT0 semantic presentation

definition

let c₁ be non empty AffinStruct ;
attr a₁ is WeakAffVect-like means :Def1: :: AFVECT0:def 1
( ( for b₁, b₂, b₃ being Element of a₁ st b₁,b₂ // b₃,b₃ holds
b₁ = b₂ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st b₁,b₂ // b₅,b₆ & b₃,b₄ // b₅,b₆ holds
b₁,b₂ // b₃,b₄ ) & ( for b₁, b₂, b₃ being Element of a₁ ex b₄ being Element of a₁ st b₁,b₂ // b₃,b₄ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st b₁,b₂ // b₄,b₅ & b₁,b₃ // b₄,b₆ holds
b₂,b₃ // b₅,b₆ ) & ( for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st b₁,b₃ // b₃,b₂ ) & ( for b₁, b₂, b₃, b₄ being Element of a₁ st b₁,b₂ // b₃,b₄ holds
b₁,b₃ // b₂,b₄ ) );

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 Th1: :: AFVECT0:1

canceled;

theorem Th2: :: AFVECT0:2

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds b₂,b₃ // b₂,b₃

proof end;

theorem Th3: :: AFVECT0:3

for b₁ being WeakAffVect
for b₂ being Element of b₁ holds b₂,b₂ // b₂,b₂ by Th2;

theorem Th4: :: AFVECT0:4

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₄,b₅ // b₂,b₃

proof end;

theorem Th5: :: AFVECT0:5

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃ // b₂,b₄ holds
b₃ = b₄

proof end;

theorem Th6: :: AFVECT0:6

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂,b₃ // b₄,b₅ & b₂,b₃ // b₄,b₆ holds
b₅ = b₆

proof end;

theorem Th7: :: AFVECT0:7

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds b₂,b₂ // b₃,b₃

proof end;

theorem Th8: :: AFVECT0:8

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₃,b₂ // b₅,b₄

proof end;

theorem Th9: :: AFVECT0:9

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂,b₃ // b₄,b₅ & b₂,b₄ // b₆,b₅ holds
b₃ = b₆

proof end;

theorem Th10: :: AFVECT0:10

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st b₂,b₃ // b₄,b₅ & b₆,b₇ // b₂,b₃ & b₆,b₈ // b₄,b₅ holds
b₇ = b₈

proof end;

theorem Th11: :: AFVECT0:11

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st b₂,b₃ // b₄,b₅ & b₆,b₇ // b₃,b₂ & b₆,b₈ // b₅,b₄ holds
b₇ = b₈

proof end;

theorem Th12: :: AFVECT0:12

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of b₁ st b₂,b₃ // b₄,b₅ & b₆,b₇ // b₈,b₉ & b₃,b₁₀ // b₆,b₇ & b₅,b₁₁ // b₈,b₉ holds
b₂,b₁₀ // b₄,b₁₁

proof end;

theorem Th13: :: AFVECT0:13

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂,b₃ // b₄,b₅ & b₂,b₆ // b₇,b₅ holds
b₃,b₆ // b₇,b₄

proof end;

definition

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

end;

:: deftheorem Def2 defines MDist AFVECT0:def 2 :

theorem Th14: :: AFVECT0:14

canceled;

theorem Th15: :: AFVECT0:15

canceled;

theorem Th16: :: AFVECT0:16

for b₁ being WeakAffVect ex b₂, b₃ being Element of b₁ st
( b₂ <> b₃ & not MDist b₂,b₃ )

proof end;

theorem Th17: :: AFVECT0:17

canceled;

theorem Th18: :: AFVECT0:18

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ st MDist b₂,b₃ & MDist b₂,b₄ & not b₃ = b₄ holds
MDist b₃,b₄

proof end;

theorem Th19: :: AFVECT0:19

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ st MDist b₂,b₃ & b₂,b₃ // b₄,b₅ holds
MDist b₄,b₅

proof end;

definition

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;
pred Mid c₂,c₃,c₄ means :Def3: :: AFVECT0:def 3
a₂,a₃ // a₃,a₄;

end;

:: deftheorem Def3 defines Mid AFVECT0:def 3 :

theorem Th20: :: AFVECT0:20

canceled;

theorem Th21: :: AFVECT0:21

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ st Mid b₂,b₃,b₄ holds
Mid b₄,b₃,b₂

proof end;

theorem Th22: :: AFVECT0:22

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds
( Mid b₂,b₃,b₃ iff b₂ = b₃ )

proof end;

theorem Th23: :: AFVECT0:23

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds
( Mid b₂,b₃,b₂ iff ( b₂ = b₃ or MDist b₂,b₃ ) )

proof end;

theorem Th24: :: AFVECT0:24

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st Mid b₂,b₄,b₃

proof end;

theorem Th25: :: AFVECT0:25

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₂,b₅,b₄ & not b₃ = b₅ holds
MDist b₃,b₅

proof end;

theorem Th26: :: AFVECT0:26

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st Mid b₂,b₃,b₄

proof end;

theorem Th27: :: AFVECT0:27

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₂,b₃,b₅ holds
b₄ = b₅

proof end;

theorem Th28: :: AFVECT0:28

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ st Mid b₂,b₃,b₄ & MDist b₃,b₅ holds
Mid b₂,b₅,b₄

proof end;

theorem Th29: :: AFVECT0:29

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₂,b₅,b₆ & MDist b₃,b₅ holds
b₄ = b₆

proof end;

theorem Th30: :: AFVECT0:30

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₅,b₃,b₆ holds
b₂,b₅ // b₆,b₄

proof end;

theorem Th31: :: AFVECT0:31

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₅,b₆,b₇ & MDist b₃,b₆ holds
b₂,b₅ // b₇,b₄

proof end;

definition

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
func PSym c₂,c₃ -> Element of a₁ means :Def4: :: AFVECT0:def 4
Mid a₃,a₂,a₄;
correctness by Th26, Th27;

end;

:: deftheorem Def4 defines PSym AFVECT0:def 4 :

theorem Th32: :: AFVECT0:32

canceled;

theorem Th33: :: AFVECT0:33

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( PSym b₂,b₃ = b₄ iff b₃,b₂ // b₂,b₄ )

proof end;

theorem Th34: :: AFVECT0:34

canceled;

theorem Th35: :: AFVECT0:35

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds
( PSym b₂,b₃ = b₃ iff ( b₃ = b₂ or MDist b₃,b₂ ) )

proof end;

theorem Th36: :: AFVECT0:36

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds PSym b₂,(PSym b₂,b₃) = b₃

proof end;

theorem Th37: :: AFVECT0:37

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ st PSym b₂,b₃ = PSym b₂,b₄ holds
b₃ = b₄

proof end;

theorem Th38: :: AFVECT0:38

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st PSym b₂,b₄ = b₃

proof end;

theorem Th39: :: AFVECT0:39

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds b₂,b₃ // PSym b₄,b₃, PSym b₄,b₂

proof end;

theorem Th40: :: AFVECT0:40

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds
( b₂,b₃ // b₄,b₅ iff PSym b₆,b₂, PSym b₆,b₃ // PSym b₆,b₄, PSym b₆,b₅ )

proof end;

theorem Th41: :: AFVECT0:41

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( MDist b₂,b₃ iff MDist PSym b₄,b₂, PSym b₄,b₃ )

proof end;

theorem Th42: :: AFVECT0:42

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( Mid b₂,b₃,b₄ iff Mid PSym b₅,b₂, PSym b₅,b₃, PSym b₅,b₄ )

proof end;

theorem Th43: :: AFVECT0:43

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( PSym b₂,b₃ = PSym b₄,b₃ iff ( b₂ = b₄ or MDist b₂,b₄ ) )

proof end;

theorem Th44: :: AFVECT0:44

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds PSym b₂,(PSym b₃,(PSym b₂,b₄)) = PSym (PSym b₂,b₃),b₄

proof end;

theorem Th45: :: AFVECT0:45

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( PSym b₂,(PSym b₃,b₄) = PSym b₃,(PSym b₂,b₄) iff ( b₂ = b₃ or MDist b₂,b₃ or MDist b₃, PSym b₂,b₃ ) )

proof end;

theorem Th46: :: AFVECT0:46

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds PSym b₂,(PSym b₃,(PSym b₄,b₅)) = PSym b₄,(PSym b₃,(PSym b₂,b₅))

proof end;

theorem Th47: :: AFVECT0:47

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ ex b₆ being Element of b₁ st PSym b₂,(PSym b₃,(PSym b₄,b₅)) = PSym b₆,b₅

proof end;

theorem Th48: :: AFVECT0:48

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st PSym b₂,(PSym b₅,b₃) = PSym b₅,(PSym b₄,b₃)

proof end;

definition

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;
func Padd c₂,c₃,c₄ -> Element of a₁ means :Def5: :: AFVECT0:def 5
a₂,a₃ // a₄,a₅;
correctness by Def1, Th6;

end;

:: deftheorem Def5 defines Padd AFVECT0:def 5 :

notation

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
synonym Pcom c₂,c₃ for PSym c₂,c₃;

end;

Lemma31: for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( Pcom b₂,b₃ = b₄ iff b₃,b₂ // b₂,b₄ )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 AFVECT0:def 6 :

:: deftheorem Def7 defines Padd AFVECT0:def 7 :

definition

let c₁ be WeakAffVect;
let c₂ be Element of c₁;
func Pcom c₂ -> UnOp of the carrier of a₁ means :Def8: :: AFVECT0:def 8
for b₁ being Element of a₁ holds a₃ . b₁ = Pcom a₂,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Pcom AFVECT0:def 8 :

definition

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

end;

:: deftheorem Def9 defines GroupVect AFVECT0:def 9 :

registration

let c₁ be WeakAffVect;
let c₂ be Element of c₁;
cluster GroupVect a₁,a₂ -> non empty strict ;
coherence

proof end;

end;

theorem Th49: :: AFVECT0:49

canceled;

theorem Th50: :: AFVECT0:50

canceled;

theorem Th51: :: AFVECT0:51

canceled;

theorem Th52: :: AFVECT0:52

canceled;

theorem Th53: :: AFVECT0:53

canceled;

theorem Th54: :: AFVECT0:54

canceled;

theorem Th55: :: AFVECT0:55

for b₁ being WeakAffVect
for b₂ being Element of b₁ holds
( the carrier of (GroupVect b₁,b₂) = the carrier of b₁ & the add of (GroupVect b₁,b₂) = Padd b₂ & the Zero of (GroupVect b₁,b₂) = b₂ ) ;

theorem Th56: :: AFVECT0:56

canceled;

theorem Th57: :: AFVECT0:57

for b₁ being WeakAffVect
for b₂ being Element of b₁
for b₃, b₄ being Element of (GroupVect b₁,b₂)
for b₅, b₆ being Element of b₁ st b₃ = b₅ & b₄ = b₆ holds
b₃ + b₄ = (Padd b₂) . b₅,b₆ ;

Lemma35: for b₁ being WeakAffVect
for b₂ being Element of b₁
for b₃, b₄ being Element of (GroupVect b₁,b₂) holds b₃ + b₄ = b₄ + b₃

proof end;

Lemma36: for b₁ being WeakAffVect
for b₂ being Element of b₁
for b₃, b₄, b₅ being Element of (GroupVect b₁,b₂) holds (b₃ + b₄) + b₅ = b₃ + (b₄ + b₅)

proof end;

Lemma37: for b₁ being WeakAffVect
for b₂ being Element of b₁
for b₃ being Element of (GroupVect b₁,b₂) holds b₃ + (0. (GroupVect b₁,b₂)) = b₃

proof end;

Lemma38: for b₁ being WeakAffVect
for b₂ being Element of b₁ holds
( GroupVect b₁,b₂ is Abelian & GroupVect b₁,b₂ is add-associative & GroupVect b₁,b₂ is right_zeroed )

proof end;

Lemma39: for b₁ being WeakAffVect
for b₂ being Element of b₁ holds GroupVect b₁,b₂ is right_complementable

proof end;

registration

let c₁ be WeakAffVect;
let c₂ be Element of c₁;
cluster GroupVect a₁,a₂ -> non empty strict Abelian add-associative right_zeroed right_complementable ;
coherence by Lemma38, Lemma39;

end;

theorem Th58: :: AFVECT0:58

for b₁ being WeakAffVect
for b₂ being Element of b₁
for b₃ being Element of (GroupVect b₁,b₂)
for b₄ being Element of b₁ st b₃ = b₄ holds
- b₃ = (Pcom b₂) . b₄

proof end;

theorem Th59: :: AFVECT0:59

for b₁ being WeakAffVect
for b₂ being Element of b₁ holds 0. (GroupVect b₁,b₂) = b₂ ;

theorem Th60: :: AFVECT0:60

canceled;

theorem Th61: :: AFVECT0:61

canceled;

theorem Th62: :: AFVECT0:62

canceled;

theorem Th63: :: AFVECT0:63

canceled;

theorem Th64: :: AFVECT0:64

canceled;

theorem Th65: :: AFVECT0:65

canceled;

theorem Th66: :: AFVECT0:66

for b₁ being WeakAffVect
for b₂ being Element of b₁
for b₃ being Element of (GroupVect b₁,b₂) ex b₄ being Element of (GroupVect b₁,b₂) st b₄ + b₄ = b₃

proof end;

registration

let c₁ be WeakAffVect;
let c₂ be Element of c₁;
cluster GroupVect a₁,a₂ -> non empty strict Abelian add-associative right_zeroed right_complementable Two_Divisible ;
coherence

proof end;

end;

theorem Th67: :: AFVECT0:67

for b₁ being AffVect
for b₂ being Element of b₁
for b₃ being Element of (GroupVect b₁,b₂) st b₃ + b₃ = 0. (GroupVect b₁,b₂) holds
b₃ = 0. (GroupVect b₁,b₂)

proof end;

registration

let c₁ be AffVect;
let c₂ be Element of c₁;
cluster GroupVect a₁,a₂ -> 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 Th68: :: AFVECT0:68

canceled;

theorem Th69: :: AFVECT0:69

for b₁ being AffVect
for b₂ being Element of b₁ holds GroupVect b₁,b₂ is Proper_Uniquely_Two_Divisible_Group

proof end;

registration

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

end;

theorem Th70: :: AFVECT0:70

for b₁ being Proper_Uniquely_Two_Divisible_Group holds AV b₁ is AffVect

proof end;

registration

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

end;

theorem Th71: :: AFVECT0:71

for b₁ being strict AffVect
for b₂ being Element of b₁ holds b₁ = AV (GroupVect b₁,b₂)

proof end;

theorem Th72: :: AFVECT0:72

for b₁ being strict AffinStruct holds
( b₁ is AffVect iff ex b₂ being Proper_Uniquely_Two_Divisible_Group st b₁ = AV b₂ )

proof end;

definition

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

end;

:: deftheorem Def10 defines is_Iso_of AFVECT0:def 10 :

definition

let c₁, c₂ be non empty LoopStr ;
pred c₁,c₂ are_Iso means :Def11: :: AFVECT0:def 11
ex b₁ being Function of the carrier of a₁,the carrier of a₂ st b₁ is_Iso_of a₁,a₂;

end;

:: deftheorem Def11 defines are_Iso AFVECT0:def 11 :

theorem Th73: :: AFVECT0:73

canceled;

theorem Th74: :: AFVECT0:74

canceled;

theorem Th75: :: AFVECT0:75

for b₁ being Proper_Uniquely_Two_Divisible_Group
for b₂ being Function of the carrier of b₁,the carrier of b₁
for b₃ being Element of b₁
for b₄ being Element of (AV b₁) st ( for b₅ being Element of b₁ holds b₂ . b₅ = b₃ + b₅ ) & b₄ = b₃ holds
for b₅, b₆ being Element of b₁ holds
( b₂ . (b₅ + b₆) = (Padd b₄) . (b₂ . b₅),(b₂ . b₆) & b₂ . (0. b₁) = 0. (GroupVect (AV b₁),b₄) & b₂ . (- b₅) = (Pcom b₄) . (b₂ . b₅) )

proof end;

theorem Th76: :: AFVECT0:76

for b₁ being Proper_Uniquely_Two_Divisible_Group
for b₂ being Function of the carrier of b₁,the carrier of b₁
for b₃ being Element of b₁ st ( for b₄ being Element of b₁ holds b₂ . b₄ = b₃ + b₄ ) holds
b₂ is one-to-one

proof end;

theorem Th77: :: AFVECT0:77

proof end;

theorem Th78: :: AFVECT0:78

for b₁ being Proper_Uniquely_Two_Divisible_Group
for b₂ being Element of b₁
for b₃ being Element of (AV b₁) st b₃ = b₂ holds
b₁, GroupVect (AV b₁),b₃ are_Iso

proof end;