Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Analytical Metric Affine Spaces and Planes

by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

MML identifier: ANALMETR
[ Mizar article, MML identifier index ]

```environ

vocabulary RLVECT_1, ARYTM_1, RELAT_1, ANALOAF, DIRAF, SYMSP_1, REALSET1,
INCSP_1, AFF_1, ANALMETR;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, DOMAIN_1, REAL_1,
STRUCT_0, DIRAF, RELSET_1, RLVECT_1, AFF_1, ANALOAF, REALSET1;
constructors DOMAIN_1, REAL_1, AFF_1, XREAL_0, MEMBERED, XBOOLE_0;
clusters DIRAF, ANALOAF, RELSET_1, STRUCT_0, SUBSET_1, XREAL_0, MEMBERED,
ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve V for RealLinearSpace;
reserve u,u1,u2,v,v1,v2,w,w1,y for VECTOR of V;
reserve a,a1,a2,b,b1,b2,c1,c2 for Real;
reserve x,z for set;

definition let V; let w,y;
pred Gen w,y means
:: ANALMETR:def 1
(for u ex a1,a2 st u = a1*w + a2*y) &
(for a1,a2 st a1*w + a2*y = 0.V holds a1=0 & a2=0);
end;

definition let V; let u,v,w,y;
pred u,v are_Ort_wrt w,y means
:: ANALMETR:def 2
ex a1,a2,b1,b2 st (u = a1*w + a2*y & v = b1*w + b2*y &
a1*b1 + a2*b2 = 0);
end;

canceled 4;

theorem :: ANALMETR:5
for w,y st Gen w,y holds (u,v are_Ort_wrt w,y iff
(for a1,a2,b1,b2 st u = a1*w + a2*y & v = b1*w + b2*y
holds a1*b1 + a2*b2 = 0));

theorem :: ANALMETR:6
w,y are_Ort_wrt w,y;

theorem :: ANALMETR:7
ex V st ex w,y st Gen w,y;

theorem :: ANALMETR:8
u,v are_Ort_wrt w,y implies v,u are_Ort_wrt w,y;

theorem :: ANALMETR:9
Gen w,y implies (for u,v holds
u,0.V are_Ort_wrt w,y & 0.V,v are_Ort_wrt w,y);

theorem :: ANALMETR:10
u,v are_Ort_wrt w,y implies a*u,b*v are_Ort_wrt w,y;

theorem :: ANALMETR:11
u,v are_Ort_wrt w,y implies
a*u,v are_Ort_wrt w,y & u,b*v are_Ort_wrt w,y;

theorem :: ANALMETR:12
Gen w,y implies
(for u ex v st (u,v are_Ort_wrt w,y & v<>0.V));

theorem :: ANALMETR:13
Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v<>0.V
implies ( ex a,b st a*u1 = b*u2 & (a<>0 or b<>0) );

theorem :: ANALMETR:14
Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y implies
u,v1+v2 are_Ort_wrt w,y & u,v1-v2 are_Ort_wrt w,y;

theorem :: ANALMETR:15
Gen w,y & u,u are_Ort_wrt w,y implies u = 0.V;

theorem :: ANALMETR:16
Gen w,y & u,u1-u2 are_Ort_wrt w,y & u1,u2-u are_Ort_wrt w,y
implies u2,u-u1 are_Ort_wrt w,y;

theorem :: ANALMETR:17
(Gen w,y & u <> 0.V) implies ex a st v - a*u,u are_Ort_wrt w,y;

theorem :: ANALMETR:18
(u,v // u1,v1 or u,v // v1,u1) iff
(ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0));

theorem :: ANALMETR:19
[[u,v],[u1,v1]] in lambda(DirPar(V)) iff
(ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0));

definition let V; let u,u1,v,v1,w,y;
pred u,u1,v,v1 are_Ort_wrt w,y means
:: ANALMETR:def 3
u1-u,v1-v are_Ort_wrt w,y;
end;

definition let V; let w,y;
func Orthogonality(V,w,y) -> Relation of [:the carrier of V,the carrier of V:]
means
:: ANALMETR:def 4
[x,z] in it iff
ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1 are_Ort_wrt w,y;
end;

reserve p,p1,q,q1 for
Element of Lambda(OASpace(V));

canceled 2;

theorem :: ANALMETR:22
the carrier of Lambda(OASpace(V)) = the carrier of V;

theorem :: ANALMETR:23
the CONGR of Lambda(OASpace(V)) = lambda(DirPar(V));

theorem :: ANALMETR:24
p=u & q=v & p1=u1 & q1=v1 implies
(p,q // p1,q1 iff (ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0)));

definition
struct(AffinStruct) ParOrtStr (# carrier -> set,
CONGR -> (Relation of [:the carrier,the carrier:]),
orthogonality -> Relation of [:the carrier,the carrier:] #);
end;

definition
cluster non empty ParOrtStr;
end;

reserve POS for non empty ParOrtStr;

definition let POS; let a,b,c,d be Element of POS;
pred a,b // c,d means
:: ANALMETR:def 5
[[a,b],[c,d]] in the CONGR of POS;
pred a,b _|_ c,d means
:: ANALMETR:def 6
[[a,b],[c,d]] in the orthogonality of POS;
end;

definition let V,w,y;
func AMSpace(V,w,y) -> strict ParOrtStr equals
:: ANALMETR:def 7

ParOrtStr(#the carrier of V,lambda(DirPar(V)),Orthogonality(V,w,y)#);
end;

definition let V,w,y;
cluster AMSpace(V,w,y) -> non empty;
end;

canceled 3;

theorem :: ANALMETR:28
(the carrier of AMSpace(V,w,y) = the carrier of V
& the CONGR of AMSpace(V,w,y) = lambda(DirPar(V))
& the orthogonality of AMSpace(V,w,y) = Orthogonality(V,w,y));

definition let POS; func Af(POS) -> strict AffinStruct equals
:: ANALMETR:def 8
AffinStruct (# the carrier of POS, the CONGR of POS #);
end;

definition let POS;
cluster Af POS -> non empty;
end;

canceled;

theorem :: ANALMETR:30
Af(AMSpace(V,w,y)) = Lambda(OASpace(V));

reserve p,p1,p2,q,q1,r,r1,r2 for Element of AMSpace(V,w,y);

theorem :: ANALMETR:31
p=u & p1=u1 & q=v & q1=v1 implies
(p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y);

theorem :: ANALMETR:32
p=u & q=v & p1=u1 & q1=v1 implies
(p,q // p1,q1 iff (ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0)));

theorem :: ANALMETR:33
p,q _|_ p1,q1 implies p1,q1 _|_ p,q;

theorem :: ANALMETR:34
p,q _|_ p1,q1 implies p,q _|_ q1,p1;

theorem :: ANALMETR:35
Gen w,y implies for p,q,r holds p,q _|_ r,r;

theorem :: ANALMETR:36
p,p1 _|_ q,q1 & p,p1 // r,r1 implies p=p1 or q,q1 _|_ r,r1;

theorem :: ANALMETR:37
Gen w,y implies (for p,q,r ex r1 st p,q _|_ r,r1 & r<>r1);

theorem :: ANALMETR:38
Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_
r,r1 implies p=p1 or q,q1 // r,r1;

theorem :: ANALMETR:39
Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 implies p,q _|_ r1,r2;

theorem :: ANALMETR:40
Gen w,y & p,q _|_ p,q implies p = q;

theorem :: ANALMETR:41
Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p implies p2,q _|_ p,p1;

theorem :: ANALMETR:42
Gen w,y & p<>p1 implies for q ex q1 st p,p1 // p,q1 & p,p1 _|_ q1,q;

definition let IT be non empty ParOrtStr;
attr IT is OrtAfSp-like means
:: ANALMETR:def 9
AffinStruct(#the carrier of IT,the CONGR of IT#) is AffinSpace
& (for a,b,c,d,p,q,r,s being Element of IT holds
(a,b _|_ a,b implies a=b) & a,b _|_ c,c &
(a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) &
(a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) &
(a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s)) &
(for a,b,c being Element of IT st a<>b
ex x being Element of IT st a,b // a,x & a,b _|_ x,c) &
(for a,b,c being Element of IT
ex x being Element of IT st a,b _|_ c,x & c <>x);
end;

definition
cluster strict OrtAfSp-like (non empty ParOrtStr);
end;

definition
mode OrtAfSp is OrtAfSp-like (non empty ParOrtStr);
end;

canceled;

theorem :: ANALMETR:44
Gen w,y implies AMSpace(V,w,y) is OrtAfSp;

definition let IT be non empty ParOrtStr;
attr IT is OrtAfPl-like means
:: ANALMETR:def 10
AffinStruct(#the carrier of IT,the CONGR of IT#) is AffinPlane
& (for a,b,c,d,p,q,r,s being Element of IT holds
(a,b _|_ a,b implies a=b) & a,b _|_ c,c &
(a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) &
(a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) &
(a,b _|_ p,q & a,b _|_ r,s implies p,q // r,s or a=b)) &
(for a,b,c being Element of IT
ex x being Element of IT st a,b _|_ c,x & c <>x);
end;

definition
cluster strict OrtAfPl-like (non empty ParOrtStr);
end;

definition
mode OrtAfPl is OrtAfPl-like (non empty ParOrtStr);
end;

canceled;

theorem :: ANALMETR:46
Gen w,y implies AMSpace(V,w,y) is OrtAfPl;

theorem :: ANALMETR:47
for x being set holds (x is Element of POS iff
x is Element of Af(POS));

theorem :: ANALMETR:48
for a,b,c,d being Element of POS, a',b',c',d' being
Element of Af(POS) st a=a'& b=b' & c = c' & d=d' holds
(a,b // c,d iff a',b' // c',d');

definition let POS be OrtAfSp;
cluster Af(POS) -> AffinSpace-like non trivial;
end;

definition let POS be OrtAfPl;
cluster Af(POS) -> 2-dimensional AffinSpace-like non trivial;
end;

theorem :: ANALMETR:49
for POS being OrtAfPl holds POS is OrtAfSp;

definition
cluster OrtAfPl-like -> OrtAfSp-like (non empty ParOrtStr);
end;

theorem :: ANALMETR:50
for POS being OrtAfSp st Af(POS) is AffinPlane
holds POS is OrtAfPl;

theorem :: ANALMETR:51
for POS being non empty ParOrtStr holds POS is OrtAfPl-like iff
( (ex a,b being Element of POS st a<>b) &
(for a,b,c,d,p,q,r,s being Element of POS
holds (a,b // b,a & a,b // c,c & (a,b // p,q & a,b // r,s
implies p,q // r,s or a=b) & (a,b // a,c implies b,a // b,c) &
(ex x being Element of POS st a,b // c,x & a,c // b,x) &
(ex x,y,z being Element of POS st not x,y // x,z ) &
(ex x being Element of POS st a,b // c,x & c <>x) &
(a,b // b,d & b<>a implies ex x being Element of POS
st c,b // b,x & c,a // d,x) &
(a,b _|_ a,b implies a=b) & a,b _|_ c,c &
(a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) &
(a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) &
(a,b _|_ p,q & a,b _|_ r,s implies p,q // r,s or a=b) &
(ex x being Element of POS st a,b _|_ c,x & c <>x) &
(not a,b // c,d implies ex x being Element of POS
st a,b // a,x & c,d // c,x ))));

reserve x,a,b,c,d,p,q,y for Element of POS;

definition let POS; let a,b,c;
pred LIN a,b,c means
:: ANALMETR:def 11
a,b // a,c;
end;

definition let POS,a,b;
func Line(a,b) -> Subset of POS means
:: ANALMETR:def 12
for x being Element of POS holds x in it iff LIN a,b,x; end;

reserve A,K,M for Subset of POS;

definition let POS; let A;
attr A is being_line means
:: ANALMETR:def 13
ex a,b st a<>b & A=Line(a,b);
synonym A is_line;
end;

canceled 3;

theorem :: ANALMETR:55
for POS being OrtAfSp for a,b,c being Element of POS,
a',b',c' being Element of Af(POS) st a=a'& b=b' & c = c' holds
(LIN a,b,c iff LIN a',b',c');

theorem :: ANALMETR:56
for POS being OrtAfSp for a,b being Element of POS,
a',b' being Element of Af(POS) st a=a' & b=b' holds
Line(a,b) = Line(a',b');

theorem :: ANALMETR:57
for X being set holds ( X is Subset of POS iff
X is Subset of Af(POS));

theorem :: ANALMETR:58
for POS being OrtAfSp for X being Subset of POS,
Y being Subset of Af(POS) st X=Y holds
( X is_line iff Y is_line);

definition let POS; let a,b,K; pred a,b _|_ K means
:: ANALMETR:def 14
ex p,q st p<>q & K = Line(p,q) & a,b _|_ p,q; end;

definition let POS; let K,M; pred K _|_ M means
:: ANALMETR:def 15
ex p,q st p<>q & K = Line(p,q) & p,q _|_ M; end;

definition let POS; let K,M; pred K // M means
:: ANALMETR:def 16
ex a,b,c,d st a<>b & c <>d & K = Line(a,b) & M = Line(c,d)
& a,b // c,d; end;

canceled 3;

theorem :: ANALMETR:62
(a,b _|_ K implies K is_line) & (K _|_ M implies (K is_line & M is_line));

theorem :: ANALMETR:63
K _|_ M iff ex a,b,c,d st (a<>b & c <>d & K = Line(a,b) & M = Line(c,d) &
a,b _|_ c,d);

theorem :: ANALMETR:64
for POS being OrtAfSp for M,N being Subset of POS,
M',N' being Subset of Af(POS) st M = M' & N = N' holds
(M // N iff M' // N');

reserve POS for OrtAfSp;
reserve A,K,M,N for Subset of POS;
reserve a,b,c,d,p,q,r,s for Element of POS;

theorem :: ANALMETR:65
K is_line implies a,a _|_ K;

theorem :: ANALMETR:66
a,b _|_ K & (a,b // c,d or c,d // a,b) & a<>b implies c,d _|_ K;

theorem :: ANALMETR:67
a,b _|_ K implies b,a _|_ K;

theorem :: ANALMETR:68
K // M implies M // K;

theorem :: ANALMETR:69
r,s _|_ K & (K // M or M // K) implies r,s _|_ M;

theorem :: ANALMETR:70
K _|_ M implies M _|_ K;

definition let POS be OrtAfSp; let K,M be Subset of POS;
redefine pred K // M;
symmetry;
redefine pred K _|_ M;
symmetry;
end;

theorem :: ANALMETR:71
a in K & b in K & a,b _|_ K implies a=b;

theorem :: ANALMETR:72
not K _|_ K;

theorem :: ANALMETR:73
(K _|_ M or M _|_ K) & (K // N or N // K) implies (M _|_ N & N _|_ M);

theorem :: ANALMETR:74
K // N implies not K _|_ N;

theorem :: ANALMETR:75
a in K & b in K & c,d _|_ K implies (c,d _|_ a,b & a,b _|_ c,d);

theorem :: ANALMETR:76
a in K & b in K & a<>b & K is_line implies K =Line(a,b);

theorem :: ANALMETR:77
a in K & b in
K & a<>b & K is_line & (a,b _|_ c,d or c,d _|_ a,b) implies c,d _|_ K;

theorem :: ANALMETR:78
a in M & b in M & c in N & d in N & M _|_ N implies a,b _|_ c,d;

theorem :: ANALMETR:79
p in M & p in N & a in M & b in N & a<>b & a in K & b in
K & A _|_ M & A _|_ N &
K is_line implies A _|_ K;

theorem :: ANALMETR:80
b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c;

theorem :: ANALMETR:81
a,b // c,d implies a,b // d,c & b,a // c,d & b,a // d,c &
c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a;

theorem :: ANALMETR:82
p<>q & ((p,q // a,b & p,q // c,d) or (p,q // a,b & c,d // p,q) or
(a,b // p,q & c,d // p,q) or (a,b // p,q & p,q // c,d)) implies a,b // c,d;

theorem :: ANALMETR:83
a,b _|_ c,d implies a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c &
c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a;

theorem :: ANALMETR:84
p<>q & ((p,q // a,b & p,q _|_ c,d) or (p,q // c,d & p,q _|_ a,b) or
(p,q // a,b & c,d _|_ p,q) or (p,q // c,d & a,b _|_ p,q) or
(a,b // p,q & c,d _|_ p,q) or (c,d // p,q & a,b _|_ p,q) or
(a,b // p,q & p,q _|_ c,d) or (c,d // p,q & p,q _|_ a,b))
implies a,b _|_ c,d;

reserve POS for OrtAfPl;
reserve K,M,N for Subset of POS;
reserve x,a,b,c,d,p,q for Element of POS;

theorem :: ANALMETR:85
p<>q & ((p,q _|_ a,b & p,q _|_ c,d) or (p,q _|_ a,b & c,d _|_ p,q) or
(a,b _|_ p,q & c,d _|_ p,q) or (a,b _|_ p,q & p,q _|_ c,d)) implies a,b // c,d
;

theorem :: ANALMETR:86
a in M & b in M & a<>b & M is_line & c in N & d in N & c <>d & N is_line &
a,b // c,d implies M // N;

theorem :: ANALMETR:87
(K _|_ M or M _|_ K) & (K _|_ N or N _|_ K) implies (M // N & N // M
);

theorem :: ANALMETR:88
M _|_ N implies ex p st p in M & p in N;

theorem :: ANALMETR:89
a,b _|_ c,d implies ex p st LIN a,b,p & LIN c,d,p;

theorem :: ANALMETR:90
a,b _|_ K implies ex p st LIN a,b,p & p in K;

theorem :: ANALMETR:91
ex x st a,x _|_ p,q & LIN p,q,x;

theorem :: ANALMETR:92
K is_line implies ex x st a,x _|_ K & x in K;
```