begin
theorem Th2:
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 )
theorem Th3:
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 )
theorem Th4:
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 )
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 )
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
Lm3:
for V being RealLinearSpace
for u1, u2, v1, v2 being VECTOR of V st u1 # u2 = v1 # v2 holds
v1 - u1 = - (v2 - u2)
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
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
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
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
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
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 )
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 )
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:
(
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 Th19:
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
theorem Th20:
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 )
theorem Th21:
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
theorem Th22:
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
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
theorem Th24:
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
theorem Th25:
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
theorem Th26:
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
theorem Th27:
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
theorem Th28:
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
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) )
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)
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 )
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)
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) )
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)) )
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)) )
Lm19:
for V being RealLinearSpace
for u, v being VECTOR of V holds (- u) + (- v) = - (u + v)
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)
definition
let V be
RealLinearSpace;
let w,
y,
u,
v be
VECTOR of
V;
func PProJ (
w,
y,
u,
v)
-> Real equals
((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 Th30:
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)) )
theorem Th31:
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 )
theorem Th33:
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 )
theorem Th34:
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))
theorem Th36:
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
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))) ") )
theorem Th37:
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
theorem
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
theorem Th39:
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
theorem Th40:
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
theorem Th41:
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
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:
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 ) )
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
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:
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 )
theorem Th44:
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 )
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 )
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
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 )
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 )
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
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
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
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)
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
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
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
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
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
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
definition
let IT be non
empty AfMidStruct ;
attr IT is
MidOrdTrapSpace-like means :
Def12:
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 ) ) );
set MOS = the MidOrdTrapSpace;
set X = Af the MidOrdTrapSpace;
Lm36:
now 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);
( ( 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 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);
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;
( 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 )
;
( a,b // c,d iff a9,b9 // c9,d9 )
A3:
now ( a9,b9 // c9,d9 implies a,b // c,d )
assume
a9,
b9 // c9,
d9
;
a,b // c,dthen
[[a,b],[c,d]] in the
CONGR of the
MidOrdTrapSpace
by A2, ANALOAF:def 2;
hence
a,
b // c,
d
by ANALOAF:def 2;
verum
end;
now ( a,b // c,d implies a9,b9 // c9,d9 )
assume
a,
b // c,
d
;
a9,b9 // c9,d9then
[[a,b],[c,d]] in the
CONGR of the
MidOrdTrapSpace
by ANALOAF:def 2;
hence
a9,
b9 // c9,
d9
by A2, ANALOAF:def 2;
verum
end;
hence
(
a,
b // c,
d iff
a9,
b9 // c9,
d9 )
by A3;
verum
end;
hereby ( ( 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
;
( a = b & b = c )then
a9,
b9 // b9,
c9
by A1;
hence
(
a = b &
b = c )
by Def12;
verum
end;
hereby ( ( 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
;
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;
verum
end;
hereby ( 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
;
( 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;
verum
end;
thus
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 )
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
;
( a,b // c,x or a,b // x,c )
thus
(
a,
b // c,
x or
a,
b // x,
c )
by A1, A6;
verum
end;
assume
(
a,
b // c,
p &
a,
b // c,
q )
;
( a = b or p = q )then
(
a9,
b9 // c9,
p9 &
a9,
b9 // c9,
q9 )
by A1;
hence
(
a = b or
p = q )
by Def12;
verum
end;
definition
let IT be non
empty AffinStruct ;
attr IT is
OrdTrapSpace-like means :
Def13:
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 ) ) );
theorem Th48:
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 ) )
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
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
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
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
Lm41:
for OTS being OrdTrapSpace
for a, b being Element of OTS holds a,b // a,b
Lm42:
for OTS being OrdTrapSpace
for a9, b9 being Element of (Lambda OTS) holds a9,b9 // b9,a9
definition
let IT be non
empty AffinStruct ;
attr IT is
TrapSpace-like means
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
definition
let IT be non
empty AffinStruct ;
attr IT is
Regular means :
Def15:
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 );