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


begin

definition
let V be RealLinearSpace;
let u, v, u1, v1 be VECTOR of V;
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 V 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 V 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 V
for p, q, p1, q1 being Element of (OASpace V) 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 V 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 V
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 V;
func u # v -> VECTOR of V means :Def2: :: GEOMTRAP:def 2
it + it = u + v;
existence
ex b1 being VECTOR of V st b1 + b1 = u + v
proof end;
uniqueness
for b1, b2 being VECTOR of V st b1 + b1 = u + v & b2 + b2 = u + v holds
b1 = b2
proof end;
commutativity
for b1, u, v being VECTOR of V st b1 + b1 = u + v holds
b1 + b1 = v + u ;
idempotence
for u being VECTOR of V holds u + u = u + u ;
end;

:: deftheorem Def2 defines # GEOMTRAP:def 2 :
for V being RealLinearSpace
for u, v, b4 being VECTOR of V 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 V ex y being VECTOR of V st u # y = w
proof end;

theorem Th8: :: GEOMTRAP:8
for V being RealLinearSpace
for u, u1, v, v1 being VECTOR of V 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 V 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 V holds u,v // y # u,y # v
proof end;

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

theorem Th12: :: GEOMTRAP:12
for V being RealLinearSpace
for u, v being VECTOR of V 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 V holds u,u # v // u # v,v
proof end;

theorem Th14: :: GEOMTRAP:14
for V being RealLinearSpace
for u, v being VECTOR of V 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 V 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 V 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 V 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 V 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 V 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 V 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 V 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 V 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 V 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 V 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 V 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 V 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 V;
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 V 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 V 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 V 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 V 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 V 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 V 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 V st Gen w,y holds
ex t being VECTOR of V 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 V 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 V 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 V 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 V 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 V 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 V 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 V 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 V 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 V 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 V
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 V
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 V
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 V;
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 V 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 V;
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 V 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 V 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 V
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 V
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 V 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 V holds (- u) + (- v) = - (u + v)
proof end;

Lm20: for V being RealLinearSpace
for u2, v, u1 being VECTOR of V
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 V;
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 V 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 V 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 V st Gen w,y holds
for u, v, v1 being VECTOR of V 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 V st Gen w,y holds
for u, v being VECTOR of V
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 V st Gen w,y holds
for u, v being VECTOR of V 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 V st Gen w,y holds
for u, v, u1, v1 being VECTOR of V 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 V st Gen w,y holds
for u, v, v1 being VECTOR of V 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 V st Gen w,y holds
for u, v being VECTOR of V 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 V st Gen w,y holds
for p, q, u, v, v9 being VECTOR of V
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))) ") & v9 = u + (A * (p - q)) holds
v = v9
proof end;

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

theorem Th39: :: GEOMTRAP:39
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, u9, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & u,u9,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 V st Gen w,y holds
for u, u9, u1, u2, v1, t1, t2, w1 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,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 V st Gen w,y holds
for u, u9, u1, u2, t1, t2 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y holds
u,u9,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 V st Gen w,y holds
for u, u9, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & u,u9,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, u9, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st Gen w,y & u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & u,u9,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 V;
func DTrapezium (V,w,y) -> Relation of [: the carrier of V, the carrier of V:] means :Def7: :: GEOMTRAP:def 7
 for x, z being set holds
( [x,z] in it iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_DTr_wrt w,y ) );
existence
ex b1 being Relation of [: the carrier of V, the carrier of V:] st
for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of V 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 [: the carrier of V, the carrier of V:] st ( for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of V 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 V 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 V
for b4 being Relation of [: the carrier of V, the carrier of V:] 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 V 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 V 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 V holds it . (u,v) = u # v;
existence
ex b1 being BinOp of the carrier of V st
for u, v being VECTOR of V 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 V holds b1 . (u,v) = u # v ) & ( for u, v being VECTOR of V 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 V 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 V;
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 V 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 V;
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 AMS;
canceled;
func a # b -> Element of AMS equals :: GEOMTRAP:def 12
 the MIDPOINT of AMS . (a,b);
correctness
coherence
the MIDPOINT of AMS . (a,b) is Element of AMS;
;
end;

:: deftheorem GEOMTRAP:def 11 :
canceled;

:: deftheorem defines # GEOMTRAP:def 12 :
for AMS being non empty AfMidStruct
for a, b being Element of AMS 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 V
for x being set holds
( x is Element of the carrier of (DTrSpace (V,w,y)) iff x is VECTOR of V ) ;

theorem Th47: :: GEOMTRAP:47
for V being RealLinearSpace
for u, v, u1, v1, w, y being VECTOR of V
for a, b, a1, b1 being Element of (DTrSpace (V,w,y)) 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 V
for a, b being Element of (DTrSpace (V,w,y)) 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 V
for a, b, c being Element of (DTrSpace (V,w,y)) 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 V
for a, b, a1, b1, c1, d1 being Element of (DTrSpace (V,w,y)) 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 V
for a, b, c, d being Element of (DTrSpace (V,w,y)) 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 V
for a, b, c being Element of (DTrSpace (V,w,y)) st Gen w,y holds
ex d being Element of (DTrSpace (V,w,y)) st
( a,b // c,d or a,b // d,c )
proof end;

Lm26: for V being RealLinearSpace
for w, y being VECTOR of V
for a, b, c, d1, d2 being Element of (DTrSpace (V,w,y)) 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 V
for a, b being Element of (DTrSpace (V,w,y)) holds a # b = b # a
proof end;

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

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

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

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

Lm32: for V being RealLinearSpace
for w, y being VECTOR of V
for a, b, c, d being Element of (DTrSpace (V,w,y)) 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 V
for a, b, c, d being Element of (DTrSpace (V,w,y)) 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 V
for a, b, c, d, a1, p, b1, c1, d1 being Element of (DTrSpace (V,w,y)) 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 V
for p, q, a, a1, b, b1, c, c1, d, d1 being Element of (DTrSpace (V,w,y)) 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 IT holds
( a # b = b # a & a # a = a & (a # b) # (c # d) = (a # c) # (b # d) & ex p being Element of IT 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 IT 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 IT holds
( a # b = b # a & a # a = a & (a # b) # (c # d) = (a # c) # (b # d) & ex p being Element of IT 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 IT 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 V st Gen w,y holds
DTrSpace (V,w,y) is MidOrdTrapSpace
proof end;

set MOS = the MidOrdTrapSpace;

set X = Af the MidOrdTrapSpace;

Lm36: now
let a, b, c, d, a1, b1, c1, d1, p, q be Element of (Af the MidOrdTrapSpace); :: 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 (Af the MidOrdTrapSpace) 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 a9 = a, b9 = b, c9 = c, d9 = d, a19 = a1, b19 = b1, c19 = c1, d19 = d1, p9 = p, q9 = q as Element of the MidOrdTrapSpace ;
A1: now
let a, b, c, d be Element of (Af the MidOrdTrapSpace); :: thesis: for a9, b9, c9, d9 being Element of the carrier of the MidOrdTrapSpace st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b // c,d iff a9,b9 // c9,d9 )
let a9, b9, c9, d9 be Element of the carrier of the MidOrdTrapSpace; :: thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a,b // c,d iff a9,b9 // c9,d9 ) )
assume A2: ( a = a9 & b = b9 & c = c9 & d = d9 ) ; :: thesis: ( a,b // c,d iff a9,b9 // c9,d9 )
A3: now
assume a9,b9 // c9,d9 ; :: thesis: a,b // c,d
then [[a,b],[c,d]] in the CONGR of the MidOrdTrapSpace by A2, ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2; :: thesis: verum
end;
now
assume a,b // c,d ; :: thesis: a9,b9 // c9,d9
then [[a,b],[c,d]] in the CONGR of the MidOrdTrapSpace by ANALOAF:def 2;
hence a9,b9 // c9,d9 by A2, ANALOAF:def 2; :: thesis: verum
end;
hence ( a,b // c,d iff a9,b9 // c9,d9 ) 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 (Af the MidOrdTrapSpace) 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 a9,b9 // b9,c9 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 (Af the MidOrdTrapSpace) 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
( a9,b9 // a19,b19 & a9,b9 // c19,d19 ) by A1, A4;
then a19,b19 // c19,d19 by A5, Def13;
hence a1,b1 // c1,d1 by A1; :: thesis: verum
end;
hereby :: thesis: ( ex d being Element of (Af the MidOrdTrapSpace) 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 a9,b9 // c9,d9 by A1;
then ( c9,d9 // a9,b9 & b9,a9 // d9,c9 ) by Def13;
hence ( c,d // a,b & b,a // d,c ) by A1; :: thesis: verum
end;
thus ex d being Element of (Af the MidOrdTrapSpace) 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 x9 being Element of the MidOrdTrapSpace such that
A6: ( a9,b9 // c9,x9 or a9,b9 // x9,c9 ) by Def13;
reconsider x = x9 as Element of (Af the MidOrdTrapSpace) ;
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 ( a9,b9 // c9,p9 & a9,b9 // c9,q9 ) 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 IT 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 IT 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 IT 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 IT 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 OTS iff x is Element of (Lambda OTS) )
proof end;

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

Lm37: for OTS being OrdTrapSpace
for a9, b9, c9 being Element of (Lambda OTS) ex d9 being Element of (Lambda OTS) st a9,b9 // c9,d9
proof end;

Lm38: for OTS being OrdTrapSpace
for a9, b9, c9, d9 being Element of (Lambda OTS) st a9,b9 // c9,d9 holds
c9,d9 // a9,b9
proof end;

Lm39: for OTS being OrdTrapSpace
for a19, b19, a9, b9, c9, d9 being Element of (Lambda OTS) st a19 <> b19 & a19,b19 // a9,b9 & a19,b19 // c9,d9 holds
a9,b9 // c9,d9
proof end;

Lm40: for OTS being OrdTrapSpace
for a9, b9, c9, d9, d19 being Element of (Lambda OTS) st a9,b9 // c9,d9 & a9,b9 // c9,d19 & not a9 = b9 holds
d9 = d19
proof end;

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

Lm42: for OTS being OrdTrapSpace
for a9, b9 being Element of (Lambda OTS) holds a9,b9 // b9,a9
proof end;

definition
let IT be non empty AffinStruct ;
attr IT is TrapSpace-like means :: GEOMTRAP:def 15
 for a9, b9, c9, d9, p9, q9 being Element of IT holds
( a9,b9 // b9,a9 & ( a9,b9 // c9,d9 & a9,b9 // c9,q9 & not a9 = b9 implies d9 = q9 ) & ( p9 <> q9 & p9,q9 // a9,b9 & p9,q9 // c9,d9 implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies c9,d9 // a9,b9 ) & ex x9 being Element of IT st a9,b9 // c9,x9 );
end;

:: deftheorem defines TrapSpace-like GEOMTRAP:def 15 :
for IT being non empty AffinStruct holds
( IT is TrapSpace-like iff for a9, b9, c9, d9, p9, q9 being Element of IT holds
( a9,b9 // b9,a9 & ( a9,b9 // c9,d9 & a9,b9 // c9,q9 & not a9 = b9 implies d9 = q9 ) & ( p9 <> q9 & p9,q9 // a9,b9 & p9,q9 // c9,d9 implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies c9,d9 // a9,b9 ) & ex x9 being Element of IT st a9,b9 // c9,x9 ) );

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 IT 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 IT 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 OrdTrapSpace-like 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;