:: 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;