:: 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 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, v' 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)) " ) & v' = u + (A * (p - q)) holds
v = v'
proof end;

Lm21: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, u', u1, u2, t1, t2 being VECTOR of V
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 V st Gen w,y holds
for u, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V 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 V st Gen w,y holds
for u, u', u1, u2, v1, t1, t2, w1 being VECTOR of V 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 V st Gen w,y holds
for u, u', u1, u2, t1, t2 being VECTOR of V 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 V st Gen w,y holds
for u, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V 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 V 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 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;

consider MOS being MidOrdTrapSpace;

set X = Af MOS;

Lm36: now
let a, b, c, d, a1, b1, c1, d1, p, q be Element of (Af MOS); :: 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 MOS) 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 MOS ;
A1: now
let a, b, c, d be Element of (Af MOS); :: 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 (Af MOS) 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 (Af MOS) 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 (Af MOS) 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 (Af MOS) 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 MOS such that
A6: ( a',b' // c',x' or a',b' // x',c' ) by Def13;
reconsider x = x' as Element of (Af MOS) ;
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 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 a', b', c', d' being Element of (Lambda OTS) 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 (Lambda OTS) ex d' being Element of (Lambda OTS) st a',b' // c',d'
proof end;

Lm38: for OTS being OrdTrapSpace
for a', b', c', d' being Element of (Lambda OTS) 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 (Lambda OTS) 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 (Lambda OTS) 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 OTS holds a,b // a,b
proof end;

Lm42: for OTS being OrdTrapSpace
for a', b' being Element of (Lambda OTS) 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 IT 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 IT 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 IT 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 IT 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 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 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;