:: A Construction of Analytical Ordered Trapezium Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received October 29, 1990
:: Copyright (c) 1990 Association of Mizar Users


begin

definition
let V be RealLinearSpace;
let u, v, u1, v1 be VECTOR of ;
pred u,v '||' u1,v1 means :Def1: :: GEOMTRAP:def 1
( u,v // u1,v1 or u,v // v1,u1 );
end;

:: deftheorem Def1 defines '||' GEOMTRAP:def 1 :
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of holds
( u,v '||' u1,v1 iff ( u,v // u1,v1 or u,v // v1,u1 ) );

theorem Th1: :: GEOMTRAP:1
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
OASpace V is OAffinSpace
proof end;

theorem Th2: :: GEOMTRAP:2
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of
for p, q, p1, q1 being Element of st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v // u1,v1 )
proof end;

theorem Th3: :: GEOMTRAP:3
for V being RealLinearSpace
for w, y, u, v, u1, v1 being VECTOR of st Gen w,y holds
for p, q, p1, q1 being Element of the carrier of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v '||' u1,v1 )
proof end;

theorem Th4: :: GEOMTRAP:4
for V being RealLinearSpace
for w, y, u, v, u1, v1 being VECTOR of
for p, q, p1, q1 being Element of the carrier of (AMSpace V,w,y) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v '||' u1,v1 )
proof end;

definition
let V be RealLinearSpace;
let u, v be VECTOR of ;
func u # v -> VECTOR of means :Def2: :: GEOMTRAP:def 2
it + it = u + v;
existence
ex b1 being VECTOR of st b1 + b1 = u + v
proof end;
uniqueness
for b1, b2 being VECTOR of st b1 + b1 = u + v & b2 + b2 = u + v holds
b1 = b2
proof end;
commutativity
for b1, u, v being VECTOR of st b1 + b1 = u + v holds
b1 + b1 = v + u ;
idempotence
for u being VECTOR of holds u + u = u + u ;
end;

:: deftheorem Def2 defines # GEOMTRAP:def 2 :
for V being RealLinearSpace
for u, v, b4 being VECTOR of holds
( b4 = u # v iff b4 + b4 = u + v );

theorem :: GEOMTRAP:5
canceled;

theorem :: GEOMTRAP:6
canceled;

theorem Th7: :: GEOMTRAP:7
for V being RealLinearSpace
for u, w being VECTOR of ex y being VECTOR of st u # y = w
proof end;

theorem Th8: :: GEOMTRAP:8
for V being RealLinearSpace
for u, u1, v, v1 being VECTOR of holds (u # u1) # (v # v1) = (u # v) # (u1 # v1)
proof end;

theorem Th9: :: GEOMTRAP:9
for V being RealLinearSpace
for u, y, w being VECTOR of st u # y = u # w holds
y = w
proof end;

theorem Th10: :: GEOMTRAP:10
for V being RealLinearSpace
for u, v, y being VECTOR of holds u,v // y # u,y # v
proof end;

theorem :: GEOMTRAP:11
for V being RealLinearSpace
for u, v, w being VECTOR of holds u,v '||' w # u,w # v
proof end;

theorem Th12: :: GEOMTRAP:12
for V being RealLinearSpace
for u, v being VECTOR of holds
( 2 * ((u # v) - u) = v - u & 2 * (v - (u # v)) = v - u )
proof end;

theorem Th13: :: GEOMTRAP:13
for V being RealLinearSpace
for u, v being VECTOR of holds u,u # v // u # v,v
proof end;

theorem Th14: :: GEOMTRAP:14
for V being RealLinearSpace
for u, v being VECTOR of holds
( u,v // u,u # v & u,v // u # v,v )
proof end;

Lm1: for V being RealLinearSpace
for u, y, v being VECTOR of st u,y // y,v holds
( v,y // y,u & u,y // u,v & y,v // u,v )
proof end;

theorem Th15: :: GEOMTRAP:15
for V being RealLinearSpace
for u, y, v being VECTOR of st u,y // y,v holds
u # y,y // y,y # v
proof end;

theorem Th16: :: GEOMTRAP:16
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of st u,v // u1,v1 holds
u,v // u # u1,v # v1
proof end;

Lm2: for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of st u,v // u1,v1 holds
u,v '||' u # v1,v # u1
proof end;

Lm3: for V being RealLinearSpace
for u1, u2, v1, v2 being VECTOR of st u1 # u2 = v1 # v2 holds
v1 - u1 = - (v2 - u2)
proof end;

Lm4: for V being RealLinearSpace
for u, v, u1, v1, w, y being VECTOR of st u,v,u1,v1 are_Ort_wrt w,y holds
u,v,v1,u1 are_Ort_wrt w,y
proof end;

Lm5: for V being RealLinearSpace
for u, v, u1, v1, w, y being VECTOR of st u,v,u1,v1 are_Ort_wrt w,y holds
u1,v1,u,v are_Ort_wrt w,y
proof end;

Lm6: for V being RealLinearSpace
for w, y, u, v, u1 being VECTOR of st Gen w,y holds
u,v,u1,u1 are_Ort_wrt w,y
proof end;

Lm7: for V being RealLinearSpace
for w, y, u, v, w1, v1, v2 being VECTOR of st Gen w,y & u,v,w1,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y holds
u,v,v1,v2 are_Ort_wrt w,y
proof end;

Lm8: for V being RealLinearSpace
for w, y, u, v being VECTOR of st Gen w,y & u,v,u,v are_Ort_wrt w,y holds
u = v
proof end;

Lm9: for V being RealLinearSpace
for w, y, u, v, u1 being VECTOR of st Gen w,y holds
( u,v,u1,u1 are_Ort_wrt w,y & u1,u1,u,v are_Ort_wrt w,y )
proof end;

Lm10: for V being RealLinearSpace
for w, y, u1, v1, u, v, u2, v2 being VECTOR of st Gen w,y & ( u1,v1 '||' u,v or u,v '||' u1,v1 ) & ( u2,v2,u,v are_Ort_wrt w,y or u,v,u2,v2 are_Ort_wrt w,y ) & u <> v holds
( u1,v1,u2,v2 are_Ort_wrt w,y & u2,v2,u1,v1 are_Ort_wrt w,y )
proof end;

definition
let V be RealLinearSpace;
let w, y, u, u1, v, v1 be VECTOR of ;
pred u,u1,v,v1 are_DTr_wrt w,y means :Def3: :: GEOMTRAP:def 3
( u,u1 // v,v1 & u,u1,u # u1,v # v1 are_Ort_wrt w,y & v,v1,u # u1,v # v1 are_Ort_wrt w,y );
end;

:: deftheorem Def3 defines are_DTr_wrt GEOMTRAP:def 3 :
for V being RealLinearSpace
for w, y, u, u1, v, v1 being VECTOR of holds
( u,u1,v,v1 are_DTr_wrt w,y iff ( u,u1 // v,v1 & u,u1,u # u1,v # v1 are_Ort_wrt w,y & v,v1,u # u1,v # v1 are_Ort_wrt w,y ) );

theorem :: GEOMTRAP:17
for V being RealLinearSpace
for w, y, u, v being VECTOR of st Gen w,y holds
u,u,v,v are_DTr_wrt w,y
proof end;

theorem :: GEOMTRAP:18
for V being RealLinearSpace
for w, y, u, v being VECTOR of st Gen w,y holds
u,v,u,v are_DTr_wrt w,y
proof end;

theorem Th19: :: GEOMTRAP:19
for V being RealLinearSpace
for u, v, w, y being VECTOR of st u,v,v,u are_DTr_wrt w,y holds
u = v
proof end;

theorem Th20: :: GEOMTRAP:20
for V being RealLinearSpace
for w, y, v1, u, v2 being VECTOR of st Gen w,y & v1,u,u,v2 are_DTr_wrt w,y holds
( v1 = u & u = v2 )
proof end;

theorem Th21: :: GEOMTRAP:21
for V being RealLinearSpace
for w, y, u, v, u1, v1, u2, v2 being VECTOR of st Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & u,v,u2,v2 are_DTr_wrt w,y & u <> v holds
u1,v1,u2,v2 are_DTr_wrt w,y
proof end;

theorem Th22: :: GEOMTRAP:22
for V being RealLinearSpace
for w, y, u, v, u1 being VECTOR of st Gen w,y holds
ex t being VECTOR of st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y )
proof end;

theorem Th23: :: GEOMTRAP:23
for V being RealLinearSpace
for u, v, u1, v1, w, y being VECTOR of st u,v,u1,v1 are_DTr_wrt w,y holds
u1,v1,u,v are_DTr_wrt w,y
proof end;

theorem Th24: :: GEOMTRAP:24
for V being RealLinearSpace
for u, v, u1, v1, w, y being VECTOR of st u,v,u1,v1 are_DTr_wrt w,y holds
v,u,v1,u1 are_DTr_wrt w,y
proof end;

Lm11: for V being RealLinearSpace
for w, y, u, v, u1, v1, u2, v2 being VECTOR of st Gen w,y & u <> v & u,v '||' u,u1 & u,v '||' u,v1 & u,v '||' u,u2 & u,v '||' u,v2 holds
u1,v1 '||' u2,v2
proof end;

theorem Th25: :: GEOMTRAP:25
for V being RealLinearSpace
for w, y, v, u1, u2 being VECTOR of st Gen w,y & v,u1,v,u2 are_DTr_wrt w,y holds
u1 = u2
proof end;

theorem Th26: :: GEOMTRAP:26
for V being RealLinearSpace
for w, y, u, v, u1, v1, v2 being VECTOR of st Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & u,v,u1,v2 are_DTr_wrt w,y & not u = v holds
v1 = v2
proof end;

theorem Th27: :: GEOMTRAP:27
for V being RealLinearSpace
for w, y, u, u1, v, v1, v2 being VECTOR of st Gen w,y & u <> u1 & u,u1,v,v1 are_DTr_wrt w,y & ( u,u1,v,v2 are_DTr_wrt w,y or u,u1,v2,v are_DTr_wrt w,y ) holds
v1 = v2
proof end;

theorem Th28: :: GEOMTRAP:28
for V being RealLinearSpace
for w, y, u, v, u1, v1 being VECTOR of st Gen w,y & u,v,u1,v1 are_DTr_wrt w,y holds
u,v,u # u1,v # v1 are_DTr_wrt w,y
proof end;

theorem Th29: :: GEOMTRAP:29
for V being RealLinearSpace
for w, y, u, v, u1, v1 being VECTOR of st Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & not u,v,u # v1,v # u1 are_DTr_wrt w,y holds
u,v,v # u1,u # v1 are_DTr_wrt w,y
proof end;

theorem Th30: :: GEOMTRAP:30
for V being RealLinearSpace
for w, y, u, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of st u = u1 # t1 & u = u2 # t2 & u = v1 # w1 & u = v2 # w2 & u1,u2,v1,v2 are_DTr_wrt w,y holds
t1,t2,w1,w2 are_DTr_wrt w,y
proof end;

Lm12: for V being RealLinearSpace
for v1, w, y, v2 being VECTOR of
for b1, b2, c1, c2 being Real st v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
proof end;

Lm13: for V being RealLinearSpace
for v, w, y being VECTOR of
for b1, b2, a being Real st v = (b1 * w) + (b2 * y) holds
a * v = ((a * b1) * w) + ((a * b2) * y)
proof end;

Lm14: for V being RealLinearSpace
for w, y being VECTOR of
for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
proof end;

definition
let V be RealLinearSpace;
let w, y, u be VECTOR of ;
assume A1: Gen w,y ;
func pr1 w,y,u -> Real means :Def4: :: GEOMTRAP:def 4
 ex b being Real st u = (it * w) + (b * y);
existence
ex b1, b being Real st u = (b1 * w) + (b * y) by A1, ANALMETR:def 1;
uniqueness
for b1, b2 being Real st ex b being Real st u = (b1 * w) + (b * y) & ex b being Real st u = (b2 * w) + (b * y) holds
b1 = b2 by A1, Lm14;
end;

:: deftheorem Def4 defines pr1 GEOMTRAP:def 4 :
for V being RealLinearSpace
for w, y, u being VECTOR of st Gen w,y holds
for b5 being Real holds
( b5 = pr1 w,y,u iff ex b being Real st u = (b5 * w) + (b * y) );

definition
let V be RealLinearSpace;
let w, y, u be VECTOR of ;
assume A1: Gen w,y ;
func pr2 w,y,u -> Real means :Def5: :: GEOMTRAP:def 5
 ex a being Real st u = (a * w) + (it * y);
existence
ex b1, a being Real st u = (a * w) + (b1 * y)
proof end;
uniqueness
for b1, b2 being Real st ex a being Real st u = (a * w) + (b1 * y) & ex a being Real st u = (a * w) + (b2 * y) holds
b1 = b2 by A1, Lm14;
end;

:: deftheorem Def5 defines pr2 GEOMTRAP:def 5 :
for V being RealLinearSpace
for w, y, u being VECTOR of st Gen w,y holds
for b5 being Real holds
( b5 = pr2 w,y,u iff ex a being Real st u = (a * w) + (b5 * y) );

Lm15: for V being RealLinearSpace
for w, y, u being VECTOR of st Gen w,y holds
u = ((pr1 w,y,u) * w) + ((pr2 w,y,u) * y)
proof end;

Lm16: for V being RealLinearSpace
for w, y, u being VECTOR of
for a, b being Real st Gen w,y & u = (a * w) + (b * y) holds
( a = pr1 w,y,u & b = pr2 w,y,u )
proof end;

Lm17: for V being RealLinearSpace
for w, y, u, v being VECTOR of
for a being Real st Gen w,y holds
( pr1 w,y,(u + v) = (pr1 w,y,u) + (pr1 w,y,v) & pr2 w,y,(u + v) = (pr2 w,y,u) + (pr2 w,y,v) & pr1 w,y,(u - v) = (pr1 w,y,u) - (pr1 w,y,v) & pr2 w,y,(u - v) = (pr2 w,y,u) - (pr2 w,y,v) & pr1 w,y,(a * u) = a * (pr1 w,y,u) & pr2 w,y,(a * u) = a * (pr2 w,y,u) )
proof end;

Lm18: for V being RealLinearSpace
for w, y, u, v being VECTOR of st Gen w,y holds
( 2 * (pr1 w,y,(u # v)) = (pr1 w,y,u) + (pr1 w,y,v) & 2 * (pr2 w,y,(u # v)) = (pr2 w,y,u) + (pr2 w,y,v) )
proof end;

Lm19: for V being RealLinearSpace
for u, v being VECTOR of holds (- u) + (- v) = - (u + v)
proof end;

Lm20: for V being RealLinearSpace
for u2, v, u1 being VECTOR of
for a2, a1 being Real holds (u2 + (a2 * v)) - (u1 + (a1 * v)) = (u2 - u1) + ((a2 - a1) * v)
proof end;

definition
let V be RealLinearSpace;
let w, y, u, v be VECTOR of ;
func PProJ w,y,u,v -> Real equals :: GEOMTRAP:def 6
((pr1 w,y,u) * (pr1 w,y,v)) + ((pr2 w,y,u) * (pr2 w,y,v));
correctness
coherence
((pr1 w,y,u) * (pr1 w,y,v)) + ((pr2 w,y,u) * (pr2 w,y,v)) is Real;
;
end;

:: deftheorem defines PProJ GEOMTRAP:def 6 :
for V being RealLinearSpace
for w, y, u, v being VECTOR of holds PProJ w,y,u,v = ((pr1 w,y,u) * (pr1 w,y,v)) + ((pr2 w,y,u) * (pr2 w,y,v));

theorem :: GEOMTRAP:31
for V being RealLinearSpace
for w, y, u, v being VECTOR of holds PProJ w,y,u,v = PProJ w,y,v,u ;

theorem Th32: :: GEOMTRAP:32
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, v, v1 being VECTOR of holds
( PProJ w,y,u,(v + v1) = (PProJ w,y,u,v) + (PProJ w,y,u,v1) & PProJ w,y,u,(v - v1) = (PProJ w,y,u,v) - (PProJ w,y,u,v1) & PProJ w,y,(v - v1),u = (PProJ w,y,v,u) - (PProJ w,y,v1,u) & PProJ w,y,(v + v1),u = (PProJ w,y,v,u) + (PProJ w,y,v1,u) )
proof end;

theorem Th33: :: GEOMTRAP:33
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, v being VECTOR of
for a being Real holds
( PProJ w,y,(a * u),v = a * (PProJ w,y,u,v) & PProJ w,y,u,(a * v) = a * (PProJ w,y,u,v) & PProJ w,y,(a * u),v = (PProJ w,y,u,v) * a & PProJ w,y,u,(a * v) = (PProJ w,y,u,v) * a )
proof end;

theorem Th34: :: GEOMTRAP:34
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, v being VECTOR of holds
( u,v are_Ort_wrt w,y iff PProJ w,y,u,v = 0 )
proof end;

theorem Th35: :: GEOMTRAP:35
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, v, u1, v1 being VECTOR of holds
( u,v,u1,v1 are_Ort_wrt w,y iff PProJ w,y,(v - u),(v1 - u1) = 0 )
proof end;

theorem Th36: :: GEOMTRAP:36
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, v, v1 being VECTOR of holds 2 * (PProJ w,y,u,(v # v1)) = (PProJ w,y,u,v) + (PProJ w,y,u,v1)
proof end;

theorem Th37: :: GEOMTRAP:37
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, v being VECTOR of st u <> v holds
PProJ w,y,(u - v),(u - v) <> 0
proof end;

theorem Th38: :: GEOMTRAP:38
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for p, q, u, v, v' being VECTOR of
for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v' = u + (A * (p - q)) holds
v = v'
proof end;

Lm21: for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, u', u1, u2, t1, t2 being VECTOR of
for A1, A2 being Real st A1 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) & A2 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " ) & t1 = u1 + (A1 * (u - u')) & t2 = u2 + (A2 * (u - u')) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) & A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) )
proof end;

theorem Th39: :: GEOMTRAP:39
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y & u1,u2 // v1,v2 holds
t1,t2 // w1,w2
proof end;

theorem :: GEOMTRAP:40
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, u', u1, u2, v1, t1, t2, w1 being VECTOR of st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & v1 = u1 # u2 holds
w1 = t1 # t2
proof end;

theorem Th41: :: GEOMTRAP:41
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, u', u1, u2, t1, t2 being VECTOR of st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y holds
u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y
proof end;

theorem Th42: :: GEOMTRAP:42
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
for u, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_Ort_wrt w,y holds
t1,t2,w1,w2 are_Ort_wrt w,y
proof end;

theorem Th43: :: GEOMTRAP:43
for V being RealLinearSpace
for w, y, u, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of st Gen w,y & u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_DTr_wrt w,y holds
t1,t2,w1,w2 are_DTr_wrt w,y
proof end;

definition
let V be RealLinearSpace;
let w, y be VECTOR of ;
func DTrapezium V,w,y -> Relation of means :Def7: :: GEOMTRAP:def 7
for x, z being set holds
( [x,z] in it iff ex u, u1, v, v1 being VECTOR of st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_DTr_wrt w,y ) );
existence
ex b1 being Relation of st
for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_DTr_wrt w,y ) )
proof end;
uniqueness
for b1, b2 being Relation of st ( for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_DTr_wrt w,y ) ) ) & ( for x, z being set holds
( [x,z] in b2 iff ex u, u1, v, v1 being VECTOR of st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_DTr_wrt w,y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines DTrapezium GEOMTRAP:def 7 :
for V being RealLinearSpace
for w, y being VECTOR of
for b4 being Relation of holds
( b4 = DTrapezium V,w,y iff for x, z being set holds
( [x,z] in b4 iff ex u, u1, v, v1 being VECTOR of st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_DTr_wrt w,y ) ) );

theorem Th44: :: GEOMTRAP:44
for V being RealLinearSpace
for u, v, u1, v1, w, y being VECTOR of holds
( [[u,v],[u1,v1]] in DTrapezium V,w,y iff u,v,u1,v1 are_DTr_wrt w,y )
proof end;

definition
let V be RealLinearSpace;
func MidPoint V -> BinOp of the carrier of V means :Def8: :: GEOMTRAP:def 8
for u, v being VECTOR of holds it . u,v = u # v;
existence
ex b1 being BinOp of the carrier of V st
for u, v being VECTOR of holds b1 . u,v = u # v
proof end;
uniqueness
for b1, b2 being BinOp of the carrier of V st ( for u, v being VECTOR of holds b1 . u,v = u # v ) & ( for u, v being VECTOR of holds b2 . u,v = u # v ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines MidPoint GEOMTRAP:def 8 :
for V being RealLinearSpace
for b2 being BinOp of the carrier of V holds
( b2 = MidPoint V iff for u, v being VECTOR of holds b2 . u,v = u # v );

definition
attr c1 is strict ;
struct AfMidStruct -> AffinStruct , MidStr ;
aggr AfMidStruct(# carrier, MIDPOINT, CONGR #) -> AfMidStruct ;
end;

registration
cluster non empty strict AfMidStruct ;
existence
ex b1 being AfMidStruct st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let V be RealLinearSpace;
let w, y be VECTOR of ;
func DTrSpace V,w,y -> strict AfMidStruct equals :: GEOMTRAP:def 9
 AfMidStruct(# the carrier of V,(MidPoint V),(DTrapezium V,w,y) #);
correctness
coherence
AfMidStruct(# the carrier of V,(MidPoint V),(DTrapezium V,w,y) #) is strict AfMidStruct ;
;
end;

:: deftheorem defines DTrSpace GEOMTRAP:def 9 :
for V being RealLinearSpace
for w, y being VECTOR of holds DTrSpace V,w,y = AfMidStruct(# the carrier of V,(MidPoint V),(DTrapezium V,w,y) #);

registration
let V be RealLinearSpace;
let w, y be VECTOR of ;
cluster DTrSpace V,w,y -> non empty strict ;
coherence
not DTrSpace V,w,y is empty ;
end;

definition
let AMS be AfMidStruct ;
func Af AMS -> strict AffinStruct equals :: GEOMTRAP:def 10
 AffinStruct(# the carrier of AMS,the CONGR of AMS #);
correctness
coherence
AffinStruct(# the carrier of AMS,the CONGR of AMS #) is strict AffinStruct ;
;
end;

:: deftheorem defines Af GEOMTRAP:def 10 :
for AMS being AfMidStruct holds Af AMS = AffinStruct(# the carrier of AMS,the CONGR of AMS #);

registration
let AMS be non empty AfMidStruct ;
cluster Af AMS -> non empty strict ;
coherence
not Af AMS is empty ;
end;

definition
let AMS be non empty AfMidStruct ;
let a, b be Element of ;
canceled;
func a # b -> Element of equals :: GEOMTRAP:def 12
the MIDPOINT of AMS . a,b;
correctness
coherence
the MIDPOINT of AMS . a,b is Element of ;
;
end;

:: deftheorem GEOMTRAP:def 11 :
canceled;

:: deftheorem defines # GEOMTRAP:def 12 :
for AMS being non empty AfMidStruct
for a, b being Element of holds a # b = the MIDPOINT of AMS . a,b;

theorem :: GEOMTRAP:45
canceled;

theorem :: GEOMTRAP:46
for V being RealLinearSpace
for w, y being VECTOR of
for x being set holds
( x is Element of the carrier of (DTrSpace V,w,y) iff x is VECTOR of ) ;

theorem Th47: :: GEOMTRAP:47
for V being RealLinearSpace
for u, v, u1, v1, w, y being VECTOR of
for a, b, a1, b1 being Element of st u = a & v = b & u1 = a1 & v1 = b1 holds
( a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y )
proof end;

theorem :: GEOMTRAP:48
for V being RealLinearSpace
for w, y, u, v being VECTOR of
for a, b being Element of st Gen w,y & u = a & v = b holds
u # v = a # b by Def8;

Lm22: for V being RealLinearSpace
for w, y being VECTOR of
for a, b, c being Element of st Gen w,y & a,b // b,c holds
( a = b & b = c )
proof end;

Lm23: for V being RealLinearSpace
for w, y being VECTOR of
for a, b, a1, b1, c1, d1 being Element of st Gen w,y & a,b // a1,b1 & a,b // c1,d1 & a <> b holds
a1,b1 // c1,d1
proof end;

Lm24: for V being RealLinearSpace
for w, y being VECTOR of
for a, b, c, d being Element of st a,b // c,d holds
( c,d // a,b & b,a // d,c )
proof end;

Lm25: for V being RealLinearSpace
for w, y being VECTOR of
for a, b, c being Element of st Gen w,y holds
ex d being Element of st
( a,b // c,d or a,b // d,c )
proof end;

Lm26: for V being RealLinearSpace
for w, y being VECTOR of
for a, b, c, d1, d2 being Element of st Gen w,y & a,b // c,d1 & a,b // c,d2 & not a = b holds
d1 = d2
proof end;

Lm27: for V being RealLinearSpace
for w, y being VECTOR of
for a, b being Element of holds a # b = b # a
proof end;

Lm28: for V being RealLinearSpace
for w, y being VECTOR of
for a being Element of holds a # a = a
proof end;

Lm29: for V being RealLinearSpace
for w, y being VECTOR of
for a, b, c, d being Element of holds (a # b) # (c # d) = (a # c) # (b # d)
proof end;

Lm30: for V being RealLinearSpace
for y, w being VECTOR of
for a, b being Element of ex p being Element of st p # a = b
proof end;

Lm31: for V being RealLinearSpace
for w, y being VECTOR of
for a, a1, a2 being Element of st a # a1 = a # a2 holds
a1 = a2
proof end;

Lm32: for V being RealLinearSpace
for w, y being VECTOR of
for a, b, c, d being Element of st Gen w,y & a,b // c,d holds
a,b // a # c,b # d
proof end;

Lm33: for V being RealLinearSpace
for w, y being VECTOR of
for a, b, c, d being Element of st Gen w,y & a,b // c,d & not a,b // a # d,b # c holds
a,b // b # c,a # d
proof end;

Lm34: for V being RealLinearSpace
for w, y being VECTOR of
for a, b, c, d, a1, p, b1, c1, d1 being Element of st a,b // c,d & a # a1 = p & b # b1 = p & c # c1 = p & d # d1 = p holds
a1,b1 // c1,d1
proof end;

Lm35: for V being RealLinearSpace
for w, y being VECTOR of
for p, q, a, a1, b, b1, c, c1, d, d1 being Element of st Gen w,y & p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d holds
a1,b1 // c1,d1
proof end;

definition
let IT be non empty AfMidStruct ;
attr IT is MidOrdTrapSpace-like means :Def13: :: GEOMTRAP:def 13
for a, b, c, d, a1, b1, c1, d1, p, q being Element of holds
( a # b = b # a & a # a = a & (a # b) # (c # d) = (a # c) # (b # d) & ex p being Element of st p # a = b & ( a # b = a # c implies b = c ) & ( a,b // c,d implies a,b // a # c,b # d ) & ( not a,b // c,d or a,b // a # d,b # c or a,b // b # c,a # d ) & ( a,b // c,d & a # a1 = p & b # b1 = p & c # c1 = p & d # d1 = p implies a1,b1 // c1,d1 ) & ( p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d implies a1,b1 // c1,d1 ) & ( a,b // b,c implies ( a = b & b = c ) ) & ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) & ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) );
end;

:: deftheorem Def13 defines MidOrdTrapSpace-like GEOMTRAP:def 13 :
for IT being non empty AfMidStruct holds
( IT is MidOrdTrapSpace-like iff for a, b, c, d, a1, b1, c1, d1, p, q being Element of holds
( a # b = b # a & a # a = a & (a # b) # (c # d) = (a # c) # (b # d) & ex p being Element of st p # a = b & ( a # b = a # c implies b = c ) & ( a,b // c,d implies a,b // a # c,b # d ) & ( not a,b // c,d or a,b // a # d,b # c or a,b // b # c,a # d ) & ( a,b // c,d & a # a1 = p & b # b1 = p & c # c1 = p & d # d1 = p implies a1,b1 // c1,d1 ) & ( p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d implies a1,b1 // c1,d1 ) & ( a,b // b,c implies ( a = b & b = c ) ) & ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) & ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) ) );

registration
cluster non empty strict MidOrdTrapSpace-like AfMidStruct ;
existence
ex b1 being non empty AfMidStruct st
( b1 is strict & b1 is MidOrdTrapSpace-like )
proof end;
end;

definition
mode MidOrdTrapSpace is non empty MidOrdTrapSpace-like AfMidStruct ;
end;

theorem :: GEOMTRAP:49
for V being RealLinearSpace
for w, y being VECTOR of st Gen w,y holds
DTrSpace V,w,y is MidOrdTrapSpace
proof end;

consider MOS being MidOrdTrapSpace;

set X = Af MOS;

Lm36: now
let a, b, c, d, a1, b1, c1, d1, p, q be Element of ; :: thesis: ( ( a,b // b,c implies ( a = b & b = c ) ) & ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) & ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) )
reconsider a' = a, b' = b, c' = c, d' = d, a1' = a1, b1' = b1, c1' = c1, d1' = d1, p' = p, q' = q as Element of ;
A1: now
let a, b, c, d be Element of ; :: thesis: for a', b', c', d' being Element of the carrier of MOS st a = a' & b = b' & c = c' & d = d' holds
( a,b // c,d iff a',b' // c',d' )
let a', b', c', d' be Element of the carrier of MOS; :: thesis: ( a = a' & b = b' & c = c' & d = d' implies ( a,b // c,d iff a',b' // c',d' ) )
assume A2: ( a = a' & b = b' & c = c' & d = d' ) ; :: thesis: ( a,b // c,d iff a',b' // c',d' )
A3: now
assume a',b' // c',d' ; :: thesis: a,b // c,d
then [[a,b],[c,d]] in the CONGR of MOS by A2, ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2; :: thesis: verum
end;
now
assume a,b // c,d ; :: thesis: a',b' // c',d'
then [[a,b],[c,d]] in the CONGR of MOS by ANALOAF:def 2;
hence a',b' // c',d' by A2, ANALOAF:def 2; :: thesis: verum
end;
hence ( a,b // c,d iff a',b' // c',d' ) by A3; :: thesis: verum
end;
hereby :: thesis: ( ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) & ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) )
assume a,b // b,c ; :: thesis: ( a = b & b = c )
then a',b' // b',c' by A1;
hence ( a = b & b = c ) by Def13; :: thesis: verum
end;
hereby :: thesis: ( ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) )
assume that
A4: ( a,b // a1,b1 & a,b // c1,d1 ) and
A5: a <> b ; :: thesis: a1,b1 // c1,d1
( a',b' // a1',b1' & a',b' // c1',d1' ) by A1, A4;
then a1',b1' // c1',d1' by A5, Def13;
hence a1,b1 // c1,d1 by A1; :: thesis: verum
end;
hereby :: thesis: ( ex d being Element of st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) )
assume a,b // c,d ; :: thesis: ( c,d // a,b & b,a // d,c )
then a',b' // c',d' by A1;
then ( c',d' // a',b' & b',a' // d',c' ) by Def13;
hence ( c,d // a,b & b,a // d,c ) by A1; :: thesis: verum
end;
thus ex d being Element of st
( a,b // c,d or a,b // d,c ) :: thesis: ( a,b // c,p & a,b // c,q & not a = b implies p = q )
proof
consider x' being Element of such that
A6: ( a',b' // c',x' or a',b' // x',c' ) by Def13;
reconsider x = x' as Element of ;
take x ; :: thesis: ( a,b // c,x or a,b // x,c )
thus ( a,b // c,x or a,b // x,c ) by A1, A6; :: thesis: verum
end;
assume ( a,b // c,p & a,b // c,q ) ; :: thesis: ( a = b or p = q )
then ( a',b' // c',p' & a',b' // c',q' ) by A1;
hence ( a = b or p = q ) by Def13; :: thesis: verum
end;

definition
let IT be non empty AffinStruct ;
attr IT is OrdTrapSpace-like means :Def14: :: GEOMTRAP:def 14
for a, b, c, d, a1, b1, c1, d1, p, q being Element of holds
( ( a,b // b,c implies ( a = b & b = c ) ) & ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) & ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) );
end;

:: deftheorem Def14 defines OrdTrapSpace-like GEOMTRAP:def 14 :
for IT being non empty AffinStruct holds
( IT is OrdTrapSpace-like iff for a, b, c, d, a1, b1, c1, d1, p, q being Element of holds
( ( a,b // b,c implies ( a = b & b = c ) ) & ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) & ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) ) );

registration
cluster non empty strict OrdTrapSpace-like AffinStruct ;
existence
ex b1 being non empty AffinStruct st
( b1 is strict & b1 is OrdTrapSpace-like )
proof end;
end;

definition
mode OrdTrapSpace is non empty OrdTrapSpace-like AffinStruct ;
end;

registration
let MOS be MidOrdTrapSpace;
cluster Af MOS -> strict OrdTrapSpace-like ;
coherence
Af MOS is OrdTrapSpace-like
proof end;
end;

theorem Th50: :: GEOMTRAP:50
for OTS being OrdTrapSpace
for x being set holds
( x is Element of iff x is Element of )
proof end;

theorem Th51: :: GEOMTRAP:51
for OTS being OrdTrapSpace
for a, b, c, d being Element of
for a', b', c', d' being Element of st a = a' & b = b' & c = c' & d = d' holds
( a',b' // c',d' iff ( a,b // c,d or a,b // d,c ) )
proof end;

Lm37: for OTS being OrdTrapSpace
for a', b', c' being Element of ex d' being Element of st a',b' // c',d'
proof end;

Lm38: for OTS being OrdTrapSpace
for a', b', c', d' being Element of st a',b' // c',d' holds
c',d' // a',b'
proof end;

Lm39: for OTS being OrdTrapSpace
for a1', b1', a', b', c', d' being Element of st a1' <> b1' & a1',b1' // a',b' & a1',b1' // c',d' holds
a',b' // c',d'
proof end;

Lm40: for OTS being OrdTrapSpace
for a', b', c', d', d1' being Element of st a',b' // c',d' & a',b' // c',d1' & not a' = b' holds
d' = d1'
proof end;

Lm41: for OTS being OrdTrapSpace
for a, b being Element of holds a,b // a,b
proof end;

Lm42: for OTS being OrdTrapSpace
for a', b' being Element of holds a',b' // b',a'
proof end;

definition
let IT be non empty AffinStruct ;
attr IT is TrapSpace-like means :: GEOMTRAP:def 15
for a', b', c', d', p', q' being Element of holds
( a',b' // b',a' & ( a',b' // c',d' & a',b' // c',q' & not a' = b' implies d' = q' ) & ( p' <> q' & p',q' // a',b' & p',q' // c',d' implies a',b' // c',d' ) & ( a',b' // c',d' implies c',d' // a',b' ) & ex x' being Element of st a',b' // c',x' );
end;

:: deftheorem defines TrapSpace-like GEOMTRAP:def 15 :
for IT being non empty AffinStruct holds
( IT is TrapSpace-like iff for a', b', c', d', p', q' being Element of holds
( a',b' // b',a' & ( a',b' // c',d' & a',b' // c',q' & not a' = b' implies d' = q' ) & ( p' <> q' & p',q' // a',b' & p',q' // c',d' implies a',b' // c',d' ) & ( a',b' // c',d' implies c',d' // a',b' ) & ex x' being Element of st a',b' // c',x' ) );

Lm43: for OTS being OrdTrapSpace holds Lambda OTS is TrapSpace-like
proof end;

registration
cluster non empty strict TrapSpace-like AffinStruct ;
existence
ex b1 being non empty AffinStruct st
( b1 is strict & b1 is TrapSpace-like )
proof end;
end;

definition
mode TrapSpace is non empty TrapSpace-like AffinStruct ;
end;

registration
let OTS be OrdTrapSpace;
cluster Lambda OTS -> TrapSpace-like ;
correctness
coherence
Lambda OTS is TrapSpace-like ;
by Lm43;
end;

definition
let IT be non empty AffinStruct ;
attr IT is Regular means :Def16: :: GEOMTRAP:def 16
for p, q, a, a1, b, b1, c, c1, d, d1 being Element of st p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d holds
a1,b1 // c1,d1;
end;

:: deftheorem Def16 defines Regular GEOMTRAP:def 16 :
for IT being non empty AffinStruct holds
( IT is Regular iff for p, q, a, a1, b, b1, c, c1, d, d1 being Element of st p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d holds
a1,b1 // c1,d1 );

registration
cluster non empty strict Regular AffinStruct ;
existence
ex b1 being non empty OrdTrapSpace st
( b1 is strict & b1 is Regular )
proof end;
end;

registration
let MOS be MidOrdTrapSpace;
cluster Af MOS -> strict Regular ;
correctness
coherence
Af MOS is Regular ;
proof end;
end;