:: Transformations in Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received May 31, 1990
:: Copyright (c) 1990-2021 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;
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;
end;
theorem :: TRANSGEO:1
ex x st f.x=y;
theorem :: TRANSGEO:2
f.x=y iff (f").y=x;
definition
let A,f,g;
func f\g -> Permutation of A equals
:: TRANSGEO:def 1
(g*f)*g";
end;
scheme :: TRANSGEO:sch 1
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
for x being Element of A() ex y being Element of A() st P[x,y] and
for y being Element of A() ex x being Element of A() st P[x,y] and
for x,y,x9 being Element of A() st P[x,y] & P[x9,y] holds x=x9 and
for x,y,y9 being Element of A() st P[x,y] & P[x,y9] holds y=y9;
theorem :: TRANSGEO:3
f.(f".x) = x & f".(f.x) = x;
theorem :: TRANSGEO:4
f*(id A) = (id A)*f;
theorem :: TRANSGEO:5
g*f=h*f or f*g=f*h implies g=h;
theorem :: TRANSGEO:6
(f*g)\h = (f\h)*(g\h);
theorem :: TRANSGEO:7
(f")\g = (f\g)";
theorem :: TRANSGEO:8
f\(g*h) = (f\h)\g;
theorem :: TRANSGEO:9
(id A)\f = id A;
theorem :: TRANSGEO:10
f\(id A) = f;
theorem :: TRANSGEO:11
f.a=a implies (f\g).(g.a)=g.a;
reserve R for Relation of [:A,A:];
definition
let A,f,R;
pred f is_FormalIz_of R means
:: TRANSGEO:def 2
for x,y holds [[x,y],[f.x,f.y]] in R;
end;
theorem :: TRANSGEO:12
R is_reflexive_in [:A,A:] implies id A is_FormalIz_of R;
theorem :: TRANSGEO:13
R is_symmetric_in [:A,A:] & f is_FormalIz_of R implies f" is_FormalIz_of R;
theorem :: TRANSGEO:14
R is_transitive_in [:A,A:] & f is_FormalIz_of R & g is_FormalIz_of R
implies (f*g) is_FormalIz_of R;
theorem :: TRANSGEO:15
(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;
definition
let A;
let f;
let R;
pred f is_automorphism_of R means
:: TRANSGEO:def 3
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 :: TRANSGEO:16
id A is_automorphism_of R;
theorem :: TRANSGEO:17
f is_automorphism_of R implies f" is_automorphism_of R;
theorem :: TRANSGEO:18
f is_automorphism_of R & g is_automorphism_of R implies g*f
is_automorphism_of R;
theorem :: TRANSGEO:19
R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] & f
is_FormalIz_of R implies f is_automorphism_of R;
theorem :: TRANSGEO:20
(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;
theorem :: TRANSGEO:21
f is_FormalIz_of R & g is_automorphism_of R implies f\g is_FormalIz_of R;
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
:: TRANSGEO:def 4
f is_FormalIz_of the CONGR of AS;
end;
reserve a,b,x,y for Element of AS;
theorem :: TRANSGEO:22
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 );
definition
let IT be non empty AffinStruct;
attr IT is CongrSpace-like means
:: TRANSGEO:def 5
(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;
end;
definition
mode CongrSpace is CongrSpace-like non empty AffinStruct;
end;
reserve CS for CongrSpace;
theorem :: TRANSGEO:23
id the carrier of CS is_DIL_of CS;
theorem :: TRANSGEO:24
for f being Permutation of the carrier of CS st f is_DIL_of CS
holds f" is_DIL_of CS;
theorem :: TRANSGEO:25
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;
reserve OAS for OAffinSpace;
reserve a,b,c,d,p,q,r,x,y,z,t,u for Element of OAS;
theorem :: TRANSGEO:26
OAS is CongrSpace-like;
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
:: TRANSGEO:def 6
f is_DIL_of OAS;
end;
theorem :: TRANSGEO:27
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 );
definition
let OAS;
let f be Permutation of the carrier of OAS;
attr f is negative_dilatation means
:: TRANSGEO:def 7
for a,b holds a,b // f.b,f.a;
end;
theorem :: TRANSGEO:28
id the carrier of OAS is positive_dilatation;
theorem :: TRANSGEO:29
for f being Permutation of the carrier of OAS st f is
positive_dilatation holds f" is positive_dilatation;
theorem :: TRANSGEO:30
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
;
theorem :: TRANSGEO:31
not ex f st f is negative_dilatation & f is positive_dilatation;
theorem :: TRANSGEO:32
f is negative_dilatation implies f" is negative_dilatation;
theorem :: TRANSGEO:33
f is positive_dilatation & g is negative_dilatation implies f*g is
negative_dilatation & g*f is negative_dilatation;
definition
let OAS;
let f be Permutation of the carrier of OAS;
attr f is dilatation means
:: TRANSGEO:def 8
f is_FormalIz_of lambda(the CONGR of OAS);
end;
theorem :: TRANSGEO:34
for f being Permutation of the carrier of OAS holds (f is
dilatation iff for a,b holds a,b '||' f.a,f.b );
theorem :: TRANSGEO:35
f is positive_dilatation or f is negative_dilatation implies f is dilatation;
theorem :: TRANSGEO:36
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);
theorem :: TRANSGEO:37
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;
theorem :: TRANSGEO:38
id the carrier of OAS is dilatation;
theorem :: TRANSGEO:39
f is positive_dilatation or f is negative_dilatation implies f is dilatation;
theorem :: TRANSGEO:40
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);
theorem :: TRANSGEO:41
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;
theorem :: TRANSGEO:42
id the carrier of OAS is dilatation;
theorem :: TRANSGEO:43
f is dilatation implies f" is dilatation;
theorem :: TRANSGEO:44
f is dilatation & g is dilatation implies f*g is dilatation;
theorem :: TRANSGEO:45
f is dilatation implies for a,b,c,d holds a,b '||' c,d iff f.a,f
.b '||' f.c,f.d;
theorem :: TRANSGEO:46
f is dilatation implies
for a,b,c holds a,b,c are_collinear iff f.a,f.b,f.c are_collinear;
theorem :: TRANSGEO:47
f is dilatation & x,f.x,y are_collinear implies x,f.x,f.y are_collinear;
theorem :: TRANSGEO:48
a,b '||' c,d implies
(a,c '||' b,d or ex x st a,c,x are_collinear & b,d,x are_collinear );
theorem :: TRANSGEO:49
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 );
theorem :: TRANSGEO:50
f is dilatation & f.a=a & f.b=b & not a,b,x are_collinear implies f.x=x;
theorem :: TRANSGEO:51
f is dilatation & f.a=a & f.b=b & a<>b implies f=(id the carrier of OAS);
theorem :: TRANSGEO:52
f is dilatation & g is dilatation & f.a=g.a & f.b=g.b implies a=b or f =g;
definition
let OAS;
let f be Permutation of the carrier of OAS;
attr f is translation means
:: TRANSGEO:def 9
f is dilatation & (f = id the carrier of OAS or for a holds a<>f.a);
end;
theorem :: TRANSGEO:53
f is dilatation implies (f is translation iff for x,y holds x,f.
x '||' y,f.y );
theorem :: TRANSGEO:54
f is translation & g is translation & f.a=g.a & not a,f.a,x are_collinear
implies f.x=g.x;
theorem :: TRANSGEO:55
f is translation & g is translation & f.a=g.a implies f=g;
theorem :: TRANSGEO:56
f is translation implies f" is translation;
theorem :: TRANSGEO:57
f is translation & g is translation implies (f*g) is translation;
theorem :: TRANSGEO:58
f is translation implies f is positive_dilatation;
theorem :: TRANSGEO:59
f is dilatation & f.p=p & Mid q,p,f.q & not p,q,x are_collinear
implies Mid x,p,f.x;
theorem :: TRANSGEO:60
f is dilatation & f.p=p & Mid q,p,f.q & q<>p implies Mid x,p,f.x;
theorem :: TRANSGEO:61
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;
theorem :: TRANSGEO:62
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;
theorem :: TRANSGEO:63
f is dilatation & f.p=p & q<>p & Mid q,p,f.q implies f is negative_dilatation
;
theorem :: TRANSGEO:64
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;
theorem :: TRANSGEO:65
f is dilatation implies f is positive_dilatation or f is negative_dilatation;
reserve AFS for AffinSpace;
reserve a,b,c,d,d1,d2,p,x,y,z,t for Element of AFS;
theorem :: TRANSGEO:66
AFS is CongrSpace-like;
theorem :: TRANSGEO:67
Lambda(OAS) is CongrSpace;
reserve f,g for Permutation of the carrier of AFS;
definition
let AFS;
let f;
attr f is dilatation means
:: TRANSGEO:def 10
f is_DIL_of AFS;
end;
theorem :: TRANSGEO:68
f is dilatation iff for a,b holds a,b // f.a,f.b;
theorem :: TRANSGEO:69
id the carrier of AFS is dilatation;
theorem :: TRANSGEO:70
f is dilatation implies f" is dilatation;
theorem :: TRANSGEO:71
f is dilatation & g is dilatation implies (f*g) is dilatation;
theorem :: TRANSGEO:72
f is dilatation implies for a,b,c,d holds a,b // c,d iff f.a,f.b // f.c,f.d;
theorem :: TRANSGEO:73
f is dilatation implies for a,b,c
holds LIN a,b,c iff LIN f.a,f.b,f.c;
theorem :: TRANSGEO:74
f is dilatation & LIN x,f.x,y implies LIN x,f.x,f.y;
theorem :: TRANSGEO:75
a,b // c,d implies (a,c // b,d or ex x st LIN a,c,x & LIN b,d,x );
theorem :: TRANSGEO:76
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 );
theorem :: TRANSGEO:77
f is dilatation & f.a=a & f.b=b & not LIN a,b,x implies f.x=x;
theorem :: TRANSGEO:78
f is dilatation & f.a=a & f.b=b & a<>b implies f=id the carrier of AFS;
theorem :: TRANSGEO:79
f is dilatation & g is dilatation & f.a=g.a & f.b=g.b implies a=b or f =g;
theorem :: TRANSGEO:80
not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 & a,c //
b,d2 implies d1=d2;
definition
let AFS;
let f;
attr f is translation means
:: TRANSGEO:def 11
f is dilatation & (f = id the carrier of AFS or for a holds a<>f.a );
end;
theorem :: TRANSGEO:81
id the carrier of AFS is translation;
theorem :: TRANSGEO:82
f is dilatation implies (f is translation iff for x,y holds x,f .x // y,f.y )
;
theorem :: TRANSGEO:83
f is translation & g is translation & f.a=g.a & not LIN a,f.a,x
implies f.x=g.x;
theorem :: TRANSGEO:84
f is translation & g is translation & f.a=g.a implies f=g;
theorem :: TRANSGEO:85
f is translation implies f" is translation;
theorem :: TRANSGEO:86
f is translation & g is translation implies (f*g) is translation;
definition
let AFS;
let f;
attr f is collineation means
:: TRANSGEO:def 12
f is_automorphism_of the CONGR of AFS;
end;
theorem :: TRANSGEO:87
f is collineation iff for x,y,z,t holds (x,y // z,t iff f.x,f.y // f.z,f.t);
theorem :: TRANSGEO:88
f is collineation implies (LIN x,y,z iff LIN f.x,f.y,f.z);
theorem :: TRANSGEO:89
f is collineation & g is collineation implies f" is collineation & f*g
is collineation & id the carrier of AFS is collineation;
reserve A,C,K for Subset of AFS;
theorem :: TRANSGEO:90
a in A implies f.a in f.:A;
theorem :: TRANSGEO:91
x in f.:A iff ex y st y in A & f.y=x;
theorem :: TRANSGEO:92
f.:A=f.:C implies A=C;
theorem :: TRANSGEO:93
f is collineation implies f.:(Line(a,b))=Line(f.a,f.b);
theorem :: TRANSGEO:94
f is collineation & K is being_line implies f.:K is being_line;
theorem :: TRANSGEO:95
f is collineation & A // C implies f.:A // f.:C;
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 :: TRANSGEO:96
(for A st A is being_line holds f.:A is being_line) implies f is collineation
;
theorem :: TRANSGEO:97
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;