:: A Construction of Analytical Ordered Trapezium Spaces :: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received October 29, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let V be RealLinearSpace; let u, v, u1, v1 be VECTOR of V; predu,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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; definition let V be RealLinearSpace; let u, v be VECTOR of V; funcu # 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 proofend; uniqueness for b1, b2 being VECTOR of V st b1 + b1 = u + v & b2 + b2 = u + v holds b1 = b2 proofend; 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 Th5: :: GEOMTRAP:5 for V being RealLinearSpace for u, w being VECTOR of V ex y being VECTOR of V st u # y = w proofend; theorem Th6: :: GEOMTRAP:6 for V being RealLinearSpace for u, u1, v, v1 being VECTOR of V holds (u # u1) # (v # v1) = (u # v) # (u1 # v1) proofend; theorem Th7: :: GEOMTRAP:7 for V being RealLinearSpace for u, y, w being VECTOR of V st u # y = u # w holds y = w proofend; theorem Th8: :: GEOMTRAP:8 for V being RealLinearSpace for u, v, y being VECTOR of V holds u,v // y # u,y # v proofend; theorem :: GEOMTRAP:9 for V being RealLinearSpace for u, v, w being VECTOR of V holds u,v '||' w # u,w # v proofend; theorem Th10: :: GEOMTRAP:10 for V being RealLinearSpace for u, v being VECTOR of V holds ( 2 * ((u # v) - u) = v - u & 2 * (v - (u # v)) = v - u ) proofend; theorem Th11: :: GEOMTRAP:11 for V being RealLinearSpace for u, v being VECTOR of V holds u,u # v // u # v,v proofend; theorem Th12: :: GEOMTRAP:12 for V being RealLinearSpace for u, v being VECTOR of V holds ( u,v // u,u # v & u,v // u # v,v ) proofend; 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 ) proofend; theorem Th13: :: GEOMTRAP:13 for V being RealLinearSpace for u, y, v being VECTOR of V st u,y // y,v holds u # y,y // y,y # v proofend; theorem Th14: :: GEOMTRAP:14 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 proofend; 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 proofend; Lm3: for V being RealLinearSpace for u1, u2, v1, v2 being VECTOR of V st u1 # u2 = v1 # v2 holds v1 - u1 = - (v2 - u2) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; definition let V be RealLinearSpace; let w, y, u, u1, v, v1 be VECTOR of V; predu,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:15 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 proofend; theorem :: GEOMTRAP:16 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 proofend; theorem Th17: :: GEOMTRAP:17 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 proofend; theorem Th18: :: GEOMTRAP:18 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 ) proofend; theorem Th19: :: GEOMTRAP:19 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 proofend; theorem Th20: :: GEOMTRAP:20 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 ) proofend; theorem Th21: :: GEOMTRAP:21 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 proofend; theorem Th22: :: GEOMTRAP:22 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 proofend; 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 proofend; theorem Th23: :: GEOMTRAP:23 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 proofend; theorem Th24: :: GEOMTRAP:24 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 proofend; theorem Th25: :: GEOMTRAP:25 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 proofend; theorem Th26: :: GEOMTRAP:26 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 proofend; theorem Th27: :: GEOMTRAP:27 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 proofend; theorem Th28: :: GEOMTRAP:28 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 proofend; 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) ) proofend; 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) proofend; 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 ) proofend; 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 B1: 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) proofend; 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 B1, 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) proofend; 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) ) proofend; 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)) ) proofend; 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)) ) proofend; Lm19: for V being RealLinearSpace for u, v being VECTOR of V holds (- u) + (- v) = - (u + v) proofend; 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) proofend; 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:29 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 Th30: :: GEOMTRAP:30 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)) ) proofend; theorem Th31: :: GEOMTRAP:31 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 ) proofend; theorem Th32: :: GEOMTRAP:32 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 ) proofend; theorem Th33: :: GEOMTRAP:33 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 ) proofend; theorem Th34: :: GEOMTRAP:34 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)) proofend; theorem Th35: :: GEOMTRAP:35 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 proofend; theorem Th36: :: GEOMTRAP:36 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 proofend; 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))) ") ) proofend; theorem Th37: :: GEOMTRAP:37 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 proofend; theorem :: GEOMTRAP:38 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 proofend; 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, 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 proofend; theorem Th40: :: GEOMTRAP:40 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 proofend; theorem Th41: :: GEOMTRAP:41 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 proofend; 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 ) ) proofend; 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 proofend; 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 Th42: :: GEOMTRAP:42 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 ) proofend; 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 proofend; 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 proofend; 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 attrc1 is strict ; struct AfMidStruct -> AffinStruct , MidStr ; aggrAfMidStruct(# carrier, MIDPOINT, CONGR #) -> AfMidStruct ; end; registration cluster non empty strict for AfMidStruct ; existence ex b1 being AfMidStruct st ( not b1 is empty & b1 is strict ) proofend; 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; funca # b -> Element of AMS equals :: GEOMTRAP:def 11 the MIDPOINT of AMS . (a,b); correctness coherence the MIDPOINT of AMS . (a,b) is Element of AMS; ; end; :: deftheorem defines # GEOMTRAP:def_11_:_ for AMS being non empty AfMidStruct for a, b being Element of AMS holds a # b = the MIDPOINT of AMS . (a,b); theorem :: GEOMTRAP:43 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 Th44: :: GEOMTRAP:44 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 ) proofend; theorem :: GEOMTRAP:45 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 ) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; definition let IT be non empty AfMidStruct ; attrIT is MidOrdTrapSpace-like means :Def12: :: GEOMTRAP:def 12 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 Def12 defines MidOrdTrapSpace-like GEOMTRAP:def_12_:_ 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 for AfMidStruct ; existence ex b1 being non empty AfMidStruct st ( b1 is strict & b1 is MidOrdTrapSpace-like ) proofend; end; definition mode MidOrdTrapSpace is non empty MidOrdTrapSpace-like AfMidStruct ; end; theorem :: GEOMTRAP:46 for V being RealLinearSpace for w, y being VECTOR of V st Gen w,y holds DTrSpace (V,w,y) is MidOrdTrapSpace proofend; set MOS = the MidOrdTrapSpace; set X = Af the MidOrdTrapSpace; Lm36: now__::_thesis:_for_a,_b,_c,_d,_a1,_b1,_c1,_d1,_p,_q_being_Element_of_(Af_the_MidOrdTrapSpace)_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_(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_)_) 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__::_thesis:_for_a,_b,_c,_d_being_Element_of_(Af_the_MidOrdTrapSpace) 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 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__::_thesis:_(_a9,b9_//_c9,d9_implies_a,b_//_c,d_) 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__::_thesis:_(_a,b_//_c,d_implies_a9,b9_//_c9,d9_) 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 Def12; ::_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, Def12; 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 Def12; 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 Def12; 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 Def12; ::_thesis: verum end; definition let IT be non empty AffinStruct ; attrIT is OrdTrapSpace-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,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 OrdTrapSpace-like GEOMTRAP:def_13_:_ 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 for AffinStruct ; existence ex b1 being non empty AffinStruct st ( b1 is strict & b1 is OrdTrapSpace-like ) proofend; 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 proofend; end; theorem Th47: :: GEOMTRAP:47 for OTS being OrdTrapSpace for x being set holds ( x is Element of OTS iff x is Element of (Lambda OTS) ) proofend; theorem Th48: :: GEOMTRAP:48 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 ) ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; Lm41: for OTS being OrdTrapSpace for a, b being Element of OTS holds a,b // a,b proofend; Lm42: for OTS being OrdTrapSpace for a9, b9 being Element of (Lambda OTS) holds a9,b9 // b9,a9 proofend; definition let IT be non empty AffinStruct ; attrIT is TrapSpace-like means :: GEOMTRAP:def 14 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_14_:_ 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 proofend; registration cluster non empty strict TrapSpace-like for AffinStruct ; existence ex b1 being non empty AffinStruct st ( b1 is strict & b1 is TrapSpace-like ) proofend; 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 ; attrIT is Regular means :Def15: :: GEOMTRAP:def 15 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 Def15 defines Regular GEOMTRAP:def_15_:_ 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 for AffinStruct ; existence ex b1 being OrdTrapSpace st ( b1 is strict & b1 is Regular ) proofend; end; registration let MOS be MidOrdTrapSpace; cluster Af MOS -> strict Regular ; correctness coherence Af MOS is Regular ; proofend; end;