:: MIDSP_2 semantic presentation

definition

let c₁ be non empty LoopStr ;
let c₂ be Element of c₁;
func Double c₂ -> Element of a₁ equals :: MIDSP_2:def 1
a₂ + a₂;
coherence ;

end;

:: deftheorem Def1 defines Double MIDSP_2:def 1 :

definition

let c₁ be non empty MidStr ;
let c₂ be non empty LoopStr ;
let c₃ be Function of [:the carrier of c₁,the carrier of c₁:],the carrier of c₂;
pred c₁,c₂ are_associated_wrp c₃ means :Def2: :: MIDSP_2:def 2
for b₁, b₂, b₃ being Point of a₁ holds
( b₁ @ b₂ = b₃ iff a₃ . b₁,b₃ = a₃ . b₃,b₂ );

end;

:: deftheorem Def2 defines are_associated_wrp MIDSP_2:def 2 :

theorem Th1: :: MIDSP_2:1

for b₁ being non empty LoopStr
for b₂ being non empty MidStr
for b₃ being Point of b₂
for b₄ being Function of [:the carrier of b₂,the carrier of b₂:],the carrier of b₁ st b₂,b₁ are_associated_wrp b₄ holds
b₃ @ b₃ = b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty LoopStr ;
let c₃ be Function of [:c₁,c₁:],the carrier of c₂;
pred c₃ is_atlas_of c₁,c₂ means :Def3: :: MIDSP_2:def 3
( ( for b₁ being Element of a₁
for b₂ being Element of a₂ ex b₃ being Element of a₁ st a₃ . b₁,b₃ = b₂ ) & ( for b₁, b₂, b₃ being Element of a₁ st a₃ . b₁,b₂ = a₃ . b₁,b₃ holds
b₂ = b₃ ) & ( for b₁, b₂, b₃ being Element of a₁ holds (a₃ . b₁,b₂) + (a₃ . b₂,b₃) = a₃ . b₁,b₃ ) );

end;

:: deftheorem Def3 defines is_atlas_of MIDSP_2:def 3 :

definition

let c₁ be non empty set ;
let c₂ be non empty LoopStr ;
let c₃ be Function of [:c₁,c₁:],the carrier of c₂;
let c₄ be Element of c₁;
let c₅ be Element of c₂;
assume E4: c₃ is_atlas_of c₁,c₂ ;
func c₄,c₅ . c₃ -> Element of a₁ means :Def4: :: MIDSP_2:def 4
a₃ . a₄,a₆ = a₅;
existence by E4, Def3;
uniqueness by E4, Def3;

end;

:: deftheorem Def4 defines . MIDSP_2:def 4 :

theorem Th2: :: MIDSP_2:2

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr holds Double (0. b₁) = 0. b₁ by RLVECT_1:def 7;

theorem Th3: :: MIDSP_2:3

canceled;

theorem Th4: :: MIDSP_2:4

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Function of [:b₁,b₁:],the carrier of b₃ st b₄ is_atlas_of b₁,b₃ holds
b₄ . b₂,b₂ = 0. b₃

proof end;

theorem Th5: :: MIDSP_2:5

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being non empty add-associative right_zeroed right_complementable LoopStr
for b₅ being Function of [:b₁,b₁:],the carrier of b₄ st b₅ is_atlas_of b₁,b₄ & b₅ . b₂,b₃ = 0. b₄ holds
b₂ = b₃

proof end;

theorem Th6: :: MIDSP_2:6

proof end;

theorem Th7: :: MIDSP_2:7

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being non empty add-associative right_zeroed right_complementable LoopStr
for b₇ being Function of [:b₁,b₁:],the carrier of b₆ st b₇ is_atlas_of b₁,b₆ & b₇ . b₂,b₃ = b₇ . b₄,b₅ holds
b₇ . b₃,b₂ = b₇ . b₅,b₄

proof end;

theorem Th8: :: MIDSP_2:8

for b₁ being non empty set
for b₂ being non empty add-associative right_zeroed right_complementable LoopStr
for b₃ being Function of [:b₁,b₁:],the carrier of b₂ st b₃ is_atlas_of b₁,b₂ holds
for b₄ being Element of b₁
for b₅ being Element of b₂ ex b₆ being Element of b₁ st b₃ . b₆,b₄ = b₅

proof end;

theorem Th9: :: MIDSP_2:9

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁
for b₅ being non empty add-associative right_zeroed right_complementable LoopStr
for b₆ being Function of [:b₁,b₁:],the carrier of b₅ st b₆ is_atlas_of b₁,b₅ & b₆ . b₂,b₃ = b₆ . b₄,b₃ holds
b₂ = b₄

proof end;

theorem Th10: :: MIDSP_2:10

for b₁ being non empty MidStr
for b₂, b₃ being Point of b₁
for b₄ being non empty add-associative right_zeroed right_complementable LoopStr
for b₅ being Function of [:the carrier of b₁,the carrier of b₁:],the carrier of b₄ st b₅ is_atlas_of the carrier of b₁,b₄ & b₁,b₄ are_associated_wrp b₅ holds
b₂ @ b₃ = b₃ @ b₂

proof end;

theorem Th11: :: MIDSP_2:11

proof end;

theorem Th12: :: MIDSP_2:12

canceled;

theorem Th13: :: MIDSP_2:13

for b₁ being non empty Abelian add-associative LoopStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (b₂ + b₃) + (b₄ + b₅) = (b₂ + b₄) + (b₃ + b₅)

proof end;

theorem Th14: :: MIDSP_2:14

for b₁ being non empty Abelian add-associative LoopStr
for b₂, b₃ being Element of b₁ holds Double (b₂ + b₃) = (Double b₂) + (Double b₃) by Th13;

theorem Th15: :: MIDSP_2:15

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds Double (- b₂) = - (Double b₂)

proof end;

theorem Th16: :: MIDSP_2:16

for b₁ being non empty MidStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃ being Function of [:the carrier of b₁,the carrier of b₁:],the carrier of b₂ st b₃ is_atlas_of the carrier of b₁,b₂ & b₁,b₂ are_associated_wrp b₃ holds
for b₄, b₅, b₆, b₇ being Point of b₁ holds
( b₄ @ b₅ = b₆ @ b₇ iff b₃ . b₄,b₇ = b₃ . b₆,b₅ )

proof end;

theorem Th17: :: MIDSP_2:17

for b₁ being non empty set
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃ being Function of [:b₁,b₁:],the carrier of b₂ st b₃ is_atlas_of b₁,b₂ holds
for 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₇,b₈ = Double (b₃ . b₅,b₆)

proof end;

registration

let c₁ be MidSp;
cluster vectgroup a₁ -> Abelian add-associative right_zeroed right_complementable ;
coherence by MIDSP_1:86;

end;

theorem Th18: :: MIDSP_2:18

for b₁ being MidSp holds
( ( for b₂ being set holds
( b₂ is Element of (vectgroup b₁) iff b₂ is Vector of b₁ ) ) & 0. (vectgroup b₁) = ID b₁ & ( for b₂, b₃ being Element of (vectgroup b₁)
for b₄, b₅ being Vector of b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ + b₃ = b₄ + b₅ ) )

proof end;

Lemma20: for b₁ being MidSp holds
( ( for b₂ being Element of (vectgroup b₁) ex b₃ being Element of (vectgroup b₁) st Double b₃ = b₂ ) & ( for b₂ being Element of (vectgroup b₁) st Double b₂ = 0. (vectgroup b₁) holds
b₂ = 0. (vectgroup b₁) ) )

proof end;

definition

let c₁ be non empty LoopStr ;
attr a₁ is midpoint_operator means :Def5: :: MIDSP_2:def 5
( ( for b₁ being Element of a₁ ex b₂ being Element of a₁ st Double b₂ = b₁ ) & ( for b₁ being Element of a₁ st Double b₁ = 0. a₁ holds
b₁ = 0. a₁ ) );

end;

:: deftheorem Def5 defines midpoint_operator MIDSP_2:def 5 :

registration

cluster non empty midpoint_operator -> non empty Fanoian LoopStr ;
coherence

proof end;

end;

registration

cluster non empty strict Abelian add-associative right_zeroed right_complementable Fanoian midpoint_operator LoopStr ;
existence

proof end;

end;

theorem Th19: :: MIDSP_2:19

for b₁ being non empty add-associative right_zeroed right_complementable Fanoian LoopStr
for b₂ being Element of b₁ st b₂ = - b₂ holds
b₂ = 0. b₁

proof end;

theorem Th20: :: MIDSP_2:20

for b₁ being non empty Abelian add-associative right_zeroed right_complementable Fanoian LoopStr
for b₂, b₃ being Element of b₁ st Double b₂ = Double b₃ holds
b₂ = b₃

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr ;
let c₂ be Element of c₁;
func Half c₂ -> Element of a₁ means :Def6: :: MIDSP_2:def 6
Double a₃ = a₂;
existence by Def5;
uniqueness by Th20;

end;

:: deftheorem Def6 defines Half MIDSP_2:def 6 :

theorem Th21: :: MIDSP_2:21

for b₁ being non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr
for b₂, b₃ being Element of b₁ holds
( Half (0. b₁) = 0. b₁ & Half (b₂ + b₃) = (Half b₂) + (Half b₃) & ( Half b₂ = Half b₃ implies b₂ = b₃ ) & Half (Double b₂) = b₂ )

proof end;

theorem Th22: :: MIDSP_2:22

for b₁ being non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr
for b₂ being non empty MidStr
for b₃ being Function of [:the carrier of b₂,the carrier of b₂:],the carrier of b₁ st b₃ is_atlas_of the carrier of b₂,b₁ & b₂,b₁ are_associated_wrp b₃ holds
for b₄, b₅, b₆, b₇ being Point of b₂ holds (b₄ @ b₅) @ (b₆ @ b₇) = (b₄ @ b₆) @ (b₅ @ b₇)

proof end;

theorem Th23: :: MIDSP_2:23

proof end;

registration

let c₁ be MidSp;
cluster vectgroup a₁ -> Abelian add-associative right_zeroed right_complementable Fanoian midpoint_operator ;
coherence

proof end;

end;

definition

let c₁ be MidSp;
let c₂, c₃ be Point of c₁;
func vector c₂,c₃ -> Element of (vectgroup a₁) equals :: MIDSP_2:def 7
vect a₂,a₃;
coherence by Th18;

end;

:: deftheorem Def7 defines vector MIDSP_2:def 7 :

definition

let c₁ be MidSp;
func vect c₁ -> Function of [:the carrier of a₁,the carrier of a₁:],the carrier of (vectgroup a₁) means :Def8: :: MIDSP_2:def 8
for b₁, b₂ being Point of a₁ holds a₂ . b₁,b₂ = vect b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines vect MIDSP_2:def 8 :

theorem Th24: :: MIDSP_2:24

for b₁ being MidSp holds vect b₁ is_atlas_of the carrier of b₁, vectgroup b₁

proof end;

theorem Th25: :: MIDSP_2:25

for b₁ being MidSp
for b₂, b₃, b₄, b₅ being Point of b₁ holds
( vect b₂,b₃ = vect b₄,b₅ iff b₂ @ b₅ = b₃ @ b₄ )

proof end;

theorem Th26: :: MIDSP_2:26

for b₁ being MidSp
for b₂, b₃, b₄ being Point of b₁ holds
( b₂ @ b₃ = b₄ iff vect b₂,b₄ = vect b₄,b₃ )

proof end;

theorem Th27: :: MIDSP_2:27

for b₁ being MidSp holds b₁, vectgroup b₁ are_associated_wrp vect b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr ;
let c₃ be Function of [:c₁,c₁:],the carrier of c₂;
assume E32: c₃ is_atlas_of c₁,c₂ ;
func @ c₃ -> BinOp of a₁ means :Def9: :: MIDSP_2:def 9
for b₁, b₂ being Element of a₁ holds a₃ . b₁,(a₄ . b₁,b₂) = a₃ . (a₄ . b₁,b₂),b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines @ MIDSP_2:def 9 :

theorem Th28: :: MIDSP_2:28

for b₁ being non empty set
for b₂ being non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr
for b₃ being Function of [:b₁,b₁:],the carrier of b₂ st b₃ is_atlas_of b₁,b₂ holds
for b₄, b₅, b₆ being Element of b₁ holds
( (@ b₃) . b₄,b₅ = b₆ iff b₃ . b₄,b₆ = b₃ . b₆,b₅ )

proof end;

registration

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
cluster MidStr(# a₁,a₂ #) -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr ;
let c₃ be Function of [:c₁,c₁:],the carrier of c₂;
func Atlas c₃ -> Function of [:the carrier of MidStr(# a₁,(@ a₃) #),the carrier of MidStr(# a₁,(@ a₃) #):],the carrier of a₂ equals :: MIDSP_2:def 10
a₃;
coherence ;

end;

:: deftheorem Def10 defines Atlas MIDSP_2:def 10 :

Lemma34: for b₁ being non empty set
for b₂ being non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr
for b₃ being Function of [:b₁,b₁:],the carrier of b₂ st b₃ is_atlas_of b₁,b₂ holds
for b₄, b₅, b₆ being Point of MidStr(# b₁,(@ b₃) #) holds
( b₄ @ b₅ = b₆ iff (Atlas b₃) . b₄,b₆ = (Atlas b₃) . b₆,b₅ )

proof end;

theorem Th29: :: MIDSP_2:29

canceled;

theorem Th30: :: MIDSP_2:30

canceled;

theorem Th31: :: MIDSP_2:31

canceled;

theorem Th32: :: MIDSP_2:32

for b₁ being non empty set
for b₂ being non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr
for b₃ being Function of [:b₁,b₁:],the carrier of b₂ st b₃ is_atlas_of b₁,b₂ holds
MidStr(# b₁,(@ b₃) #),b₂ are_associated_wrp Atlas b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr ;
let c₃ be Function of [:c₁,c₁:],the carrier of c₂;
assume E36: c₃ is_atlas_of c₁,c₂ ;
func MidSp. c₃ -> strict MidSp equals :: MIDSP_2:def 11
MidStr(# a₁,(@ a₃) #);
coherence

proof end;

end;

:: deftheorem Def11 defines MidSp. MIDSP_2:def 11 :

theorem Th33: :: MIDSP_2:33

for b₁ being non empty MidStr holds
( b₁ is MidSp iff ex b₂ being non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr ex b₃ being Function of [:the carrier of b₁,the carrier of b₁:],the carrier of b₂ st
( b₃ is_atlas_of the carrier of b₁,b₂ & b₁,b₂ are_associated_wrp b₃ ) )

proof end;

definition

let c₁ be non empty MidStr ;
attr a₂ is strict;
struct AtlasStr of c₁ -> ;
aggr AtlasStr(# algebra, function #) -> AtlasStr of a₁;
sel algebra c₂ -> non empty LoopStr ;
sel function c₂ -> Function of [:the carrier of a₁,the carrier of a₁:],the carrier of the algebra of a₂;

end;

definition

let c₁ be non empty MidStr ;
let c₂ be AtlasStr of c₁;
attr a₂ is ATLAS-like means :Def12: :: MIDSP_2:def 12
( the algebra of a₂ is midpoint_operator & the algebra of a₂ is add-associative & the algebra of a₂ is right_zeroed & the algebra of a₂ is right_complementable & the algebra of a₂ is Abelian & a₁,the algebra of a₂ are_associated_wrp the function of a₂ & the function of a₂ is_atlas_of the carrier of a₁,the algebra of a₂ );

end;

:: deftheorem Def12 defines ATLAS-like MIDSP_2:def 12 :

registration

let c₁ be MidSp;
cluster ATLAS-like AtlasStr of a₁;
existence

proof end;

end;

definition

let c₁ be non empty MidSp;
mode ATLAS of a₁ is ATLAS-like AtlasStr of a₁;

end;

definition

let c₁ be non empty MidStr ;
let c₂ be AtlasStr of c₁;
mode Vector of a₂ is Element of the algebra of a₂;

end;

definition

let c₁ be MidSp;
let c₂ be AtlasStr of c₁;
let c₃, c₄ be Point of c₁;
func c₂ . c₃,c₄ -> Element of the algebra of a₂ equals :: MIDSP_2:def 13
the function of a₂ . a₃,a₄;
coherence ;

end;

:: deftheorem Def13 defines . MIDSP_2:def 13 :

definition

let c₁ be MidSp;
let c₂ be AtlasStr of c₁;
let c₃ be Point of c₁;
let c₄ be Vector of c₂;
func c₃,c₄ . c₂ -> Point of a₁ equals :: MIDSP_2:def 14
a₃,a₄ . the function of a₂;
coherence ;

end;

:: deftheorem Def14 defines . MIDSP_2:def 14 :

definition

let c₁ be MidSp;
let c₂ be ATLAS of c₁;
func 0. c₂ -> Vector of a₂ equals :: MIDSP_2:def 15
0. the algebra of a₂;
coherence ;

end;

:: deftheorem Def15 defines 0. MIDSP_2:def 15 :

theorem Th34: :: MIDSP_2:34

for b₁ being non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr
for b₂ being non empty MidStr
for b₃ being Function of [:the carrier of b₂,the carrier of b₂:],the carrier of b₁
for b₄, b₅, b₆, b₇ being Point of b₂ st b₃ is_atlas_of the carrier of b₂,b₁ & b₂,b₁ are_associated_wrp b₃ holds
( b₄ @ b₅ = b₆ @ b₇ iff b₃ . b₄,b₅ = (b₃ . b₄,b₆) + (b₃ . b₄,b₇) )

proof end;

theorem Th35: :: MIDSP_2:35

for b₁ being non empty Abelian add-associative right_zeroed right_complementable midpoint_operator LoopStr
for b₂ being non empty MidStr
for b₃ being Function of [:the carrier of b₂,the carrier of b₂:],the carrier of b₁
for b₄, b₅, b₆ being Point of b₂ st b₃ is_atlas_of the carrier of b₂,b₁ & b₂,b₁ are_associated_wrp b₃ holds
( b₄ @ b₅ = b₆ iff b₃ . b₄,b₅ = Double (b₃ . b₄,b₆) )

proof end;

theorem Th36: :: MIDSP_2:36

for b₁ being MidSp
for b₂ being ATLAS of b₁
for b₃, b₄, b₅, b₆ being Point of b₁ holds
( b₃ @ b₄ = b₅ @ b₆ iff b₂ . b₃,b₄ = (b₂ . b₃,b₅) + (b₂ . b₃,b₆) )

proof end;

theorem Th37: :: MIDSP_2:37

for b₁ being MidSp
for b₂ being ATLAS of b₁
for b₃, b₄, b₅ being Point of b₁ holds
( b₃ @ b₄ = b₅ iff b₂ . b₃,b₄ = Double (b₂ . b₃,b₅) )

proof end;

theorem Th38: :: MIDSP_2:38

for b₁ being MidSp
for b₂ being ATLAS of b₁ holds
( ( for b₃ being Point of b₁
for b₄ being Vector of b₂ ex b₅ being Point of b₁ st b₂ . b₃,b₅ = b₄ ) & ( for b₃, b₄, b₅ being Point of b₁ st b₂ . b₃,b₄ = b₂ . b₃,b₅ holds
b₄ = b₅ ) & ( for b₃, b₄, b₅ being Point of b₁ holds (b₂ . b₃,b₄) + (b₂ . b₄,b₅) = b₂ . b₃,b₅ ) )

proof end;

theorem Th39: :: MIDSP_2:39

for b₁ being MidSp
for b₂ being ATLAS of b₁
for b₃, b₄, b₅, b₆ being Point of b₁
for b₇ being Vector of b₂ holds
( b₂ . b₃,b₃ = 0. b₂ & ( b₂ . b₃,b₄ = 0. b₂ implies b₃ = b₄ ) & b₂ . b₃,b₄ = - (b₂ . b₄,b₃) & ( b₂ . b₃,b₄ = b₂ . b₅,b₆ implies b₂ . b₄,b₃ = b₂ . b₆,b₅ ) & ( for b₈ being Point of b₁
for b₉ being Vector of b₂ ex b₁₀ being Point of b₁ st b₂ . b₁₀,b₈ = b₉ ) & ( b₂ . b₄,b₃ = b₂ . b₅,b₃ implies b₄ = b₅ ) & ( b₃ @ b₄ = b₅ implies b₂ . b₃,b₅ = b₂ . b₅,b₄ ) & ( b₂ . b₃,b₅ = b₂ . b₅,b₄ implies b₃ @ b₄ = b₅ ) & ( b₃ @ b₄ = b₅ @ b₆ implies b₂ . b₃,b₆ = b₂ . b₅,b₄ ) & ( b₂ . b₃,b₆ = b₂ . b₅,b₄ implies b₃ @ b₄ = b₅ @ b₆ ) & ( b₂ . b₃,b₄ = b₇ implies b₃,b₇ . b₂ = b₄ ) & ( b₃,b₇ . b₂ = b₄ implies b₂ . b₃,b₄ = b₇ ) )

proof end;

theorem Th40: :: MIDSP_2:40

for b₁ being MidSp
for b₂ being ATLAS of b₁
for b₃ being Point of b₁ holds b₃,(0. b₂) . b₂ = b₃

proof end;