:: Transformations in Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received May 31, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, FUNCT_2, RELAT_1, FUNCT_1, TARSKI, ZFMISC_1,
RELAT_2, ANALOAF, STRUCT_0, DIRAF, PARSP_1, INCSP_1, AFF_1, TRANSGEO,
PENCIL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_2, FUNCT_1, RELSET_1,
STRUCT_0, ANALOAF, DIRAF, PARTFUN1, FUNCT_2, AFF_1;
constructors RELAT_2, PARTFUN1, DOMAIN_1, AFF_1, RELSET_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0,
ANALOAF, DIRAF;
requirements SUBSET, BOOLE;
definitions RELAT_2;
theorems DOMAIN_1, FUNCT_1, FUNCT_2, ANALOAF, DIRAF, AFF_1, PASCH, TARSKI,
ZFMISC_1, RELAT_1, XBOOLE_0, STRUCT_0;
schemes FUNCT_2;
begin
reserve A for non empty set,
a,b,x,y,z,t for Element of A,
f,g,h for Permutation of A;
definition
let A be set, f,g be Permutation of A;
redefine func g*f -> Permutation of A; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
thus g*f is Permutation of A;
end;
end;
theorem Th1:
ex x st f.x=y
proof
rng f = A by FUNCT_2:def 3;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis;
end;
theorem Th2:
f.x=y iff (f").y=x
proof
A1: now
x in A;
then
A2: x in dom f by FUNCT_2:def 1;
assume f.x=y;
hence x=f".y by A2,FUNCT_1:34;
end;
rng f = A by FUNCT_2:def 3;
hence thesis by A1,FUNCT_1:35;
end;
definition
let A,f,g;
func f\g -> Permutation of A equals
(g*f)*g";
coherence;
end;
scheme
EXPermutation{A() -> non empty set,P[object,object]}:
ex f being Permutation of A(
) st for x,y being Element of A() holds f.x=y iff P[x,y]
provided
A1: for x being Element of A() ex y being Element of A() st P[x,y] and
A2: for y being Element of A() ex x being Element of A() st P[x,y] and
A3: for x,y,x9 being Element of A() st P[x,y] & P[x9,y] holds x=x9 and
A4: for x,y,y9 being Element of A() st P[x,y] & P[x,y9] holds y=y9
proof
A5: for x being Element of A() ex y being Element of A() st P[x,y] by A1;
consider f being Function of A(), A() such that
A6: for x being Element of A() holds P[x,f.x] from FUNCT_2:sch 3(A5);
now
let y be object;
assume
A7: y in A();
then consider x being Element of A() such that
A8: P[x,y] by A2;
P[x,f.x] by A6;
then f.x = y by A4,A7,A8;
hence y in rng f by FUNCT_2:4;
end;
then A() c= rng f by TARSKI:def 3;
then
A9: rng f = A() by XBOOLE_0:def 10;
now
let x1,x2 be object;
assume that
A10: x1 in A() and
A11: x2 in A();
A12: f.x1 is Element of A() by A10,FUNCT_2:5;
( P[x1,f.x1])& P[x2,f.x2] by A6,A10,A11;
hence f.x1 = f.x2 implies x1 = x2 by A3,A10,A11,A12;
end;
then f is one-to-one by FUNCT_2:19;
then reconsider f as Permutation of A() by A9,FUNCT_2:57;
take f;
let x,y be Element of A();
thus f.x=y implies P[x,y] by A6;
assume
A13: P[x,y];
P[x,f.x] by A6;
hence thesis by A4,A13;
end;
theorem
f.(f".x) = x & f".(f.x) = x by Th2;
theorem
f*(id A) = (id A)*f
proof
f*(id A)=f by FUNCT_2:17;
hence thesis by FUNCT_2:17;
end;
Lm1: f*g=f*h implies g=h
proof
assume f*g=f*h;
then (f"*f)*g=f"*(f*h) by RELAT_1:36;
then (f"*f)*g=(f"*f)*h by RELAT_1:36;
then (id A)*g=(f"*f)*h by FUNCT_2:61;
then (id A)*g=(id A)*h by FUNCT_2:61;
then g=(id A)*h by FUNCT_2:17;
hence thesis by FUNCT_2:17;
end;
Lm2: g*f=h*f implies g=h
proof
assume g*f=h*f;
then g*(f*f")=(h*f)*f" by RELAT_1:36;
then g*(f*f")=h*(f*f") by RELAT_1:36;
then g*(id A)=h*(f*f") by FUNCT_2:61;
then g*(id A)=h*(id A) by FUNCT_2:61;
then g=h*(id A) by FUNCT_2:17;
hence thesis by FUNCT_2:17;
end;
theorem
g*f=h*f or f*g=f*h implies g=h by Lm1,Lm2;
theorem
(f*g)\h = (f\h)*(g\h)
proof
thus (f*g)\h = (h*(f*((id A)*g)))*h" by FUNCT_2:17
.= (h*(f*((h"*h)*g)))*h" by FUNCT_2:61
.= (h*(f*(h"*(h*g))))*h" by RELAT_1:36
.= (h*((f*h")*(h*g)))*h" by RELAT_1:36
.= ((h*(f*h"))*(h*g))*h" by RELAT_1:36
.= (h*(f*h"))*((h*g)*h") by RELAT_1:36
.= (f\h)*(g\h) by RELAT_1:36;
end;
theorem
(f")\g = (f\g)"
proof
thus (f\g)" = (g")"*(g*f)" by FUNCT_1:44
.= (g")"*(f"*g") by FUNCT_1:44
.= g*(f"*g") by FUNCT_1:43
.= f"\g by RELAT_1:36;
end;
theorem
f\(g*h) = (f\h)\g
proof
thus f\(g*h) = ((g*h)*f)*(h"*g") by FUNCT_1:44
.= (((g*h)*f)*h")*g" by RELAT_1:36
.= ((g*(h*f))*h")*g" by RELAT_1:36
.= (f\h)\g by RELAT_1:36;
end;
theorem
(id A)\f = id A
proof
thus (id A)\f = f*f" by FUNCT_2:17
.= id A by FUNCT_2:61;
end;
theorem
f\(id A) = f
proof
thus f\(id A) = f*(id A)" by FUNCT_2:17
.= f*(id A) by FUNCT_1:45
.= f by FUNCT_2:17;
end;
theorem
f.a=a implies (f\g).(g.a)=g.a
proof
assume
A1: f.a=a;
g".(g.a) = (g"*g).a by FUNCT_2:15
.= (id A).a by FUNCT_2:61
.= a;
hence (f\g).(g.a) = (g*f).a by FUNCT_2:15
.= g.a by A1,FUNCT_2:15;
end;
reserve R for Relation of [:A,A:];
definition
let A,f,R;
pred f is_FormalIz_of R means
for x,y holds [[x,y],[f.x,f.y]] in R;
end;
theorem Th12:
R is_reflexive_in [:A,A:] implies id A is_FormalIz_of R
proof
assume
A1: for x being object st x in [:A,A:] holds [x,x] in R;
let x,y;
A2: [x,y] in [:A,A:] by ZFMISC_1:def 2;
thus thesis by A1,A2;
end;
theorem Th13:
R is_symmetric_in [:A,A:] & f is_FormalIz_of R implies f" is_FormalIz_of R
proof
assume
A1: for x,y being object st x in [:A,A:] & y in [:A,A:] & [x,y] in R holds
[y,x] in R;
assume
A2: for x,y holds [[x,y],[f.x,f.y]] in R;
let x,y;
A3: [[f".x,f".y],[f.(f".x),f.(f".y)]] in R by A2;
A4: [f".x,f".y] in [:A,A:] & [f.(f".x),f.(f".y)] in [:A,A:] by ZFMISC_1:def 2;
f.(f".x) = x & f.(f".y) =y by Th2;
hence thesis by A1,A3,A4;
end;
theorem
R is_transitive_in [:A,A:] & f is_FormalIz_of R & g is_FormalIz_of R
implies (f*g) is_FormalIz_of R
proof
assume that
A1: for x,y,z being object st x in [:A,A:] & y in [:A,A:] & z in [:A,A:] &
[x,y] in R & [y,z] in R holds [x,z] in R and
A2: for x,y holds [[x,y],[f.x,f.y]] in R and
A3: for x,y holds [[x,y],[g.x,g.y]] in R;
let x,y;
f.(g.x) = (f*g).x & f.(g.y) = (f*g).y by FUNCT_2:15;
then
A4: [[g.x,g.y],[(f*g).x,(f*g).y]] in R by A2;
A5: [(f*g).x,(f*g).y] in [:A,A:] by ZFMISC_1:def 2;
A6: [x,y] in [:A,A:] & [g.x,g.y] in [:A,A:] by ZFMISC_1:def 2;
[[x,y],[g.x,g.y]] in R by A3;
hence thesis by A1,A4,A6,A5;
end;
theorem Th15:
(for a,b,x,y,z,t st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a
<>b holds [[x,y],[z,t]] in R) & (for x,y,z holds [[x,x],[y,z]] in R) & f
is_FormalIz_of R & g is_FormalIz_of R implies f*g is_FormalIz_of R
proof
assume that
A1: for a,b,x,y,z,t st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a<>b
holds [[x,y],[z,t]] in R and
A2: for x,y,z holds [[x,x],[y,z]] in R and
A3: for x,y holds [[x,y],[f.x,f.y]] in R and
A4: for x,y holds [[x,y],[g.x,g.y]] in R;
let x,y;
f.(g.x) = (f*g).x & f.(g.y) = (f*g).y by FUNCT_2:15;
then
A5: [[g.x,g.y],[(f*g).x,(f*g).y]] in R by A3;
A6: now
assume g.x = g.y;
then x = y by FUNCT_2:58;
hence thesis by A2;
end;
[[x,y],[g.x,g.y]] in R by A4;
hence thesis by A1,A5,A6;
end;
definition
let A;
let f;
let R;
pred f is_automorphism_of R means
for x,y,z,t holds ([[x,y],[z,t]] in R iff [[f.x,f.y],[f.z,f.t]] in R);
end;
theorem
id A is_automorphism_of R;
theorem Th17:
f is_automorphism_of R implies f" is_automorphism_of R
proof
assume
A1: for x,y,z,t holds ([[x,y],[z,t]] in R iff [[f.x,f.y],[f.z,f.t]] in R );
let x,y,z,t;
A2: f.(f".z) = z & f.(f".t) = t by Th2;
f.(f".x) = x & f.(f".y) = y by Th2;
hence thesis by A1,A2;
end;
theorem Th18:
f is_automorphism_of R & g is_automorphism_of R implies g*f
is_automorphism_of R
proof
assume that
A1: for x,y,z,t holds ([[x,y],[z,t]] in R iff [[f.x,f.y],[f.z,f.t]] in R ) and
A2: for x,y,z,t holds ([[x,y],[z,t]] in R iff [[g.x,g.y],[g.z,g.t]] in R );
let x,y,z,t;
A3: g.(f.x) = (g*f).x & g.(f.y) = (g*f).y by FUNCT_2:15;
A4: g.(f.z) = (g*f).z & g.(f.t) = (g*f).t by FUNCT_2:15;
[[x,y],[z,t]] in R iff [[f.x,f.y],[f.z,f.t]] in R by A1;
hence thesis by A2,A3,A4;
end;
theorem
R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] & f
is_FormalIz_of R implies f is_automorphism_of R
proof
assume that
A1: for x,y being object st x in [:A,A:] & y in [:A,A:] & [x,y] in R holds
[y,x] in R and
A2: for x,y,z being object st x in [:A,A:] & y in [:A,A:] & z in [:A,A:] &
[x,y] in R & [y,z] in R holds [x,z] in R and
A3: for x,y holds [[x,y],[f.x,f.y]] in R;
let x,y,z,t;
A4: [z,t] in [:A,A:] by ZFMISC_1:def 2;
A5: [f.z,f.t] in [:A,A:] by ZFMISC_1:def 2;
A6: [f.x,f.y] in [:A,A:] by ZFMISC_1:def 2;
A7: [x,y] in [:A,A:] by ZFMISC_1:def 2;
A8: now
[[z,t],[f.z,f.t]] in R by A3;
then
A9: [[f.z,f.t],[z,t]] in R by A1,A4,A5;
assume
A10: [[f.x,f.y],[f.z,f.t]] in R;
[[x,y],[f.x,f.y]] in R by A3;
then [[x,y],[f.z,f.t]] in R by A2,A7,A6,A5,A10;
hence [[x,y],[z,t]] in R by A2,A7,A4,A5,A9;
end;
now
[[x,y],[f.x,f.y]] in R by A3;
then
A11: [[f.x,f.y],[x,y]] in R by A1,A7,A6;
A12: [[z,t],[f.z,f.t]] in R by A3;
assume [[x,y],[z,t]] in R;
then [[f.x,f.y],[z,t]] in R by A2,A7,A4,A6,A11;
hence [[f.x,f.y],[f.z,f.t]] in R by A2,A4,A6,A5,A12;
end;
hence thesis by A8;
end;
theorem
(for a,b,x,y,z,t st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a<>b
holds [[x,y],[z,t]] in R) & (for x,y,z holds [[x,x],[y,z]] in R) & R
is_symmetric_in [:A,A:] & f is_FormalIz_of R implies f is_automorphism_of R
proof
assume that
A1: for a,b,x,y,z,t st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a<>b
holds [[x,y],[z,t]] in R and
A2: for x,y,z holds [[x,x],[y,z]] in R and
A3: for x,y being object st x in [:A,A:] & y in [:A,A:] & [x,y] in R holds
[y,x] in R and
A4: for x,y holds [[x,y],[f.x,f.y]] in R;
A5: for x,y,z holds [[y,z],[x,x]] in R
proof
let x,y,z;
A6: [y,z] in [:A,A:] & [x,x] in [:A,A:] by ZFMISC_1:def 2;
[[x,x],[y,z]] in R by A2;
hence thesis by A3,A6;
end;
let x,y,z,t;
A7: [[x,y],[f.x,f.y]] in R by A4;
A8: [[z,t],[f.z,f.t]] in R by A4;
[z,t] in [:A,A:] & [f.z,f.t] in [:A,A:] by ZFMISC_1:def 2;
then
A9: [[f.z,f.t],[z,t]] in R by A3,A8;
A10: now
assume
A11: [[f.x,f.y],[f.z,f.t]] in R;
A12: now
assume that
A13: f.x<>f.y and
A14: f.z<>f.t;
[[x,y],[f.z,f.t]] in R by A1,A7,A11,A13;
hence [[x,y],[z,t]] in R by A1,A9,A14;
end;
A15: now
assume f.z = f.t;
then z=t by FUNCT_2:58;
hence [[x,y],[z,t]] in R by A5;
end;
now
assume f.x = f.y;
then x=y by FUNCT_2:58;
hence [[x,y],[z,t]] in R by A2;
end;
hence [[x,y],[z,t]] in R by A15,A12;
end;
[x,y] in [:A,A:] & [f.x,f.y] in [:A,A:] by ZFMISC_1:def 2;
then
A16: [[f.x,f.y],[x,y]] in R by A3,A7;
now
assume
A17: [[x,y],[z,t]] in R;
now
assume that
A18: x<>y and
A19: z<>t;
[[f.x,f.y],[z,t]] in R by A1,A16,A17,A18;
hence [[f.x,f.y],[f.z,f.t]] in R by A1,A8,A19;
end;
hence [[f.x,f.y],[f.z,f.t]] in R by A2,A5;
end;
hence thesis by A10;
end;
theorem
f is_FormalIz_of R & g is_automorphism_of R implies f\g is_FormalIz_of R
proof
assume that
A1: for x,y holds [[x,y],[f.x,f.y]] in R and
A2: for x,y,z,t holds ([[x,y],[z,t]] in R iff [[g.x,g.y],[g.z,g.t]] in R );
let x,y;
A3: [[g".x,g".y],[f.(g".x),f.(g".y)]] in R by A1;
g.(g".x) = x & g.(g".y) = y by Th2;
then [[x,y],[g.(f.(g".x)),g.(f.(g".y))]] in R by A2,A3;
then [[x,y],[(g*f).(g".x),g.(f.(g".y))]] in R by FUNCT_2:15;
then [[x,y],[(g*f).(g".x),(g*f).(g".y)]] in R by FUNCT_2:15;
then [[x,y],[((g*f)*g").x,(g*f).(g".y)]] in R by FUNCT_2:15;
hence thesis by FUNCT_2:15;
end;
reserve AS for non empty AffinStruct;
definition
let AS;
let f be Permutation of the carrier of AS;
pred f is_DIL_of AS means
f is_FormalIz_of the CONGR of AS;
end;
reserve a,b,x,y for Element of AS;
theorem Th22:
for f being Permutation of the carrier of AS holds (f is_DIL_of
AS iff for a,b holds a,b // f.a,f.b )
proof
let f be Permutation of the carrier of AS;
A1: now
assume
A2: for a,b holds a,b // f.a,f.b;
for x,y holds [[x,y],[f.x,f.y]] in the CONGR of AS
by A2,ANALOAF:def 2;
then f is_FormalIz_of the CONGR of AS;
hence f is_DIL_of AS;
end;
now
assume
A3: f is_DIL_of AS;
let a,b;
f is_FormalIz_of the CONGR of AS by A3;
then [[a,b],[f.a,f.b]] in the CONGR of AS;
hence a,b // f.a,f.b by ANALOAF:def 2;
end;
hence thesis by A1;
end;
definition
let IT be non empty AffinStruct;
attr IT is CongrSpace-like means
:Def5:
(for x,y,z,t,a,b being Element of IT
st x,y // a,b & a,b // z,t & a<>b holds x,y // z,t) & (for x,y,z being Element
of IT holds x,x // y,z) & (for x,y,z,t being Element of IT st x,y // z,t holds
z,t // x,y) & for x,y being Element of IT holds x,y // x,y;
end;
registration
cluster strict CongrSpace-like for non empty AffinStruct;
existence
proof
set OAS = the strict OAffinSpace;
A1: ( for x,y,z,t being Element of OAS st x,y // z,t holds z,t // x,y)&
for x,y being Element of OAS holds x,y // x,y by DIRAF:1,2;
( for x,y,z,t,a,b being Element of OAS st x,y // a,b & a,b // z,t & a
<>b holds x,y // z,t)& for x,y,z being Element of OAS holds x,x // y,z by
DIRAF:3,4;
then OAS is CongrSpace-like by A1;
hence thesis;
end;
end;
definition
mode CongrSpace is CongrSpace-like non empty AffinStruct;
end;
reserve CS for CongrSpace;
Lm3: the CONGR of CS is_reflexive_in [:the carrier of CS,the carrier of CS:]
proof
let x be object;
assume x in [:the carrier of CS,the carrier of CS:];
then consider x1,x2 being Element of CS such that
A1: x=[x1,x2] by DOMAIN_1:1;
x1,x2 // x1,x2 by Def5;
hence thesis by A1,ANALOAF:def 2;
end;
Lm4: the CONGR of CS is_symmetric_in [:the carrier of CS,the carrier of CS:]
proof
let x,y be object;
assume that
A1: x in [:the carrier of CS,the carrier of CS:] and
A2: y in [:the carrier of CS,the carrier of CS:] and
A3: [x,y] in the CONGR of CS;
consider x1,x2 being Element of CS such that
A4: x=[x1,x2] by A1,DOMAIN_1:1;
consider y1,y2 being Element of CS such that
A5: y=[y1,y2] by A2,DOMAIN_1:1;
x1,x2 // y1,y2 by A3,A4,A5,ANALOAF:def 2;
then y1,y2 // x1,x2 by Def5;
hence thesis by A4,A5,ANALOAF:def 2;
end;
theorem Th23:
id the carrier of CS is_DIL_of CS
by Lm3,Th12;
theorem Th24:
for f being Permutation of the carrier of CS st f is_DIL_of CS
holds f" is_DIL_of CS
by Lm4,Th13;
theorem Th25:
for f,g being Permutation of the carrier of CS st f is_DIL_of CS
& g is_DIL_of CS holds f*g is_DIL_of CS
proof
let f,g be Permutation of the carrier of CS;
A1: now
let a,b,x,y,z,t be Element of CS;
assume that
A2: [[x,y],[a,b]] in the CONGR of CS & [[a,b],[z,t]] in the CONGR of CS and
A3: a<>b;
x,y // a,b & a,b // z,t by A2,ANALOAF:def 2;
then x,y // z,t by A3,Def5;
hence [[x,y],[z,t]] in the CONGR of CS by ANALOAF:def 2;
end;
A4: now
let x,y,z be Element of CS;
x,x // y,z by Def5;
hence [[x,x],[y,z]] in the CONGR of CS by ANALOAF:def 2;
end;
assume f is_DIL_of CS & g is_DIL_of CS;
then f is_FormalIz_of the CONGR of CS & g is_FormalIz_of the CONGR of CS;
then f*g is_FormalIz_of the CONGR of CS by A1,A4,Th15;
hence thesis;
end;
reserve OAS for OAffinSpace;
reserve a,b,c,d,p,q,r,x,y,z,t,u for Element of OAS;
theorem Th26:
OAS is CongrSpace-like
by DIRAF:3,DIRAF:4,DIRAF:2,DIRAF:1;
reserve f,g for Permutation of the carrier of OAS;
definition
let OAS;
let f be Permutation of the carrier of OAS;
attr f is positive_dilatation means
f is_DIL_of OAS;
end;
theorem Th27:
for f being Permutation of the carrier of OAS holds (f is
positive_dilatation iff for a,b holds a,b // f.a,f.b ) by Th22;
definition
let OAS;
let f be Permutation of the carrier of OAS;
attr f is negative_dilatation means
for a,b holds a,b // f.b,f.a;
end;
theorem Th28:
id the carrier of OAS is positive_dilatation
proof
OAS is CongrSpace by Th26;
then id the carrier of OAS is_DIL_of OAS by Th23;
hence thesis;
end;
theorem
for f being Permutation of the carrier of OAS st f is
positive_dilatation holds f" is positive_dilatation
proof
let f be Permutation of the carrier of OAS;
assume f is positive_dilatation;
then
A1: f is_DIL_of OAS;
OAS is CongrSpace by Th26;
then f" is_DIL_of OAS by A1,Th24;
hence thesis;
end;
theorem
for f,g being Permutation of the carrier of OAS st f is
positive_dilatation & g is positive_dilatation holds f*g is positive_dilatation
proof
let f,g be Permutation of the carrier of OAS;
assume f is positive_dilatation & g is positive_dilatation;
then
A1: f is_DIL_of OAS & g is_DIL_of OAS;
OAS is CongrSpace by Th26;
then f*g is_DIL_of OAS by A1,Th25;
hence thesis;
end;
theorem
not ex f st f is negative_dilatation & f is positive_dilatation
proof
given f such that
A1: f is negative_dilatation & f is positive_dilatation;
consider a,b such that
A2: a<>b by STRUCT_0:def 10;
a,b // f.a,f.b & a,b // f.b,f.a by A1,Th27;
then f.a,f.b // f.b,f.a by A2,ANALOAF:def 5;
then f.a = f.b by ANALOAF:def 5;
hence contradiction by A2,FUNCT_2:58;
end;
theorem
f is negative_dilatation implies f" is negative_dilatation
proof
assume
A1: f is negative_dilatation;
let x,y;
set x9=f".x, y9=f".y;
f.x9=x & f.y9=y by Th2;
then y9,x9 // x,y by A1;
hence thesis by DIRAF:2;
end;
theorem
f is positive_dilatation & g is negative_dilatation implies f*g is
negative_dilatation & g*f is negative_dilatation
proof
assume
A1: f is positive_dilatation & g is negative_dilatation;
thus x,y // (f*g).y,(f*g).x
proof
set x9=g.x;
set y9=g.y;
A2: (f*g).x= f.x9 & (f*g).y=f.y9 by FUNCT_2:15;
A3: now
assume x9=y9;
then x=y by FUNCT_2:58;
hence thesis by DIRAF:4;
end;
x,y // y9,x9 & y9,x9 // f.y9,f.x9 by A1,Th27;
hence thesis by A2,A3,DIRAF:3;
end;
thus x,y // (g*f).y,(g*f).x
proof
set x9=f.x;
set y9=f.y;
A4: (g*f).x= g.x9 & (g*f).y=g.y9 by FUNCT_2:15;
A5: now
assume x9=y9;
then x=y by FUNCT_2:58;
hence thesis by DIRAF:4;
end;
x,y // x9,y9 & x9,y9 // g.y9,g.x9 by A1,Th27;
hence thesis by A4,A5,DIRAF:3;
end;
end;
definition
let OAS;
let f be Permutation of the carrier of OAS;
attr f is dilatation means
f is_FormalIz_of lambda(the CONGR of OAS);
end;
theorem Th34:
for f being Permutation of the carrier of OAS holds (f is
dilatation iff for a,b holds a,b '||' f.a,f.b )
proof
let f be Permutation of the carrier of OAS;
A1: now
assume
A2: for a,b holds a,b '||' f.a,f.b;
for a,b holds [[a,b],[f.a,f.b]] in lambda (the CONGR of OAS)
by A2,DIRAF:18;
then f is_FormalIz_of lambda(the CONGR of OAS);
hence f is dilatation;
end;
now
assume
A3: f is dilatation;
let a,b;
f is_FormalIz_of lambda(the CONGR of OAS) by A3;
then [[a,b],[f.a,f.b]] in lambda(the CONGR of OAS);
hence a,b '||' f.a,f.b by DIRAF:18;
end;
hence thesis by A1;
end;
theorem
f is positive_dilatation or f is negative_dilatation implies f is dilatation
proof
assume
A1: f is positive_dilatation or f is negative_dilatation;
now
let x,y;
x,y // f.x,f.y or x,y // f.y,f.x by A1,Th27;
hence x,y '||' f.x,f.y by DIRAF:def 4;
end;
hence thesis by Th34;
end;
theorem
for f being Permutation of the carrier of OAS st f is dilatation ex f9
being Permutation of the carrier of Lambda(OAS) st f=f9 & f9 is_DIL_of Lambda(
OAS)
proof
let f be Permutation of the carrier of OAS;
A1: Lambda(OAS) = AffinStruct(#the carrier of OAS, lambda(the CONGR of OAS)
#) by DIRAF:def 2;
then reconsider f9=f as Permutation of the carrier of Lambda(OAS);
assume f is dilatation;
then
A2: f is_FormalIz_of lambda(the CONGR of OAS);
take f9;
thus thesis by A2,A1;
end;
theorem
for f being Permutation of the carrier of Lambda(OAS) st f is_DIL_of
Lambda(OAS) ex f9 being Permutation of the carrier of OAS st f=f9 & f9 is
dilatation
proof
let f be Permutation of the carrier of Lambda(OAS);
A1: Lambda(OAS) = AffinStruct(#the carrier of OAS, lambda(the CONGR of OAS)
#) by DIRAF:def 2;
then reconsider f9=f as Permutation of the carrier of OAS;
assume f is_DIL_of Lambda(OAS);
then
A2: f is_FormalIz_of the CONGR of Lambda(OAS);
take f9;
thus thesis by A2,A1;
end;
theorem
id the carrier of OAS is dilatation
proof
for x,y
holds x,y '||' (id the carrier of OAS).x,(id the carrier of OAS).y
by DIRAF:19;
hence thesis by Th34;
end;
theorem
f is positive_dilatation or f is negative_dilatation implies f is dilatation
proof
assume
A1: f is positive_dilatation or f is negative_dilatation;
now
let x,y;
x,y // f.x,f.y or x,y // f.y,f.x by A1,Th27;
hence x,y '||' f.x,f.y by DIRAF:def 4;
end;
hence thesis by Th34;
end;
theorem
for f being Permutation of the carrier of OAS st f is dilatation ex f9
being Permutation of the carrier of Lambda(OAS) st f=f9 & f9 is_DIL_of Lambda(
OAS)
proof
let f be Permutation of the carrier of OAS;
A1: Lambda(OAS) = AffinStruct(#the carrier of OAS, lambda(the CONGR of OAS)
#) by DIRAF:def 2;
then reconsider f9=f as Permutation of the carrier of Lambda(OAS);
assume f is dilatation;
then
A2: f is_FormalIz_of lambda(the CONGR of OAS);
take f9;
thus thesis by A2,A1;
end;
theorem
for f being Permutation of the carrier of Lambda(OAS) st f is_DIL_of
Lambda(OAS) ex f9 being Permutation of the carrier of OAS st f=f9 & f9 is
dilatation
proof
let f be Permutation of the carrier of Lambda(OAS);
A1: Lambda(OAS) = AffinStruct(#the carrier of OAS, lambda(the CONGR of OAS)
#) by DIRAF:def 2;
then reconsider f9=f as Permutation of the carrier of OAS;
assume f is_DIL_of Lambda(OAS);
then
A2: f is_FormalIz_of the CONGR of Lambda(OAS);
take f9;
thus thesis by A2,A1;
end;
theorem
id the carrier of OAS is dilatation
proof
for x,y holds x,y '||' (id the carrier of OAS).x,(id the carrier of OAS).y
by DIRAF:19;
hence thesis by Th34;
end;
theorem Th43:
f is dilatation implies f" is dilatation
proof
assume
A1: f is dilatation;
now
let x,y;
set x9=f".x;
set y9=f".y;
f.x9=x & f.y9=y by Th2;
then x9,y9 '||' x,y by A1,Th34;
hence x,y '||' f".x,f".y by DIRAF:22;
end;
hence thesis by Th34;
end;
theorem Th44:
f is dilatation & g is dilatation implies f*g is dilatation
proof
assume
A1: f is dilatation & g is dilatation;
now
let x,y;
set x9=g.x;
set y9=g.y;
A2: (f*g).x= f.x9 & (f*g).y=f.y9 by FUNCT_2:15;
A3: now
assume x9=y9;
then x=y by FUNCT_2:58;
hence x,y '||' (f*g).x,(f*g).y by DIRAF:20;
end;
x,y '||' x9,y9 & x9,y9 '||' f.x9,f.y9 by A1,Th34;
hence x,y '||' (f*g).x,(f*g).y by A2,A3,DIRAF:23;
end;
hence thesis by Th34;
end;
theorem Th45:
f is dilatation implies for a,b,c,d holds a,b '||' c,d iff f.a,f
.b '||' f.c,f.d
proof
assume
A1: f is dilatation;
let a,b,c,d;
A2: c,d '||' f.c,f.d by A1,Th34;
A3: a,b '||' f.a,f.b by A1,Th34;
A4: now
A5: now
A6: now
assume f.c = f.d;
then c = d by FUNCT_2:58;
hence a,b '||' c,d by DIRAF:20;
end;
assume a,b '||' f.c,f.d;
hence a,b '||' c,d by A2,A6,DIRAF:23;
end;
A7: now
assume f.a=f.b;
then a=b by FUNCT_2:58;
hence a,b '||' c,d by DIRAF:20;
end;
assume f.a,f.b '||' f.c,f.d;
hence a,b '||' c,d by A3,A7,A5,DIRAF:23;
end;
now
A8: now
A9: c = d implies f.a,f.b '||' f.c,f.d by DIRAF:20;
assume f.a,f.b '||' c,d;
hence f.a,f.b '||' f.c,f.d by A2,A9,DIRAF:23;
end;
assume a,b '||' c,d;
then f.a,f.b '||' c,d or a=b by A3,DIRAF:23;
hence f.a,f.b '||' f.c,f.d by A8,DIRAF:20;
end;
hence thesis by A4;
end;
theorem Th46:
f is dilatation implies
for a,b,c holds a,b,c are_collinear iff f.a,f.b,f.c are_collinear
proof
assume
A1: f is dilatation;
let a,b,c;
a,b '||' a,c iff f.a,f.b '||' f.a,f.c by A1,Th45;
hence thesis by DIRAF:def 5;
end;
theorem Th47:
f is dilatation & x,f.x,y are_collinear implies x,f.x,f.y are_collinear
proof
assume
A1: f is dilatation;
assume
A2: x,f.x,y are_collinear;
now
assume
A3: x<>y;
x,f.x '||' x,y & x,y '||' f.x,f.y by A1,A2,Th34,DIRAF:def 5;
then x,f.x '||' f.x,f.y by A3,DIRAF:23;
then f.x,x '||' f.x,f.y by DIRAF:22;
then f.x,x,f.y are_collinear by DIRAF:def 5;
hence thesis by DIRAF:30;
end;
hence thesis by DIRAF:31;
end;
theorem Th48:
a,b '||' c,d implies
(a,c '||' b,d or ex x st a,c,x are_collinear & b,d,x are_collinear )
proof
assume
A1: a,b '||' c,d;
assume
A2: not a,c '||' b,d;
A3: now
consider z such that
A4: a,b '||' c,z and
A5: a,c '||' b,z by DIRAF:26;
assume
A6: a<>b;
A7: now
c,d '||' c,z by A1,A6,A4,DIRAF:23;
then c,d,z are_collinear by DIRAF:def 5;
then d,c,z are_collinear by DIRAF:30;
then d,c '||' d,z by DIRAF:def 5;
then z,d '||' d,c by DIRAF:22;
then consider t such that
A8: b,d '||' d,t and
A9: b,z '||' c,t by A2,A5,DIRAF:27;
assume b<>z;
then a,c '||' c,t by A5,A9,DIRAF:23;
then c,a '||' c,t by DIRAF:22;
then c,a,t are_collinear by DIRAF:def 5;
then
A10: a,c,t are_collinear by DIRAF:30;
d,b '||' d,t by A8,DIRAF:22;
then d,b,t are_collinear by DIRAF:def 5;
then b,d,t are_collinear by DIRAF:30;
hence thesis by A10;
end;
now
assume b=z;
then b,a '||' b,c by A4,DIRAF:22;
then b,a,c are_collinear by DIRAF:def 5;
then
A11: a,c,b are_collinear by DIRAF:30;
b,d,b are_collinear by DIRAF:31;
hence thesis by A11;
end;
hence thesis by A7;
end;
now
assume a=b;
then a,c,a are_collinear & b,d,a are_collinear by DIRAF:31;
hence thesis;
end;
hence thesis by A3;
end;
theorem Th49:
f is dilatation implies ((f=id the carrier of OAS or for x holds
f.x<>x) iff for x,y holds x,f.x '||' y,f.y )
proof
assume
A1: f is dilatation;
A2: now
assume
A3: for x,y holds x,f.x '||' y,f.y;
assume f<>(id the carrier of OAS);
then consider y such that
A4: f.y<>(id the carrier of OAS).y by FUNCT_2:63;
given x such that
A5: f.x=x;
x<>y by A5,A4;
then consider z such that
A6: not x,y,z are_collinear by DIRAF:37;
x,z '||' f.x,f.z by A1,Th34;
then x,z,f.z are_collinear by A5,DIRAF:def 5;
then
A7: z,f.z,x are_collinear by DIRAF:30;
z,f.z,z are_collinear by DIRAF:31;
then
A8: z,f.z '||' x,z by A7,DIRAF:34;
A9: f.y<>y by A4;
x,y '||' f.x,f.y by A1,Th34;
then
A10: x,y,f.y are_collinear by A5,DIRAF:def 5;
then y,x,f.y are_collinear by DIRAF:30;
then
A11: y,x '||' y,f.y by DIRAF:def 5;
A12: y,f.y,x are_collinear by A10,DIRAF:30;
A13: now
assume z=f.z;
then z,y '||' z,f.y by A1,Th34;
then z,y,f.y are_collinear by DIRAF:def 5;
then y,f.y,y are_collinear & y,f.y,z are_collinear by DIRAF:30,31;
hence contradiction by A9,A12,A6,DIRAF:32;
end;
y,f.y '||' z,f.z by A3;
then y,f.y '||' x,z by A13,A8,DIRAF:23;
then y,x '||' x,z by A9,A11,DIRAF:23;
then x,y '||' x,z by DIRAF:22;
hence contradiction by A6,DIRAF:def 5;
end;
now
assume
A14: f=(id the carrier of OAS) or for z holds f.z<>z;
let x,y;
A15: x,y '||' f.x,f.y by A1,Th34;
A16: now
assume
A17: for z holds f.z<>z;
assume
A18: not x,f.x '||' y,f.y;
then consider z such that
A19: x,f.x,z are_collinear and
A20: y,f.y,z are_collinear by A15,Th48;
set t=f.z;
x,f.x,t are_collinear by A1,A19,Th47;
then
A21: x,f.x '||' z,t by A19,DIRAF:34;
y,f.y,t are_collinear by A1,A20,Th47;
then
A22: y,f.y '||' z,t by A20,DIRAF:34;
z<>t by A17;
hence contradiction by A18,A21,A22,DIRAF:23;
end;
f=(id the carrier of OAS) implies x,f.x '||' y,f.y by DIRAF:20;
hence x,f.x '||' y,f.y by A14,A16;
end;
hence thesis by A2;
end;
theorem Th50:
f is dilatation & f.a=a & f.b=b & not a,b,x are_collinear implies f.x=x
proof
assume that
A1: f is dilatation and
A2: f.a=a and
A3: f.b=b and
A4: not a,b,x are_collinear;
a,x '||' a,f.x by A1,A2,Th34;
then a,x,f.x are_collinear by DIRAF:def 5;
then
A5: x,f.x,a are_collinear by DIRAF:30;
b,x '||' b,f.x by A1,A3,Th34;
then b,x,f.x are_collinear by DIRAF:def 5;
then
A6: x,f.x,x are_collinear & x,f.x,b are_collinear by DIRAF:30,31;
assume f.x<>x;
hence contradiction by A4,A5,A6,DIRAF:32;
end;
theorem Th51:
f is dilatation & f.a=a & f.b=b & a<>b implies f=(id the carrier of OAS)
proof
assume that
A1: f is dilatation and
A2: f.a=a and
A3: f.b=b and
A4: a<>b;
now
let x;
A5: now
assume
A6: a,b,x are_collinear;
now
consider z such that
A7: not a,b,z are_collinear by A4,DIRAF:37;
assume
A8: x<>a;
A9: not a,z,x are_collinear
proof
assume a,z,x are_collinear;
then
A10: a,x,z are_collinear by DIRAF:30;
a,x,a are_collinear & a,x,b are_collinear by A6,DIRAF:30,31;
hence contradiction by A8,A7,A10,DIRAF:32;
end;
f.z=z by A1,A2,A3,A7,Th50;
hence f.x=x by A1,A2,A9,Th50;
end;
hence f.x=x by A2;
end;
not a,b,x are_collinear implies f.x=x by A1,A2,A3,Th50;
hence f.x=(id the carrier of OAS).x by A5;
end;
hence thesis by FUNCT_2:63;
end;
theorem
f is dilatation & g is dilatation & f.a=g.a & f.b=g.b implies a=b or f =g
proof
assume that
A1: f is dilatation and
A2: g is dilatation and
A3: f.a=g.a and
A4: f.b=g.b;
A5: (g"*f).b=g".(g.b) by A4,FUNCT_2:15
.=b by Th2;
A6: g" is dilatation by A2,Th43;
assume
A7: a<>b;
(g"*f).a=g".(g.a) by A3,FUNCT_2:15
.=a by Th2;
then
A8: g"*f=(id the carrier of OAS) by A1,A7,A5,A6,Th44,Th51;
now
let x;
g".(f.x)=(g"*f).x by FUNCT_2:15;
then g".(f.x)=x by A8;
hence g.x=f.x by Th2;
end;
hence thesis by FUNCT_2:63;
end;
definition
let OAS;
let f be Permutation of the carrier of OAS;
attr f is translation means
f is dilatation & (f = id the carrier of OAS or for a holds a<>f.a);
end;
theorem Th53:
f is dilatation implies (f is translation iff for x,y holds x,f.
x '||' y,f.y )
by Th49;
theorem Th54:
f is translation & g is translation & f.a=g.a & not a,f.a,x are_collinear
implies f.x=g.x
proof
assume that
A1: f is translation and
A2: g is translation and
A3: f.a=g.a and
A4: not a,f.a,x are_collinear;
set b=f.a, y=f.x, z=g.x;
A5: a,x '||' b,z & a,b '||' x,z by A2,A3,Th34,Th53;
f is dilatation by A1;
then
A6: a,x '||' b,y by Th34;
a,b '||' x,y by A1,Th53;
hence thesis by A4,A6,A5,PASCH:5;
end;
theorem Th55:
f is translation & g is translation & f.a=g.a implies f=g
proof
assume that
A1: f is translation and
A2: g is translation and
A3: f.a=g.a;
set b=f.a;
A4: f is dilatation by A1;
A5: now
assume
A6: a<>b;
for x holds f.x=g.x
proof
let x;
now
assume
A7: a,b,x are_collinear;
now
A8: f<>(id the carrier of OAS) by A6;
then
A9: f.x<>x by A1;
assume x<>a;
consider p such that
A10: not a,b,p are_collinear by A6,DIRAF:37;
A11: f.p<>p by A1,A8;
A12: not p,f.p,x are_collinear
proof
A13: a,b,f.x are_collinear by A4,A7,Th47;
a,b,a are_collinear by DIRAF:31;
then
A14: x,f.x,a are_collinear by A6,A7,A13,DIRAF:32;
A15: p,f.p,p are_collinear by DIRAF:31;
a,b,b are_collinear by DIRAF:31;
then
A16: x,f.x,b are_collinear by A6,A7,A13,DIRAF:32;
assume
A17: p,f.p,x are_collinear;
then p,f.p,f.x are_collinear by A4,Th47;
then x,f.x,p are_collinear by A11,A17,A15,DIRAF:32;
hence contradiction by A10,A9,A14,A16,DIRAF:32;
end;
f.p=g.p by A1,A2,A3,A10,Th54;
hence thesis by A1,A2,A12,Th54;
end;
hence thesis by A3;
end;
hence thesis by A1,A2,A3,Th54;
end;
hence thesis by FUNCT_2:63;
end;
b=a implies thesis by A1,A2,A3;
hence thesis by A5;
end;
theorem Th56:
f is translation implies f" is translation
proof
A1: now
assume
A2: for x holds f.x<>x;
given y such that
A3: f".y=y;
f.y=y by A3,Th2;
hence contradiction by A2;
end;
assume
A4: f is translation;
then f is dilatation;
then
A5: f" is dilatation by Th43;
f=(id the carrier of OAS) implies f"=(id the carrier of OAS) by FUNCT_1:45;
hence thesis by A4,A5,A1;
end;
theorem
f is translation & g is translation implies (f*g) is translation
proof
assume that
A1: f is translation and
A2: g is translation;
f is dilatation & g is dilatation by A1,A2;
then
A3: (f*g) is dilatation by Th44;
now
assume
A4: (f*g)<>(id the carrier of OAS);
for x holds (f*g).x<>x
proof
given x such that
A5: (f*g).x=x;
f.(g.x)=x by A5,FUNCT_2:15;
then
A6: g.x=f".x by Th2;
f" is translation by A1,Th56;
then f*g=f*f" by A2,A6,Th55;
hence contradiction by A4,FUNCT_2:61;
end;
hence thesis by A3;
end;
hence thesis by A3;
end;
Lm5: f is translation & not a,f.a,b are_collinear implies
a,b // f.a,f.b & a,f.a // b,f.b
proof
assume that
A1: f is translation and
A2: not a,f.a,b are_collinear;
f is dilatation by A1;
then
A3: a,b '||' f.a,f.b by Th34;
a,f.a '||' b,f.b by A1,Th53;
hence thesis by A2,A3,PASCH:14;
end;
Lm6: f is translation & a<>f.a & a,f.a,b are_collinear implies a,f.a // b,f.b
proof
assume that
A1: f is translation and
A2: a<>f.a and
A3: a,f.a,b are_collinear;
consider p such that
A4: not a,f.a,p are_collinear by A2,DIRAF:37;
A5: f is dilatation by A1;
A6: f<>(id the carrier of OAS) by A2;
then
A7: p<>f.p by A1;
A8: b<>f.b by A1,A6;
not p,f.p,b are_collinear
proof
A9: p,f.p,p are_collinear by DIRAF:31;
assume
A10: p,f.p,b are_collinear;
then p,f.p,f.b are_collinear by A5,Th47;
then
A11: b,f.b,p are_collinear by A7,A10,A9,DIRAF:32;
a,f.a,f.b are_collinear & a,f.a,a are_collinear by A3,A5,Th47,DIRAF:31;
then
A12: b,f.b,a are_collinear by A2,A3,DIRAF:32;
then b,f.b,f.a are_collinear by A5,Th47;
hence contradiction by A4,A8,A12,A11,DIRAF:32;
end;
then
A13: p,f.p // b,f.b by A1,Lm5;
not p,f.p,a are_collinear
proof
assume
A14: p,f.p,a are_collinear;
then p,f.p,p are_collinear & p,f.p,f.a are_collinear by A5,Th47,DIRAF:31;
hence contradiction by A4,A7,A14,DIRAF:32;
end;
then p,f.p // a,f.a by A1,Lm5;
hence thesis by A7,A13,ANALOAF:def 5;
end;
Lm7: f is translation & Mid a,f.a,b & a<>f.a implies a,b // f.a,f.b
proof
assume that
A1: f is translation and
A2: Mid a,f.a,b and
A3: a<>f.a;
A4: a,f.a // b,f.b by A1,A2,A3,Lm6,DIRAF:28;
now
Mid b,f.a,a by A2,DIRAF:9;
then b,f.a // f.a,a by DIRAF:def 3;
then b,f.a // b,a by ANALOAF:def 5;
then
A5: a,b // f.a,b by DIRAF:2;
a,f.a // f.a,b by A2,DIRAF:def 3;
then f.a,b // b,f.b by A3,A4,ANALOAF:def 5;
then
A6: f.a,b // f.a,f.b by ANALOAF:def 5;
assume b<>f.a;
hence thesis by A5,A6,DIRAF:3;
end;
hence thesis by A1,A2,A3,Lm6,DIRAF:28;
end;
Lm8: f is translation & a<>f.a & b<>f.a & Mid a,b,f.a implies a,b // f.a,f.b
proof
assume that
A1: f is translation and
A2: a<>f.a and
A3: b<>f.a and
A4: Mid a,b,f.a;
A5: a,b // b,f.a by A4,DIRAF:def 3;
A6: f is dilatation by A1;
A7: a,b,f.a are_collinear by A4,DIRAF:28;
then
A8: a,f.a,b are_collinear by DIRAF:30;
A9: f<>(id the carrier of OAS) by A2;
now
assume
A10: a<>b;
A11: now
f.a,a,b are_collinear by A7,DIRAF:30;
then f.a,a '||' f.a,b by DIRAF:def 5;
then
A12: a,f.a '||' b,f.a by DIRAF:22;
consider q such that
A13: not a,f.a,q are_collinear by A2,DIRAF:37;
consider x such that
A14: q,b // b,x and
A15: q,a // f.a,x by A5,A10,ANALOAF:def 5;
A16: a,q // x,f.a by A15,DIRAF:2;
A17: Mid q,b,x by A14,DIRAF:def 3;
then
A18: x,b,q are_collinear by DIRAF:9,28;
A19: x<>f.a
proof
assume x=f.a;
then Mid q,b,f.a by A14,DIRAF:def 3;
then q,b,f.a are_collinear by DIRAF:28;
then
A20: f.a,b,q are_collinear by DIRAF:30;
A21: a,b,a are_collinear by DIRAF:31;
f.a,b,a are_collinear & f.a,b,b are_collinear by A7,DIRAF:30,31;
then a,b,q are_collinear by A3,A20,DIRAF:32;
hence contradiction by A7,A10,A13,A21,DIRAF:32;
end;
A22: not x,f.a,b are_collinear
proof
assume x,f.a,b are_collinear;
then f.a,x,b are_collinear by DIRAF:30;
then
A23: f.a,x '||' f.a,b by DIRAF:def 5;
f.a,b,a are_collinear by A7,DIRAF:30;
then
A24: f.a,b '||' f.a,a by DIRAF:def 5;
q,a '||' f.a,x by A15,DIRAF:def 4;
then f.a,b '||' q,a by A19,A23,DIRAF:23;
then f.a,a '||' q,a by A3,A24,DIRAF:23;
then a,f.a '||' a,q by DIRAF:22;
hence contradiction by A13,DIRAF:def 5;
end;
a,f.a // q,f.q by A1,A13,Lm5;
then a,f.a '||' q,f.q by DIRAF:def 4;
then b,f.a '||' q,f.q by A2,A12,DIRAF:23;
then
A25: f.a,b '||' q,f.q by DIRAF:22;
A26: a,f.a,f.b are_collinear by A6,A8,Th47;
a,q // f.a,f.q & a<>q by A1,A13,Lm5,DIRAF:31;
then f.a,f.q // x,f.a by A16,ANALOAF:def 5;
then f.a,f.q '||' f.a,x by DIRAF:def 4;
then f.a,f.q,x are_collinear by DIRAF:def 5;
then
A27: x,f.a,f.q are_collinear by DIRAF:30;
A28: b<>f.b by A1,A9;
a,f.a,f.a are_collinear by DIRAF:31;
then
A29: b,f.b,f.a are_collinear by A2,A8,A26,DIRAF:32;
a,f.a,a are_collinear by DIRAF:31;
then b,f.b,a are_collinear by A2,A8,A26,DIRAF:32;
then
A30: not b,f.b,q are_collinear by A13,A29,A28,DIRAF:32;
A31: not b,f.b,f.q are_collinear
proof
b,f.b '||' q,f.q by A1,Th53;
then
A32: b,f.b '||' f.q,q by DIRAF:22;
assume b,f.b,f.q are_collinear;
hence contradiction by A28,A30,A32,DIRAF:33;
end;
then
A33: f.b<>f.q by DIRAF:31;
a,b // a,f.a & a,f.a // b,f.b by A1,A8,A5,Lm6,ANALOAF:def 5;
then
A34: a,b // b,f.b by A2,DIRAF:3;
assume a,b // f.b,f.a;
then b,f.b // f.b,f.a by A10,A34,ANALOAF:def 5;
then Mid b,f.b,f.a by DIRAF:def 3;
then
A35: Mid f.a,f.b,b by DIRAF:9;
A36: x,b,b are_collinear by DIRAF:31;
Mid x,b,q by A17,DIRAF:9;
then Mid x,f.a,f.q by A22,A27,A25,PASCH:8;
then consider y such that
A37: Mid x,y,b and
A38: Mid y,f.b,f.q by A35,A22,PASCH:27;
x,y,b are_collinear by A37,DIRAF:28;
then
A39: x,b,y are_collinear by DIRAF:30;
A40: x<>b by A22,DIRAF:31;
then b,q,y are_collinear by A18,A39,A36,DIRAF:32;
then
A41: b,q '||' b,y by DIRAF:def 5;
A42: y,f.b,f.q are_collinear by A38,DIRAF:28;
then f.b,f.q,y are_collinear by DIRAF:30;
then
A43: f.b,f.q '||' f.b,y by DIRAF:def 5;
b,q '||' f.b,f.q by A6,Th34;
then b,q '||' f.b,y by A33,A43,DIRAF:23;
then f.b,y '||' b,y by A33,A41,DIRAF:23;
then y,b '||' y,f.b by DIRAF:22;
then
A44: y,b,f.b are_collinear by DIRAF:def 5;
A45: y,b,b are_collinear by DIRAF:31;
y,b,q are_collinear by A40,A18,A39,A36,DIRAF:32;
hence contradiction by A42,A30,A31,A44,A45,DIRAF:32;
end;
a,b '||' f.a,f.b by A6,Th34;
hence thesis by A11,DIRAF:def 4;
end;
hence thesis by DIRAF:4;
end;
Lm9: f is translation & a<>f.a & a,f.a,b are_collinear implies a,b // f.a,f.b
proof
assume that
A1: f is translation and
A2: a<>f.a and
A3: a,f.a,b are_collinear;
f<>(id the carrier of OAS) by A2;
then
A4: b<>f.b by A1;
A5: f is dilatation by A1;
now
assume
A6: a<>b;
A7: now
assume
A8: Mid f.a,a,b;
A9: now
assume Mid f.b,b,a;
then Mid a,b,f.b by DIRAF:9;
then a,b // b,f.b by DIRAF:def 3;
then
A10: a,b // a,f.b by ANALOAF:def 5;
Mid b,a,f.a by A8,DIRAF:9;
then b,a // a,f.a by DIRAF:def 3;
then
A11: a,b // f.a,a by ANALOAF:def 5;
then f.a,a // a,f.b by A6,A10,ANALOAF:def 5;
then f.a,a // f.a,f.b by ANALOAF:def 5;
hence thesis by A10,A11,DIRAF:3;
end;
A12: now
A13: now
assume
A14: a=f.b;
a,f.a // b,f.b by A1,A2,A3,Lm6;
hence thesis by A14,DIRAF:2;
end;
assume Mid b,a,f.b;
then b,a // f.b,f.a or a=f.b by A1,A4,Lm8;
hence thesis by A13,DIRAF:2;
end;
A15: now
assume Mid b,f.b,a;
then b,a // f.b,f.a by A1,A4,Lm7;
hence thesis by DIRAF:2;
end;
a,f.a,f.b are_collinear & a,f.a,a are_collinear by A3,A5,Th47,DIRAF:31;
hence thesis by A2,A3,A15,A12,A9,DIRAF:29,32;
end;
A16: now
assume
A17: Mid a,b,f.a;
b=f.a implies thesis by A1,A2,A3,Lm6;
hence thesis by A1,A2,A17,Lm8;
end;
Mid a,f.a,b implies thesis by A1,A2,Lm7;
hence thesis by A3,A7,A16,DIRAF:29;
end;
hence thesis by DIRAF:4;
end;
theorem Th58:
f is translation implies f is positive_dilatation
proof
assume
A1: f is translation;
A2: now
assume
A3: for x holds f.x<>x;
for a,b holds a,b // f.a,f.b
proof
let a,b;
A4: a<>f.a by A3;
not a,f.a,b are_collinear implies a,b // f.a,f.b by A1,Lm5;
hence thesis by A1,A4,Lm9;
end;
hence thesis by Th27;
end;
f=id the carrier of OAS implies thesis by Th28;
hence thesis by A1,A2;
end;
theorem Th59:
f is dilatation & f.p=p & Mid q,p,f.q & not p,q,x are_collinear
implies Mid x,p,f.x
proof
assume that
A1: f is dilatation and
A2: f.p=p and
A3: Mid q,p,f.q & not p,q,x are_collinear;
q,x '||' f.q,f.x by A1,Th34;
then
A4: q,x '||' f.x,f.q by DIRAF:22;
p,x '||' p,f.x by A1,A2,Th34;
then p,x,f.x are_collinear by DIRAF:def 5;
hence thesis by A3,A4,PASCH:6;
end;
theorem Th60:
f is dilatation & f.p=p & Mid q,p,f.q & q<>p implies Mid x,p,f.x
proof
assume that
A1: f is dilatation & f.p=p and
A2: Mid q,p,f.q and
A3: q<>p;
now
consider r such that
A4: not p,q,r are_collinear by A3,DIRAF:37;
assume
A5: p,q,x are_collinear;
A6: x=p or not p,r,x are_collinear
proof
A7: p,x,q are_collinear & p,x,p are_collinear by A5,DIRAF:30,31;
assume that
A8: x<>p and
A9: p,r,x are_collinear;
p,x,r are_collinear by A9,DIRAF:30;
hence contradiction by A4,A8,A7,DIRAF:32;
end;
Mid r,p,f.r by A1,A2,A4,Th59;
hence thesis by A1,A6,Th59,DIRAF:10;
end;
hence thesis by A1,A2,Th59;
end;
theorem Th61:
f is dilatation & f.p=p & q<>p & Mid q,p,f.q & not p,x,y are_collinear
implies x,y // f.y,f.x
proof
assume
A1: f is dilatation;
assume
A2: f.p=p & q<>p & Mid q,p,f.q;
then Mid x,p,f.x by A1,Th60;
then
A3: x,p // p,f.x by DIRAF:def 3;
Mid y,p,f.y by A1,A2,Th60;
then
A4: y,p // p,f.y by DIRAF:def 3;
x,y '||' f.x,f.y by A1,Th34;
hence thesis by A3,A4,PASCH:12;
end;
theorem Th62:
f is dilatation & f.p=p & q<>p & Mid q,p,f.q & p,x,y are_collinear implies
x,y // f.y,f.x
proof
assume that
A1: f is dilatation and
A2: f.p=p and
A3: q<>p & Mid q,p,f.q and
A4: p,x,y are_collinear;
A5: Mid y,p,f.y by A1,A2,A3,Th60;
A6: now
assume
A7: x=p;
then y,x // x,f.y by A5,DIRAF:def 3;
hence thesis by A2,A7,DIRAF:2;
end;
A8: now
assume that
A9: x<>p and
y<>p and
A10: x<>y;
consider u such that
A11: not p,x,u are_collinear by A9,DIRAF:37;
consider r such that
A12: x,y '||' u,r and
A13: x,u '||' y,r by DIRAF:26;
A14: not x,y,u are_collinear
proof
assume
A15: x,y,u are_collinear;
x,y,p are_collinear & x,y,x are_collinear by A4,DIRAF:30,31;
hence contradiction by A10,A11,A15,DIRAF:32;
end;
then
A16: x,y // u,r by A12,A13,PASCH:14;
A17: not p,u,r are_collinear
proof
A18: now
assume u=r;
then u,x '||' u,y by A13,DIRAF:22;
then u,x,y are_collinear by DIRAF:def 5;
hence contradiction by A14,DIRAF:30;
end;
x,y,p are_collinear by A4,DIRAF:30;
then x,y '||' x,p by DIRAF:def 5;
then x,y '||' p,x by DIRAF:22;
then
A19: u,r '||' p,x by A10,A12,DIRAF:23;
A20: u,r,u are_collinear by DIRAF:31;
assume p,u,r are_collinear;
then
A21: u,r,p are_collinear by DIRAF:30;
p,x '||' p,y by A4,DIRAF:def 5;
then u,r '||' p,y by A9,A19,DIRAF:23;
then
A22: u,r,y are_collinear by A18,A21,DIRAF:33;
u,r,x are_collinear by A18,A21,A19,DIRAF:33;
hence contradiction by A14,A18,A22,A20,DIRAF:32;
end;
then
A23: u<>r by DIRAF:31;
set u9=f.u, r9=f.r, x9=f.x, y9=f.y;
A24: not x9,y9,u9 are_collinear by A1,A14,Th46;
x9,y9 '||' u9,r9 & x9,u9 '||' y9,r9 by A1,A12,A13,Th45;
then x9,y9 // u9,r9 by A24,PASCH:14;
then
A25: r9,u9 // y9,x9 by DIRAF:2;
u,r // f.r,f.u by A1,A2,A3,A17,Th61;
then x,y // r9,u9 by A16,A23,DIRAF:3;
hence thesis by A25,A23,DIRAF:3,FUNCT_2:58;
end;
Mid x,p,f.x by A1,A2,A3,Th60;
hence thesis by A2,A6,A8,DIRAF:4,def 3;
end;
theorem Th63:
f is dilatation & f.p=p & q<>p & Mid q,p,f.q implies f is negative_dilatation
proof
assume
A1: f is dilatation & f.p=p & q<>p & Mid q,p,f.q;
x,y // f.y,f.x
proof
not p,x,y are_collinear implies x,y // f.y,f.x by A1,Th61;
hence thesis by A1,Th62;
end;
hence thesis;
end;
theorem Th64:
f is dilatation & f.p=p & (for x holds p,x // p,f.x) implies for
y,z holds y,z // f.y,f.z
proof
assume that
A1: f is dilatation and
A2: f.p=p and
A3: p,x // p,f.x;
A4: not p,y,z are_collinear implies y,z // f.y,f.z
proof
assume
A5: not p,y,z are_collinear;
A6: p,y // p,f.y & p,z // p,f.z by A3;
y,z '||' f.y,f.z by A1,Th34;
hence thesis by A5,A6,PASCH:13;
end;
let y,z;
p,y,z are_collinear implies y,z // f.y,f.z
proof
assume
A7: p,y,z are_collinear;
A8: now
assume that
A9: p<>y and
A10: y<>z and
z<>p;
consider q such that
A11: not p,y,q are_collinear by A9,DIRAF:37;
A12: not y,z,q are_collinear
proof
assume
A13: y,z,q are_collinear;
y,z,p are_collinear & y,z,y are_collinear by A7,DIRAF:30,31;
hence contradiction by A10,A11,A13,DIRAF:32;
end;
then
A14: not f.y,f.z,f.q are_collinear by A1,Th46;
consider r such that
A15: y,z '||' q,r and
A16: y,q '||' z,r by DIRAF:26;
f.y,f.z '||' f.q,f.r & f.y,f.q '||' f.z,f.r by A1,A15,A16,Th45;
then f.y,f.z // f.q,f.r by A14,PASCH:14;
then
A17: f.q,f.r // f.y,f.z by DIRAF:2;
A18: q<>r
proof
assume q=r;
then q,y '||' q,z by A16,DIRAF:22;
then q,y,z are_collinear by DIRAF:def 5;
hence contradiction by A12,DIRAF:30;
end;
not p,q,r are_collinear
proof
A19: q,r,q are_collinear by DIRAF:31;
assume p,q,r are_collinear;
then
A20: q,r,p are_collinear by DIRAF:30;
y,p,z are_collinear by A7,DIRAF:30;
then y,p '||' y,z by DIRAF:def 5;
then y,z '||' p,y by DIRAF:22;
then q,r '||' p,y by A10,A15,DIRAF:23;
then q,r,y are_collinear by A18,A20,DIRAF:33;
hence contradiction by A11,A18,A20,A19,DIRAF:32;
end;
then
A21: q,r // f.q,f.r by A4;
y,z // q,r by A15,A16,A12,PASCH:14;
then y,z // f.q,f.r by A18,A21,DIRAF:3;
hence thesis by A18,A17,DIRAF:3,FUNCT_2:58;
end;
now
assume p=z;
then z,y // f.z,f.y by A2,A3;
hence thesis by DIRAF:2;
end;
hence thesis by A2,A3,A8,DIRAF:4;
end;
hence thesis by A4;
end;
theorem
f is dilatation implies f is positive_dilatation or f is negative_dilatation
proof
assume
A1: f is dilatation;
A2: now
given p such that
A3: f.p=p;
A4: now
given q such that
A5: not p,q // p,f.q;
p,q '||' p,f.q by A1,A3,Th34;
then
A6: p,q // f.q,p by A5,DIRAF:def 4;
then q,p // p,f.q by DIRAF:2;
then
A7: Mid q,p,f.q by DIRAF:def 3;
p<>q by A5,A6,DIRAF:2;
hence f is negative_dilatation by A1,A3,A7,Th63;
end;
now
assume for x holds p,x // p,f.x;
then for x,y holds x,y // f.x,f.y by A1,A3,Th64;
hence f is positive_dilatation by Th27;
end;
hence thesis by A4;
end;
now
assume for x holds f.x<>x;
then f is translation by A1;
hence f is positive_dilatation by Th58;
end;
hence thesis by A2;
end;
reserve AFS for AffinSpace;
reserve a,b,c,d,d1,d2,p,x,y,z,t for Element of AFS;
theorem Th66:
AFS is CongrSpace-like
by AFF_1:5,AFF_1:3,AFF_1:4,AFF_1:2;
theorem
Lambda(OAS) is CongrSpace
proof
Lambda(OAS) is AffinSpace by DIRAF:41;
hence thesis by Th66;
end;
reserve f,g for Permutation of the carrier of AFS;
definition
let AFS;
let f;
attr f is dilatation means
f is_DIL_of AFS;
end;
theorem Th68:
f is dilatation iff for a,b holds a,b // f.a,f.b
by Th22;
theorem Th69:
id the carrier of AFS is dilatation
proof
for x,y holds
x,y // (id the carrier of AFS).x,(id the carrier of AFS).y by AFF_1:2;
hence thesis by Th68;
end;
theorem Th70:
f is dilatation implies f" is dilatation
proof
assume
A1: f is dilatation;
now
let x,y;
set x9=f".x;
set y9=f".y;
f.x9=x & f.y9=y by Th2;
then x9,y9 // x,y by A1,Th68;
hence x,y // f".x,f".y by AFF_1:4;
end;
hence thesis by Th68;
end;
theorem Th71:
f is dilatation & g is dilatation implies (f*g) is dilatation
proof
assume
A1: f is dilatation & g is dilatation;
now
let x,y;
set x9=g.x;
set y9=g.y;
A2: (f*g).x= f.x9 & (f*g).y=f.y9 by FUNCT_2:15;
A3: now
assume x9=y9;
then x=y by FUNCT_2:58;
hence x,y // (f*g).x,(f*g).y by AFF_1:3;
end;
x,y // x9,y9 & x9,y9 // f.x9,f.y9 by A1,Th68;
hence x,y // (f*g).x,(f*g).y by A2,A3,AFF_1:5;
end;
hence thesis by Th68;
end;
theorem Th72:
f is dilatation implies for a,b,c,d holds a,b // c,d iff f.a,f.b // f.c,f.d
proof
assume
A1: f is dilatation;
let a,b,c,d;
A2: c,d // f.c,f.d by A1,Th68;
A3: a,b // f.a,f.b by A1,Th68;
A4: now
A5: now
A6: now
assume f.c = f.d;
then c = d by FUNCT_2:58;
hence a,b // c,d by AFF_1:3;
end;
assume a,b // f.c,f.d;
hence a,b // c,d by A2,A6,AFF_1:5;
end;
A7: now
assume f.a=f.b;
then a=b by FUNCT_2:58;
hence a,b // c,d by AFF_1:3;
end;
assume f.a,f.b // f.c,f.d;
hence a,b // c,d by A3,A7,A5,AFF_1:5;
end;
now
A8: now
A9: c = d implies f.a,f.b // f.c,f.d by AFF_1:3;
assume f.a,f.b // c,d;
hence f.a,f.b // f.c,f.d by A2,A9,AFF_1:5;
end;
assume a,b // c,d;
then f.a,f.b // c,d or a=b by A3,AFF_1:5;
hence f.a,f.b // f.c,f.d by A8,AFF_1:3;
end;
hence thesis by A4;
end;
theorem
f is dilatation implies for a,b,c
holds LIN a,b,c iff LIN f.a,f.b,f.c
proof
assume
A1: f is dilatation;
let a,b,c;
a,b // a,c iff f.a,f.b // f.a,f.c by A1,Th72;
hence thesis by AFF_1:def 1;
end;
theorem Th74:
f is dilatation & LIN x,f.x,y implies LIN x,f.x,f.y
proof
assume
A1: f is dilatation;
assume
A2: LIN x,f.x,y;
now
assume
A3: x<>y;
x,f.x // x,y & x,y // f.x,f.y by A1,A2,Th68,AFF_1:def 1;
then x,f.x // f.x,f.y by A3,AFF_1:5;
then f.x,x // f.x,f.y by AFF_1:4;
then LIN f.x,x,f.y by AFF_1:def 1;
hence thesis by AFF_1:6;
end;
hence thesis by AFF_1:7;
end;
theorem Th75:
a,b // c,d implies (a,c // b,d or ex x st LIN a,c,x & LIN b,d,x )
proof
assume
A1: a,b // c,d;
assume
A2: not a,c // b,d;
A3: now
consider z such that
A4: a,b // c,z and
A5: a,c // b,z by DIRAF:40;
assume
A6: a<>b;
A7: now
c,d // c,z by A1,A6,A4,AFF_1:5;
then LIN c,d,z by AFF_1:def 1;
then LIN d,c,z by AFF_1:6;
then d,c // d,z by AFF_1:def 1;
then z,d // d,c by AFF_1:4;
then consider t such that
A8: b,d // d,t and
A9: b,z // c,t by A2,A5,DIRAF:40;
assume b<>z;
then a,c // c,t by A5,A9,AFF_1:5;
then c,a // c,t by AFF_1:4;
then LIN c,a,t by AFF_1:def 1;
then
A10: LIN a,c,t by AFF_1:6;
d,b // d,t by A8,AFF_1:4;
then LIN d,b,t by AFF_1:def 1;
then LIN b,d,t by AFF_1:6;
hence thesis by A10;
end;
now
assume b=z;
then b,a // b,c by A4,AFF_1:4;
then LIN b,a,c by AFF_1:def 1;
then
A11: LIN a,c,b by AFF_1:6;
LIN b,d,b by AFF_1:7;
hence thesis by A11;
end;
hence thesis by A7;
end;
now
assume a=b;
then LIN a,c,a & LIN b,d,a by AFF_1:7;
hence thesis;
end;
hence thesis by A3;
end;
theorem Th76:
f is dilatation implies ((f=id the carrier of AFS or for x holds
f.x<>x) iff for x,y holds x,f.x // y,f.y )
proof
assume
A1: f is dilatation;
A2: now
assume
A3: for x,y holds x,f.x // y,f.y;
assume f<>(id the carrier of AFS);
then consider y such that
A4: f.y<>(id the carrier of AFS).y by FUNCT_2:63;
given x such that
A5: f.x=x;
x<>y by A5,A4;
then consider z such that
A6: not LIN x,y,z by AFF_1:13;
x,z // f.x,f.z by A1,Th68;
then LIN x,z,f.z by A5,AFF_1:def 1;
then
A7: LIN z,f.z,x by AFF_1:6;
LIN z,f.z,z by AFF_1:7;
then
A8: z,f.z // x,z by A7,AFF_1:10;
A9: f.y<>y by A4;
x,y // f.x,f.y by A1,Th68;
then
A10: LIN x,y,f.y by A5,AFF_1:def 1;
then LIN y,x,f.y by AFF_1:6;
then
A11: y,x // y,f.y by AFF_1:def 1;
A12: LIN y,f.y,x by A10,AFF_1:6;
A13: now
assume z=f.z;
then z,y //z,f.y by A1,Th68;
then LIN z,y,f.y by AFF_1:def 1;
then LIN y,f.y,y & LIN y,f.y,z by AFF_1:6,7;
hence contradiction by A9,A12,A6,AFF_1:8;
end;
y,f.y // z,f.z by A3;
then y,f.y // x,z by A13,A8,AFF_1:5;
then y,x // x,z by A9,A11,AFF_1:5;
then x,y // x,z by AFF_1:4;
hence contradiction by A6,AFF_1:def 1;
end;
now
assume
A14: f=id the carrier of AFS or for z holds f.z<>z;
let x,y;
A15: x,y // f.x,f.y by A1,Th68;
A16: now
assume
A17: for z holds f.z<>z;
assume
A18: not x,f.x // y,f.y;
then consider z such that
A19: LIN x,f.x,z and
A20: LIN y,f.y,z by A15,Th75;
set t=f.z;
LIN x,f.x,t by A1,A19,Th74;
then
A21: x,f.x // z,t by A19,AFF_1:10;
LIN y,f.y,t by A1,A20,Th74;
then
A22: y,f.y // z,t by A20,AFF_1:10;
z<>t by A17;
hence contradiction by A18,A21,A22,AFF_1:5;
end;
f=(id the carrier of AFS) implies x,f.x // y,f.y by AFF_1:3;
hence x,f.x // y,f.y by A14,A16;
end;
hence thesis by A2;
end;
theorem Th77:
f is dilatation & f.a=a & f.b=b & not LIN a,b,x implies f.x=x
proof
assume that
A1: f is dilatation and
A2: f.a=a and
A3: f.b=b and
A4: not LIN a,b,x;
a,x // a,f.x by A1,A2,Th68;
then LIN a,x,f.x by AFF_1:def 1;
then
A5: LIN x,f.x,a by AFF_1:6;
b,x // b,f.x by A1,A3,Th68;
then LIN b,x,f.x by AFF_1:def 1;
then
A6: LIN x,f.x,x & LIN x,f.x,b by AFF_1:6,7;
assume f.x<>x;
hence contradiction by A4,A5,A6,AFF_1:8;
end;
theorem Th78:
f is dilatation & f.a=a & f.b=b & a<>b implies f=id the carrier of AFS
proof
assume that
A1: f is dilatation and
A2: f.a=a and
A3: f.b=b and
A4: a<>b;
now
let x;
A5: now
assume
A6: LIN a,b,x;
now
consider z such that
A7: not LIN a,b,z by A4,AFF_1:13;
assume
A8: x<>a;
A9: not LIN a,z,x
proof
assume LIN a,z,x;
then
A10: LIN a,x,z by AFF_1:6;
LIN a,x,a & LIN a,x,b by A6,AFF_1:6,7;
hence contradiction by A8,A7,A10,AFF_1:8;
end;
f.z=z by A1,A2,A3,A7,Th77;
hence f.x=x by A1,A2,A9,Th77;
end;
hence f.x=x by A2;
end;
not LIN a,b,x implies f.x=x by A1,A2,A3,Th77;
hence f.x=(id the carrier of AFS).x by A5;
end;
hence thesis by FUNCT_2:63;
end;
theorem
f is dilatation & g is dilatation & f.a=g.a & f.b=g.b implies a=b or f =g
proof
assume that
A1: f is dilatation and
A2: g is dilatation and
A3: f.a=g.a and
A4: f.b=g.b;
A5: (g"*f).b=g".(g.b) by A4,FUNCT_2:15
.=b by Th2;
A6: g" is dilatation by A2,Th70;
assume
A7: a<>b;
(g"*f).a=g".(g.a) by A3,FUNCT_2:15
.=a by Th2;
then
A8: g"*f=(id the carrier of AFS) by A1,A7,A5,A6,Th71,Th78;
now
let x;
g".(f.x)=(g"*f).x by FUNCT_2:15;
then g".(f.x)=x by A8;
hence g.x=f.x by Th2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th80:
not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 & a,c //
b,d2 implies d1=d2
proof
assume that
A1: not LIN a,b,c and
A2: a,b // c,d1 and
A3: a,b // c,d2 and
A4: a,c // b,d1 and
A5: a,c // b,d2;
assume
A6: d1<>d2;
a<>c by A1,AFF_1:7;
then b,d1 // b,d2 by A4,A5,AFF_1:5;
then LIN b,d1,d2 by AFF_1:def 1;
then
A7: LIN d1,d2,b by AFF_1:6;
A8: now
assume c = d1;
then c,a // c,b by A4,AFF_1:4;
then LIN c,a,b by AFF_1:def 1;
hence contradiction by A1,AFF_1:6;
end;
A9: LIN d1,d2,d1 by AFF_1:7;
a<>b by A1,AFF_1:7;
then c,d1 // c,d2 by A2,A3,AFF_1:5;
then
A10: LIN c,d1,d2 by AFF_1:def 1;
then
A11: LIN d1,d2,c by AFF_1:6;
LIN d1,d2,c by A10,AFF_1:6;
then d1,d2 // c,d1 by A9,AFF_1:10;
then d1,d2 // a,b or c = d1 by A2,AFF_1:5;
then d1,d2 // b,a by A8,AFF_1:4;
then LIN d1,d2,a by A6,A7,AFF_1:9;
hence contradiction by A1,A6,A11,A7,AFF_1:8;
end;
definition
let AFS;
let f;
attr f is translation means
f is dilatation & (f = id the carrier of AFS or for a holds a<>f.a );
end;
theorem
id the carrier of AFS is translation
by Th69;
theorem Th82:
f is dilatation implies (f is translation iff for x,y holds x,f .x // y,f.y )
by Th76;
theorem Th83:
f is translation & g is translation & f.a=g.a & not LIN a,f.a,x
implies f.x=g.x
proof
assume that
A1: f is translation and
A2: g is translation and
A3: f.a=g.a and
A4: not LIN a,f.a,x;
set b=f.a, y=f.x, z=g.x;
A5: a,x // b,z & a,b // x,z by A2,A3,Th68,Th82;
f is dilatation by A1;
then
A6: a,x // b,y by Th68;
a,b // x,y by A1,Th82;
hence thesis by A4,A6,A5,Th80;
end;
theorem Th84:
f is translation & g is translation & f.a=g.a implies f=g
proof
assume that
A1: f is translation and
A2: g is translation and
A3: f.a=g.a;
set b=f.a;
A4: f is dilatation by A1;
A5: now
assume
A6: a<>b;
for x holds f.x=g.x
proof
let x;
now
assume
A7: LIN a,b,x;
now
A8: f<>(id the carrier of AFS) by A6;
then
A9: f.x<>x by A1;
assume x<>a;
consider p such that
A10: not LIN a,b,p by A6,AFF_1:13;
A11: f.p<>p by A1,A8;
A12: not LIN p,f.p,x
proof
A13: LIN a,b,f.x by A4,A7,Th74;
LIN a,b,a by AFF_1:7;
then
A14: LIN x,f.x,a by A6,A7,A13,AFF_1:8;
A15: LIN p,f.p,p by AFF_1:7;
LIN a,b,b by AFF_1:7;
then
A16: LIN x,f.x,b by A6,A7,A13,AFF_1:8;
assume
A17: LIN p,f.p,x;
then LIN p,f.p,f.x by A4,Th74;
then LIN x,f.x,p by A11,A17,A15,AFF_1:8;
hence contradiction by A10,A9,A14,A16,AFF_1:8;
end;
f.p=g.p by A1,A2,A3,A10,Th83;
hence thesis by A1,A2,A12,Th83;
end;
hence thesis by A3;
end;
hence thesis by A1,A2,A3,Th83;
end;
hence thesis by FUNCT_2:63;
end;
b=a implies thesis by A1,A2,A3;
hence thesis by A5;
end;
theorem Th85:
f is translation implies f" is translation
proof
A1: now
assume
A2: for x holds f.x<>x;
given y such that
A3: f".y=y;
f.y=y by A3,Th2;
hence contradiction by A2;
end;
assume
A4: f is translation;
then f is dilatation;
then
A5: f" is dilatation by Th70;
f=(id the carrier of AFS) implies f"=(id the carrier of AFS) by FUNCT_1:45;
hence thesis by A4,A5,A1;
end;
theorem
f is translation & g is translation implies (f*g) is translation
proof
assume that
A1: f is translation and
A2: g is translation;
f is dilatation & g is dilatation by A1,A2;
then
A3: (f*g) is dilatation by Th71;
now
assume
A4: (f*g)<>(id the carrier of AFS);
for x holds (f*g).x<>x
proof
given x such that
A5: (f*g).x=x;
f.(g.x)=x by A5,FUNCT_2:15;
then
A6: g.x=f".x by Th2;
f" is translation by A1,Th85;
then (f*g) = f*f" by A2,A6,Th84;
hence contradiction by A4,FUNCT_2:61;
end;
hence thesis by A3;
end;
hence thesis by A3;
end;
definition
let AFS;
let f;
attr f is collineation means
f is_automorphism_of the CONGR of AFS;
end;
theorem Th87:
f is collineation iff for x,y,z,t holds (x,y // z,t iff f.x,f.y // f.z,f.t)
proof
thus f is collineation implies for x,y,z,t holds x,y // z,t iff f.x,f.y // f
.z,f.t
proof
assume
A1: f is_automorphism_of the CONGR of AFS;
let x,y,z,t;
thus x,y // z,t implies f.x,f.y // f.z,f.t
proof
assume x,y // z,t;
then [[x,y],[z,t]] in the CONGR of AFS by ANALOAF:def 2;
then [[f.x,f.y],[f.z,f.t]] in the CONGR of AFS by A1;
hence thesis by ANALOAF:def 2;
end;
assume f.x,f.y // f.z,f.t;
then [[f.x,f.y],[f.z,f.t]] in the CONGR of AFS by ANALOAF:def 2;
then [[x,y],[z,t]] in the CONGR of AFS by A1;
hence thesis by ANALOAF:def 2;
end;
assume
A2: for x,y,z,t holds (x,y // z,t iff f.x,f.y // f.z,f.t);
let x,y,z,t;
x,y // z,t iff f.x,f.y // f.z,f.t by A2;
hence thesis by ANALOAF:def 2;
end;
theorem Th88:
f is collineation implies (LIN x,y,z iff LIN f.x,f.y,f.z)
proof
assume f is collineation;
then x,y // x,z iff f.x,f.y // f.x,f.z by Th87;
hence thesis by AFF_1:def 1;
end;
theorem
f is collineation & g is collineation implies f" is collineation & f*g
is collineation & id the carrier of AFS is collineation
proof
assume f is_automorphism_of the CONGR of AFS & g is_automorphism_of the
CONGR of AFS;
hence f" is_automorphism_of the CONGR of AFS & f*g is_automorphism_of the
CONGR of AFS by Th17,Th18;
thus id the carrier of AFS is_automorphism_of the CONGR of AFS;
end;
reserve A,C,K for Subset of AFS;
theorem Th90:
a in A implies f.a in f.:A
proof
A1: dom f = the carrier of AFS by FUNCT_2:52;
assume a in A;
hence thesis by A1,FUNCT_1:def 6;
end;
theorem Th91:
x in f.:A iff ex y st y in A & f.y=x
proof
thus x in f.:A implies ex y st y in A & f.y=x
proof
assume x in f.:A;
then ex y being object st y in dom f & y in A & x=f.y by FUNCT_1:def 6;
hence thesis;
end;
given y such that
A1: y in A & f.y=x;
dom f = the carrier of AFS by FUNCT_2:52;
hence thesis by A1,FUNCT_1:def 6;
end;
theorem Th92:
f.:A=f.:C implies A=C
proof
assume
A1: f.:A=f.:C;
now
let b be object;
assume
A2: b in C;
then reconsider b9=b as Element of AFS;
set y=f.b9;
y in f.:C by A2,Th90;
then ex a st a in A & f.a=y by A1,Th91;
hence b in A by FUNCT_2:58;
end;
then
A3: C c= A by TARSKI:def 3;
now
let a be object;
assume
A4: a in A;
then reconsider a9=a as Element of AFS;
set x=f.a9;
x in f.:A by A4,Th90;
then ex b st b in C & f.b=x by A1,Th91;
hence a in C by FUNCT_2:58;
end;
then A c= C by TARSKI:def 3;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th93:
f is collineation implies f.:(Line(a,b))=Line(f.a,f.b)
proof
assume
A1: f is collineation;
now
let x be object;
assume
A2: x in Line(f.a,f.b);
then reconsider x9=x as Element of AFS;
consider y such that
A3: f.y=x9 by Th1;
LIN f.a,f.b,f.y by A2,A3,AFF_1:def 2;
then LIN a,b,y by A1,Th88;
then y in Line(a,b) by AFF_1:def 2;
hence x in f.:(Line(a,b)) by A3,Th91;
end;
then
A4: Line(f.a,f.b) c= f.:(Line(a,b)) by TARSKI:def 3;
now
let x be object;
assume
A5: x in f.:(Line(a,b));
then reconsider x9=x as Element of AFS;
consider y such that
A6: y in Line(a,b) and
A7: f.y=x9 by A5,Th91;
LIN a,b,y by A6,AFF_1:def 2;
then LIN f.a,f.b,x9 by A1,A7,Th88;
hence x in Line(f.a,f.b) by AFF_1:def 2;
end;
then f.:(Line(a,b)) c= Line(f.a,f.b) by TARSKI:def 3;
hence thesis by A4,XBOOLE_0:def 10;
end;
theorem
f is collineation & K is being_line implies f.:K is being_line
proof
assume that
A1: f is collineation and
A2: K is being_line;
consider a,b such that
A3: a<>b and
A4: K=Line(a,b) by A2,AFF_1:def 3;
set q=f.b;
set p=f.a;
A5: p<>q by A3,FUNCT_2:58;
f.:K=Line(p,q) by A1,A4,Th93;
hence thesis by A5,AFF_1:def 3;
end;
theorem Th95:
f is collineation & A // C implies f.:A // f.:C
proof
assume that
A1: f is collineation and
A2: A // C;
consider a,b,c,d such that
A3: a<>b & c <>d and
A4: a,b // c,d and
A5: A=Line(a,b) & C=Line(c,d) by A2,AFF_1:37;
A6: f.a,f.b // f.c,f.d by A1,A4,Th87;
A7: f.a<>f.b & f.c <>f.d by A3,FUNCT_2:58;
f.:A=Line(f.a,f.b) & f.:C=Line(f.c,f.d) by A1,A5,Th93;
hence thesis by A7,A6,AFF_1:37;
end;
reserve AFP for AffinPlane,
A,C,D,K for Subset of AFP,
a,b,c,d,p,x,y for Element of AFP,
f for Permutation of the carrier of AFP;
theorem
(for A st A is being_line holds f.:A is being_line) implies f is collineation
proof
assume
A1: for A st A is being_line holds f.:A is being_line;
A2: a<>b implies f.:(Line(a,b))=Line(f.a,f.b)
proof
set A=Line(a,b);
set x=f.a;
set y=f.b;
set K=Line(x,y);
set M=f.:A;
assume
A3: a<>b;
then x<>y by FUNCT_2:58;
then
A4: K is being_line by AFF_1:def 3;
A is being_line by A3,AFF_1:def 3;
then
A5: M is being_line by A1;
a in A by AFF_1:15;
then
A6: x in M by Th90;
b in A by AFF_1:15;
then
A7: y in M by Th90;
x in K & y in K by AFF_1:15;
hence thesis by A3,A4,A5,A6,A7,AFF_1:18,FUNCT_2:58;
end;
A8: f.:A is being_line implies A is being_line
proof
set K=f.:A;
assume f.:A is being_line;
then consider x,y such that
A9: x<>y and
A10: K=Line(x,y) by AFF_1:def 3;
y in K by A10,AFF_1:15;
then consider b such that
b in A and
A11: f.b=y by Th91;
x in K by A10,AFF_1:15;
then consider a such that
a in A and
A12: f.a=x by Th91;
set C=Line(a,b);
C is being_line & f.:C=K by A2,A9,A10,A12,A11,AFF_1:def 3;
hence thesis by Th92;
end;
A13: f.:A // f.:C implies A // C
proof
set K=f.:A;
set M=f.:C;
assume
A14: f.:A // f.:C;
then M is being_line by AFF_1:36;
then
A15: C is being_line by A8;
K is being_line by A14,AFF_1:36;
then
A16: A is being_line by A8;
now
assume
A17: A<>C;
assume not A // C;
then consider p such that
A18: p in A & p in C by A16,A15,AFF_1:58;
set x=f.p;
x in K & x in M by A18,Th90;
hence contradiction by A14,A17,Th92,AFF_1:45;
end;
hence thesis by A16,AFF_1:41;
end;
A19: f.a,f.b // f.c,f.d implies a,b // c,d
proof
set x=f.a;
set y=f.b;
set z=f.c;
set t=f.d;
assume
A20: f.a,f.b // f.c,f.d;
now
set C=Line(c,d);
set A=Line(a,b);
set K=f.:A;
set M=f.:C;
A21: c in C & d in C by AFF_1:15;
assume
A22: a<>b & c <>d;
then
A23: x<>y & z<>t by FUNCT_2:58;
K=Line(x,y) & M=Line(z,t) by A2,A22;
then
A24: K // M by A20,A23,AFF_1:37;
a in A & b in A by AFF_1:15;
hence thesis by A13,A21,A24,AFF_1:39;
end;
hence thesis by AFF_1:3;
end;
A25: A // C implies f.:A // f.:C
proof
assume
A26: A // C;
then C is being_line by AFF_1:36;
then
A27: f.:C is being_line by A1;
A is being_line by A26,AFF_1:36;
then
A28: f.:A is being_line by A1; then
A29: f.:A // f.:A by AFF_1:41;
A<>C implies f.:A // f.:C
proof
assume
A30: A<>C;
assume not f.:A // f.:C;
then consider x such that
A31: x in f.:A and
A32: x in f.:C by A28,A27,AFF_1:58;
consider b such that
A33: b in C and
A34: x=f.b by A32,Th91;
consider a such that
A35: a in A and
A36: x=f.a by A31,Th91;
a=b by A36,A34,FUNCT_2:58;
hence contradiction by A26,A30,A35,A33,AFF_1:45;
end;
hence thesis by A29;
end;
a,b // c,d implies f.a,f.b // f.c,f.d
proof
assume
A37: a,b // c,d;
now
set C=Line(c,d);
set A=Line(a,b);
set K=f.:A;
set M=f.:C;
a in A by AFF_1:15;
then
A38: f.a in K by Th90;
b in A by AFF_1:15;
then
A39: f.b in K by Th90;
d in C by AFF_1:15;
then
A40: f.d in M by Th90;
c in C by AFF_1:15;
then
A41: f.c in M by Th90;
assume a<>b & c <>d;
then A // C by A37,AFF_1:37;
hence thesis by A25,A38,A39,A41,A40,AFF_1:39;
end;
hence thesis by AFF_1:3;
end;
hence thesis by A19,Th87;
end;
theorem
f is collineation & K is being_line & (for x st x in K holds f.x=x) &
not p in K & f.p=p implies f=id the carrier of AFP
proof
assume that
A1: f is collineation and
A2: K is being_line and
A3: for x st x in K holds f.x=x and
A4: not p in K and
A5: f.p=p;
A6: for x holds f.x=x
proof
let x;
now
assume not x in K;
consider a,b such that
A7: a in K and
A8: b in K and
A9: a<>b by A2,AFF_1:19;
set A=Line(p,a);
A10: p in A by AFF_1:15;
f.:A=Line(f.p,f.a) by A1,Th93;
then
A11: f.:A=A by A3,A5,A7;
A is being_line by A4,A7,AFF_1:def 3;
then consider C such that
A12: x in C and
A13: A // C by AFF_1:49;
A14: C is being_line by A13,AFF_1:36;
f.:A // f.:C by A1,A13,Th95;
then
A15: f.:C // C by A13,A11,AFF_1:44;
A16: a in A by AFF_1:15;
not C // K
proof
assume C // K;
then A // K by A13,AFF_1:44;
hence contradiction by A4,A7,A10,A16,AFF_1:45;
end;
then consider c such that
A17: c in C and
A18: c in K by A2,A14,AFF_1:58;
f.c = c by A3,A18;
then c in f.:C by A17,Th90;
then
A19: f.:C=C by A17,A15,AFF_1:45;
set M=Line(p,b);
A20: b in M by AFF_1:15;
f.:M=Line(f.p,f.b) by A1,Th93;
then
A21: f.:M=M by A3,A5,A8;
M is being_line by A4,A8,AFF_1:def 3;
then consider D such that
A22: x in D and
A23: M // D by AFF_1:49;
A24: D is being_line by A23,AFF_1:36;
f.:M // f.:D by A1,A23,Th95;
then
A25: f.:D // D by A23,A21,AFF_1:44;
A26: p in M by AFF_1:15;
not D // K
proof
assume D // K;
then M // K by A23,AFF_1:44;
hence contradiction by A4,A8,A26,A20,AFF_1:45;
end;
then consider d such that
A27: d in D and
A28: d in K by A2,A24,AFF_1:58;
f.d=d by A3,A28;
then d in f.:D by A27,Th90;
then
A29: f.:D=D by A27,A25,AFF_1:45;
A30: A is being_line by A13,AFF_1:36;
x=f.x
proof
assume
A31: x<>f.x;
f.x in C & f.x in D by A12,A22,A19,A29,Th90;
then C=D by A12,A22,A14,A24,A31,AFF_1:18;
then A // M by A13,A23,AFF_1:44;
then A=M by A10,A26,AFF_1:45;
hence contradiction by A2,A4,A7,A8,A9,A30,A10,A16,A20,AFF_1:18;
end;
hence thesis;
end;
hence thesis by A3;
end;
for x holds f.x=(id the carrier of AFP).x
by A6;
hence thesis by FUNCT_2:63;
end;