:: The Rotation Group
:: by Karol P\kak
::
:: Received May 30, 2011
:: Copyright (c) 2011-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 NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, ARYTM_1, ARYTM_3,
SUPINF_2, XBOOLE_0, RELAT_1, CARD_1, VALUED_0, FINSEQ_1, COMPLEX1,
SQUARE_1, CARD_3, RVSUM_1, XXREAL_0, NAT_1, TARSKI, STRUCT_0,
REAL_1, FUNCT_1, UNIALG_1, MSSUBFAM, FUNCOP_1, FINSEQ_2, ALGSTR_0,
FUNCT_2, FVSUM_1, INCSP_1, MATRIX_1, MATRIX_3, MATRIX13, MATRLIN,
MATRLIN2, MESFUNC1, ORDINAL4, PARTFUN1, PRVECT_1, QC_LANG1,
RLVECT_2, RLVECT_3, TREES_1, VALUED_1, VECTSP_1, MATRIXJ1,
ZFMISC_1, BINOP_1, GROUP_1, ABIAN, XXREAL_1, SIN_COS, FINSOP_1,
FUNCT_4, MATRIX_6, PRE_POLY, TOPS_2, RFINSEQ, MONOID_0, MATRIXR2,
MATRTOP3, XCMPLX_0;
notations GCD_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, COMPLEX1, REAL_1, NAT_1, NAT_D, FUNCOP_1, FINSEQ_1,
PRE_POLY, RFINSEQ, FINSEQ_2, RVSUM_1, VALUED_0, SQUARE_1,
STRUCT_0, PRE_TOPC, TOPS_2, RLVECT_1, EUCLID, TOPREAL9, CARD_1,
VECTSP_1, MATRIX_0, MATRIX_1, MATRIX_3, MATRIX_6, GROUP_1,
MATRIX11, MATRTOP1, SIN_COS, ALGSTR_0, MATRIX_7, BINOP_1, FVSUM_1,
RCOMP_1, MONOID_0, GROUP_4, PRVECT_1, RLVECT_2, RLVECT_3, FUNCT_7,
MATRIX13, MATRIXR2, FINSOP_1, MATRLIN, MATRLIN2, MOD_2, MATRIXJ1,
TMAP_1;
constructors GCD_1, REAL_1, SQUARE_1, BORSUK_1, MONOID_0, CONVEX1,
TOPREAL9, BINARITH, FVSUM_1, LAPLACE, MATRIX_6, MATRIX11, TOPS_2,
MATRIX13, MATRLIN2, MATRTOP1, REALSET1, RLVECT_3, MATRIXJ1,
RCOMP_1, ABIAN, SIN_COS, MATRIX_7, SETWISEO, GROUP_4, TMAP_1,
FINSOP_1, MATRIXR2, MATRIX_0, BINOP_2, VECTSP_2, MATRIX_3;
registrations XBOOLE_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED,
STRUCT_0, MONOID_0, EUCLID, VALUED_0, FINSEQ_1, FUNCT_1, RELAT_1,
TOPREAL9, CARD_1, FINSEQ_2, FINSET_1, FUNCT_2, MATRIX13, MATRIX_1,
MATRTOP1, NUMBERS, PRVECT_1, RELSET_1, RLVECT_2, VECTSP_1, XCMPLX_0,
SIN_COS, MATRIX11, MATRIXJ1, GRCAT_1, BORSUK_3, FUNCOP_1, MATRIX_0,
INT_1, FUNCT_7, PRE_POLY, SUBSET_1, MATRIX_6, RVSUM_1, ORDINAL1,
POLYNOM8, VECTSP_2, GCD_1, LAPLACE;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI;
equalities SQUARE_1, EUCLID, XCMPLX_0, ALGSTR_0, STRUCT_0, FINSEQ_1, MATRTOP1,
VECTSP_1, FVSUM_1;
expansions TARSKI, STRUCT_0, TOPREAL9, FINSEQ_1, VECTSP_1;
theorems XREAL_0, TARSKI, FUNCT_2, EUCLID, XBOOLE_1, XBOOLE_0, SQUARE_1,
XCMPLX_1, ABSVALUE, RVSUM_1, EUCLID_2, ENUMSET1, XREAL_1, XXREAL_0,
RLVECT_1, ORDINAL1, VECTSP_1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_2,
FINSEQ_3, FUNCT_1, FVSUM_1, LAPLACE, MATRIX_0, MATRIX_1, MATRIX_6,
MATRIX13, MATRIXR1, MATRLIN2, MATRTOP1, NAT_1, PARTFUN1, PRE_POLY,
RELAT_1, RLSUB_1, RLVECT_2, RLVECT_3, ZFMISC_1, MATRIXJ1, TOPS_2,
TOPREAL9, MATRIX_9, SIN_COS, MATRIX_7, MATRIXR2, MATRIX11, MATRIX_3,
MATRIX15, RFINSEQ, FINSEQ_7, SIN_COS6, XXREAL_1, GROUP_4, MONOID_0,
GROUP_1, FINSEQ_5, TMAP_1, RLVECT_4, FUNCT_7, TOPREALC, VALUED_1, INT_1,
FINSOP_1, MOD_2, TOPREAL3, FINSEQ_4;
schemes NAT_1, FINSEQ_4, MATRIX_0;
begin :: Preliminaries
reserve x,X for set,
r,r1,r2,s for Real,
i,j,k,m,n for Nat;
theorem Th1:
for K be Field,M be Matrix of n,K
for P be Permutation of Seg n holds
Det((M*P)@*P)@ = Det M &
for i,j st [i,j] in Indices M holds ((M*P)@*P)@*(i,j) = M*(P.i,P.j)
proof
let K be Field,M be Matrix of n,K;
let P be Permutation of Seg n;
reconsider p=P as Element of Permutations(n) by MATRIX_1:def 16;
A1: --Det M=Det M by RLVECT_1:17;
A2: p is even & -(Det M,p)=Det M or p is odd & -(Det M,p)=-Det M
by MATRIX_1:def 20;
thus Det((M*P)@*P)@=Det((M*P)@*P) by MATRIXR2:43
.=-(Det(M*P)@,p) by MATRIX11:46
.=-(Det(M*P),p) by MATRIXR2:43
.=-(-(Det M,p),p) by MATRIX11:46
.=Det M by A1,A2,MATRIX_1:def 20;
let i,j;
assume A3: [i,j] in Indices M;
Indices M=Indices(((M*P)@*P)@) by MATRIX_0:26;
then A4: [j,i] in Indices((M*P)@*P) by A3,MATRIX_0:def 6;
then A5: ((M*P)@*P)@*(i,j)=((M*P)@*P)*(j,i) by MATRIX_0:def 6;
Indices M=Indices((M*P)@*P) & Indices M=Indices((M*P)@) by MATRIX_0:26;
then A6: ex k st k=P.j & [k,i] in Indices(M*P)@ &
((M*P)@*P)*(j,i)=((M*P)@)*(k,i) by A4,MATRIX11:37;
then A7: [i,P.j] in Indices(M*P) by MATRIX_0:def 6;
Indices(M*P)=Indices M by MATRIX_0:26;
then (M*P)*(i,P.j)=M*(P.i,P.j) by A7,MATRIX11:def 4;
hence ((M*P)@*P)@*(i,j)=M*(P.i,P.j) by A5,A6,A7,MATRIX_0:def 6;
end;
theorem Th2:
for K be Field for M be diagonal Matrix of n,K holds M@ = M
proof
let K be Field;
let M be diagonal Matrix of n,K;
for i,j st[i,j] in Indices M holds M*(i,j)=M@*(i,j)
proof
let i,j;
assume A1: [i,j] in Indices M;
then A2: [j,i] in Indices M by MATRIX_0:28;
then A3: M@*(i,j)=M*(j,i) by MATRIX_0:def 6;
per cases;
suppose i=j;
hence thesis by A1,MATRIX_0:def 6;
end;
suppose A4: i<>j;
then M*(i,j)=0.K by A1,MATRIX_1:def 10;
hence thesis by A2,A3,A4,MATRIX_1:def 10;
end;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th3:
for f be real-valued FinSequence
for i st i in dom f holds Sum sqr(f+*(i,r)) = (Sum sqr f)-(f.i)^2+r^2
proof
let f be real-valued FinSequence;
let i such that
A1: i in dom f;
reconsider fi=f.i as Element of REAL by XREAL_0:def 1;
set F=@@f;
set G=F| (i-' 1),H=F/^i;
A2: sqr<*fi*>=<*fi^2*> by RVSUM_1:55;
F=F+*(i,fi) by FUNCT_7:35
.=G^<*fi*>^H by A1,FUNCT_7:98;
then sqr F=sqr(G^<*fi*>)^sqr H by RVSUM_1:144
.=sqr G^sqr<*fi*>^sqr H by RVSUM_1:144;
then A3: Sum sqr F=Sum(sqr G^sqr<*fi*>)+Sum sqr H by RVSUM_1:75
.=Sum sqr G+fi^2+Sum sqr H by A2,RVSUM_1:74;
reconsider R=r as Element of REAL by XREAL_0:def 1;
A4: sqr<*R*>=<*R^2*> by RVSUM_1:55;
F+*(i,R)=G^<*R*>^H by A1,FUNCT_7:98;
then sqr(F+*(i,R))=sqr(G^<*R*>)^sqr H by RVSUM_1:144
.=sqr G^sqr<*R*>^sqr H by RVSUM_1:144;
then Sum sqr(F+*(i,R))=Sum(sqr G^sqr<*R*>)+Sum sqr H by RVSUM_1:75
.=Sum sqr G+R^2+Sum sqr H by A4,RVSUM_1:74;
hence thesis by A3;
end;
definition
let X;
let F be Function-yielding Function;
attr F is X -support-yielding means :Def1:
for f be Function,x st f in dom F & F.f.x <> f.x holds x in X;
end;
registration
let X;
cluster X-support-yielding for Function-yielding Function;
existence
proof
reconsider F={} as Function-yielding Function;
F is X-support-yielding;
hence thesis;
end;
end;
registration
let X;
let Y be Subset of X;
cluster Y-support-yielding -> X-support-yielding
for Function-yielding Function;
coherence
proof
let F be Function-yielding Function;
assume A1: F is Y-support-yielding;
let f be Function,x be set;
assume f in dom F & F.f.x<>f.x;
then x in Y by A1;
hence thesis;
end;
end;
registration
let X,Y be set;
cluster X-support-yielding Y-support-yielding ->
X/\Y-support-yielding for Function-yielding Function;
coherence
proof
let F be Function-yielding Function;
assume A1: F is X-support-yielding Y-support-yielding;
let f be Function,x be set;
assume f in dom F & F.f.x<>f.x;
then x in X & x in Y by A1;
hence thesis by XBOOLE_0:def 4;
end;
let f be X-support-yielding Function-yielding Function;
let g be Y-support-yielding Function-yielding Function;
cluster f*g -> (X\/Y)-support-yielding;
coherence
proof
set fg=f*g;
let h be Function,x be set;
assume that
A2: h in dom fg and
A3: fg.h.x<>h.x;
A4: h in dom g by A2,FUNCT_1:11;
assume A5: not x in X\/Y;
then not x in Y by XBOOLE_0:def 3;
then A6: g.h.x=h.x by A4,Def1;
A7: fg.h=f.(g.h) & g.h in dom f by A2,FUNCT_1:11,12;
not x in X by A5,XBOOLE_0:def 3;
hence thesis by A3,A6,A7,Def1;
end;
end;
registration
let n;
cluster homogeneous for Function of TOP-REAL n,TOP-REAL n;
existence
proof
reconsider N=n as Element of NAT by ORDINAL1:def 12;
the homogeneous Function of TOP-REAL N,TOP-REAL N is homogeneous;
hence thesis;
end;
end;
registration
let n,m;
cluster -> FinSequence-yielding for Function of TOP-REAL n,TOP-REAL m;
coherence
proof
let F be Function of TOP-REAL n,TOP-REAL m;
now let x be object;
assume x in dom F;
then rng F c=the carrier of TOP-REAL m & F.x in rng F
by FUNCT_1:def 3,RELAT_1:def 19;
hence F.x is FinSequence;
end;
hence thesis by PRE_POLY:def 3;
end;
end;
registration
let n,m;
let A be Matrix of n,m,F_Real;
cluster Mx2Tran A -> additive;
coherence
by MATRTOP1:22;
end;
registration
let n;
let A be Matrix of n,F_Real;
cluster Mx2Tran A -> homogeneous;
coherence
by MATRTOP1:23;
end;
registration
let n;
let f,g be homogeneous Function of TOP-REAL n,TOP-REAL n;
cluster f*g -> homogeneous for Function of TOP-REAL n,TOP-REAL n;
coherence
proof
set TR=TOP-REAL n;
now let r be Real,p be Point of TR;
reconsider gp=g.p as Point of TR;
A1: dom(f*g)=the carrier of TR by FUNCT_2:52;
hence (f*g).(r*p)=f.(g.(r*p)) by FUNCT_1:12
.=f.(r*gp) by TOPREAL9:def 4
.=r*f.gp by TOPREAL9:def 4
.=r*((f*g).p) by A1,FUNCT_1:12;
end;
hence thesis;
end;
end;
begin :: Improper Rotation
reserve p,q for Point of TOP-REAL n;
Lm1: i in Seg n implies
ex M be Matrix of n,F_Real st
Det M=-1.F_Real & M*(i,i)=-1.F_Real &
for k,m st[k,m] in Indices M holds
(k=m & k<>i implies M*(k,k)=1.F_Real) &
(k<>m implies M*(k,m)=0.F_Real)
proof
set FR=the carrier of F_Real;
set mm=the multF of F_Real;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
defpred P[set,set,set] means
($1=$2 & $1=i implies $3=-1.F_Real) & ($1=$2 & $1<>i implies $3=1.F_Real) &
($1<>$2 implies $3=0.F_Real);
A1: for k,m st[k,m] in [:Seg N,Seg N:]ex x being Element of F_Real st
P[k,m,x]
proof
let k,m;
assume[k,m] in [:Seg N,Seg N:];
k=m & k=i or k=m & k<>i or k<>m;
hence thesis;
end;
consider M be Matrix of N,F_Real such that
A2: for n,m st[n,m] in Indices M holds P[n,m,M*(n,m)]
from MATRIX_0:sch 2(A1);
reconsider M as Matrix of n,F_Real;
A3: Indices M=[:Seg n,Seg n:] by MATRIX_0:24;
now let k,m being Nat;
assume k in Seg n & m in Seg n;
then A4: [k,m] in Indices M by A3,ZFMISC_1:87;
assume k<>m;
hence M*(k,m)=0.F_Real by A2,A4;
end;
then A5: M is diagonal by MATRIX_7:def 2;
set D=diagonal_of_Matrix M;
defpred R[Nat] means $1+i<=n implies mm"**"(D| ($1+i))=-1.F_Real;
A6: len D=n by MATRIX_3:def 10;
A7: for k st R[k] holds R[k+1]
proof
let k;
assume A8: R[k];
set k1=k+1,ki=k1+i;
assume A9: k1+i<=n;
A10: k1+i=k+i+1;
then A11: 1<=ki by NAT_1:11;
then ki in dom D by A6,A9,FINSEQ_3:25;
then A12: D|ki=(D| (k+i))^<*D.ki*> by A10,FINSEQ_5:10;
i<=k+i by NAT_1:11;
then A13: i<k1+i by A10,NAT_1:13;
A14: ki in Seg n by A9,A11;
then [ki,ki] in Indices M by A3,ZFMISC_1:87;
then 1.F_Real=M*(ki,ki) by A2,A13
.=D.ki by A14,MATRIX_3:def 10;
hence mm"**"(D|ki) = (-1.F_Real)*1.F_Real
by A8,A9,A10,A12,FINSOP_1:4,NAT_1:13
.= (-1.F_Real)*1
.=-1.F_Real;
end;
defpred P[Nat] means $1<i implies mm"**"(D|$1)=1.F_Real;
A15: P[0]
proof
assume 0<i;
D|0=<*>the carrier of F_Real & the_unity_wrt mm=1.F_Real by FVSUM_1:5;
hence thesis by FINSOP_1:10;
end;
assume A16: i in Seg n;
then A17: 1<=i by FINSEQ_1:1;
A18: i<=n by A16,FINSEQ_1:1;
then A19: n-i+i=n & n-i is Nat by NAT_1:21;
take M;
A20: for k st P[k] holds P[k+1]
proof
let k such that
A21: P[k];
set k1=k+1;
assume A22: k1<i;
then A23: 1<=k1 & k1<=n by A18,NAT_1:14,XXREAL_0:2;
then k1 in dom D by A6,FINSEQ_3:25;
then A24: D|k1=(D|k)^<*D.k1*> by FINSEQ_5:10;
A25: k1 in Seg n by A23;
then [k1,k1] in Indices M by A3,ZFMISC_1:87;
then 1.F_Real=M*(k1,k1) by A2,A22
.=D.k1 by A25,MATRIX_3:def 10;
hence mm"**"(D|k1)=1.F_Real*1.F_Real
by A21,A22,A24,FINSOP_1:4,NAT_1:13
.=1.F_Real*1
.=1.F_Real;
end;
A26: for k holds P[k] from NAT_1:sch 2(A15,A20);
A27: R[0]
proof
reconsider I=i-1 as Nat by A17;
assume 0+i<=n;
A28: I+1=i;
then I<i by NAT_1:13;
then A29: mm"**"(D|I)=1.F_Real by A26;
1<=i by A16,FINSEQ_1:1;
then i in dom D by A6,A18,FINSEQ_3:25;
then A30: D|i=(D|I)^<*D.i*> by A28,FINSEQ_5:10;
[i,i] in Indices M by A3,A16,ZFMISC_1:87;
then -1.F_Real=M*(i,i) by A2
.=D.i by A16,MATRIX_3:def 10;
hence mm"**"(D| (0+i))
=1.F_Real*(-1.F_Real) by A29,A30,FINSOP_1:4
.= 1 * (-1.F_Real)
.=-1.F_Real;
end;
for k holds R[k] from NAT_1:sch 2(A27,A7);
hence -1.F_Real=mm"**"(D|n) by A19
.=mm"**"D by A6,FINSEQ_1:58
.=Det M by A5,A17,A18,MATRIX_7:17,XXREAL_0:2;
[i,i] in Indices M by A3,A16,ZFMISC_1:87;
hence M*(i,i)=-1.F_Real by A2;
let k,m;
assume[k,m] in Indices M;
hence thesis by A2;
end;
definition
let n,i such that
A1: i in Seg n;
func AxialSymmetry(i,n) -> invertible Matrix of n,F_Real means :Def2:
it*(i,i) = -1.F_Real &
for k,m st[k,m] in Indices it holds
(k = m & k <> i implies it*(k,k) = 1.F_Real) &
(k <> m implies it*(k,m) = 0.F_Real);
existence
proof
consider M be Matrix of n,F_Real such that
A2: Det M=-1.F_Real and
A3: M*(i,i)=-1.F_Real & for k,m st[k,m] in Indices M holds(k=m & k<>i
implies M*(k,k)=1.F_Real) & (k<>m implies M*(k,m)=0.F_Real) by A1,Lm1;
Det M<>0.F_Real by A2;
then Det M is non zero;
then Det M is unital;
then M is invertible by LAPLACE:34;
hence thesis by A3;
end;
uniqueness
proof
let A1,A2 be invertible Matrix of n,F_Real such that
A4: A1*(i,i)=-1.F_Real and
A5: for k,m st[k,m] in Indices A1 holds
(k=m & k<>i implies A1*(k,k)=1.F_Real) &
(k<>m implies A1*(k,m)=0.F_Real) and
A6: A2*(i,i)=-1.F_Real and
A7: for k,m st[k,m] in Indices A2 holds
(k=m & k<>i implies A2*(k,k)=1.F_Real) &
(k<>m implies A2*(k,m)=0.F_Real);
for k,m st[k,m] in Indices A1 holds A1*(k,m)=A2*(k,m)
proof
let k,m;
assume A8: [k,m] in Indices A1;
then A9: [k,m] in Indices A2 by MATRIX_0:26;
per cases;
suppose A10: k<>m;
then A1*(k,m)=0.F_Real by A5,A8;
hence thesis by A7,A9,A10;
end;
suppose A11: k=m & k<>i;
then A1*(k,m)=1.F_Real by A5,A8;
hence thesis by A7,A9,A11;
end;
suppose k=m & k=i;
hence thesis by A4,A6;
end;
end;
hence thesis by MATRIX_0:27;
end;
end;
theorem Th4:
i in Seg n implies Det AxialSymmetry(i,n) = -1.F_Real
proof
assume A1: i in Seg n;
then consider M be Matrix of n,F_Real such that
A2: Det M=-1.F_Real and
A3: M*(i,i)=-1.F_Real & for k,m st[k,m] in Indices M holds
(k=m & k<>i implies M*(k,k)=1.F_Real) & (k<>m implies M*(k,m)=0.F_Real)
by Lm1;
Det M<>0.F_Real by A2;
then Det M is non zero;
then Det M is unital;
then M is invertible by LAPLACE:34;
hence thesis by A1,A2,A3,Def2;
end;
theorem Th5:
i in Seg n & j in Seg n & i<>j implies @p"*"Col(AxialSymmetry(i,n),j)=p.j
proof
set S=Seg n;
assume that
A1: i in S and
A2: j in S and
A3: i<>j;
set A=AxialSymmetry(i,n),C=Col(A,j);
A4: Indices A=[:S,S:] by MATRIX_0:24;
then A5: [j,j] in Indices A by A2,ZFMISC_1:87;
A6: len A=n by MATRIX_0:25;
then A7: dom A=S by FINSEQ_1:def 3;
len C=n by A6,MATRIX_0:def 8;
then A8: dom C=S by FINSEQ_1:def 3;
A9: now let m such that
A10: m in dom C and
A11: m<>j;
A12: [m,j] in Indices A by A2,A4,A8,A10,ZFMISC_1:87;
thus C.m=A*(m,j) by A7,A8,A10,MATRIX_0:def 8
.=0.F_Real by A1,A11,A12,Def2;
end;
len p=n by CARD_1:def 7;
then A13: dom p=S by FINSEQ_1:def 3;
C.j=A*(j,j) by A2,A7,MATRIX_0:def 8
.=1.F_Real by A1,A3,A5,Def2;
hence p.j=Sum(mlt(C,@p)) by A2,A8,A9,A13,MATRIX_3:17
.=@p"*"C by FVSUM_1:64;
end;
theorem Th6:
i in Seg n implies @p"*"Col(AxialSymmetry(i,n),i) = -p.i
proof
set S=Seg n;
assume A1: i in S;
reconsider pI=@p.i as Element of F_Real by XREAL_0:def 1;
set A=AxialSymmetry(i,n),C=Col(A,i);
A2: len A=n by MATRIX_0:25;
then A3: dom A=S by FINSEQ_1:def 3;
then A4: C.i=A*(i,i) by A1,MATRIX_0:def 8;
len p=n & len C=n by A2,CARD_1:def 7;
then len mlt(@p,C)=n by MATRIX_3:6;
then A5: dom mlt(@p,C)=S by FINSEQ_1:def 3;
A6: Indices A=[:S,S:] by MATRIX_0:24;
A7: for k st k in dom mlt(@p,C) & k<>i holds mlt(@p,C).k=0.F_Real
proof
let k;
assume that
A8: k in dom mlt(@p,C) and
A9: k<>i;
@p.k in REAL by XREAL_0:def 1;
then reconsider pk=@p.k as Element of F_Real;
A10: [k,i] in Indices A by A1,A5,A6,A8,ZFMISC_1:87;
C.k=A*(k,i) by A3,A5,A8,MATRIX_0:def 8;
hence mlt(@p,C).k=pk*(A*(k,i)) by A8,FVSUM_1:60
.=pk*0.F_Real by A1,A9,A10,Def2
.=0.F_Real;
end;
thus@p"*"C=mlt(@p,C).i by A1,A5,A7,MATRIX_3:12
.=pI*(A*(i,i)) by A1,A4,A5,FVSUM_1:60
.=pI*(-1.F_Real) by A1,Def2
.= pI *(-1)
.=-p.i;
end;
theorem Th7:
i in Seg n implies AxialSymmetry(i,n) is diagonal &
AxialSymmetry(i,n)~ = AxialSymmetry(i,n)
proof
set S=Seg n,A=AxialSymmetry(i,n);
set ONE=1.(F_Real,n),AA=A*A;
assume A1: i in S;
for k,m st [k,m] in Indices A & A*(k,m)<>0.F_Real holds k=m by A1,Def2;
hence A is diagonal by MATRIX_1:def 10;
for k,m st[k,m] in Indices AA holds AA*(k,m)=ONE*(k,m)
proof
let k,m such that
A2: [k,m] in Indices AA;
A3: width A=n by MATRIX_0:24;
then len@Line(A,k)=n by CARD_1:def 7;
then reconsider L=@Line(A,k) as Element of TOP-REAL n by TOPREAL3:46;
len A=n by MATRIX_0:25;
then A4: AA*(k,m)=@L"*"Col(A,m) by A2,A3,MATRIX_3:def 4;
A5: Indices AA=[:S,S:] by MATRIX_0:24;
then A6: m in S by A2,ZFMISC_1:87;
then A7: Line(A,k).m=A*(k,m) by A3,MATRIX_0:def 7;
A8: Indices A=[:S,S:] by MATRIX_0:24;
A9: Indices ONE=[:S,S:] by MATRIX_0:24;
per cases;
suppose A10: m<>i;
then A11: AA*(k,m)=A*(k,m) by A1,A4,A6,A7,Th5;
per cases;
suppose A12: k<>m;
then ONE*(k,m)=0.F_Real by A2,A5,A9,MATRIX_1:def 3;
hence thesis by A1,A2,A5,A8,A11,A12,Def2;
end;
suppose A13: k=m;
then ONE*(k,m)=1.F_Real by A2,A5,A9,MATRIX_1:def 3;
hence thesis by A1,A2,A5,A8,A10,A11,A13,Def2;
end;
end;
suppose A14: m=i;
then A15: AA*(k,m)=-A*(k,m) by A4,A6,A7,Th6;
per cases;
suppose A16: k<>m;
then A*(k,m)=0.F_Real by A1,A2,A5,A8,Def2;
hence thesis by A2,A5,A9,A15,A16,MATRIX_1:def 3;
end;
suppose A17: k=m;
then AA*(k,m)=-(-1.F_Real) by A1,A14,A15,Def2;
hence thesis by A2,A5,A9,A17,MATRIX_1:def 3;
end;
end;
end;
then AA=ONE by MATRIX_0:27;
then A is_reverse_of A by MATRIX_6:def 2;
hence thesis by MATRIX_6:def 4;
end;
theorem Th8:
i in Seg n & i <> j implies (Mx2Tran AxialSymmetry(i,n)).p.j = p.j
proof
set A=AxialSymmetry(i,n),M=Mx2Tran A,Mp=M.p,S=Seg n;
assume A1: i in S & i<>j;
len Mp=n by CARD_1:def 7;
then A2: dom Mp=S by FINSEQ_1:def 3;
len p=n by CARD_1:def 7;
then A3: dom p=S by FINSEQ_1:def 3;
per cases;
suppose A4: j in S;
then 1<=j & j<=n by FINSEQ_1:1;
hence Mp.j=@p"*"Col(A,j) by MATRTOP1:18
.=p.j by A1,A4,Th5;
end;
suppose A5: not j in S;
then Mp.j={} by A2,FUNCT_1:def 2;
hence thesis by A3,A5,FUNCT_1:def 2;
end;
end;
theorem Th9:
i in Seg n implies (Mx2Tran AxialSymmetry(i,n)).p.i = -p.i
proof
set A=AxialSymmetry(i,n),M=Mx2Tran A,Mp=M.p,S=Seg n;
assume A1: i in S;
then 1<=i & i<=n by FINSEQ_1:1;
hence Mp.i=@p"*"Col(A,i) by MATRTOP1:18
.=-p.i by A1,Th6;
end;
theorem Th10:
i in Seg n implies (Mx2Tran AxialSymmetry(i,n)).p = p+*(i,-p.i)
proof
set S=Seg n,Mp=(Mx2Tran AxialSymmetry(i,n)).p,p0=p+*(i,-p.i);
A1: len p=n by CARD_1:def 7;
assume A2: i in S;
A3: for j st 1<=j & j<=n holds Mp.j=p0.j
proof
let j such that
A4: 1<=j & j<=n;
A5: j in S by A4;
A6: j in dom p by A1,A4,FINSEQ_3:25;
per cases;
suppose A7: j<>i;
then p0.j=p.j by FUNCT_7:32;
hence thesis by A2,A7,Th8;
end;
suppose A8: j=i;
then p0.j=-p.i by A6,FUNCT_7:31;
hence thesis by A5,A8,Th9;
end;
end;
len p0=len p & len Mp=n by CARD_1:def 7,FUNCT_7:97;
hence thesis by A1,A3;
end;
theorem Th11:
i in Seg n implies Mx2Tran AxialSymmetry(i,n) is {i}-support-yielding
proof
set M=Mx2Tran AxialSymmetry(i,n);
assume A1: i in Seg n;
let f be Function,x be set;
assume f in dom M;
then reconsider F=f as Point of TOP-REAL n by FUNCT_2:52;
assume A2: M.f.x<>f.x;
len(M.F)=n by CARD_1:def 7;
then A3: dom(M.F)=Seg n by FINSEQ_1:def 3;
A4: len F=n by CARD_1:def 7;
then A5: dom F=Seg n by FINSEQ_1:def 3;
per cases;
suppose A6: not x in Seg n;
then M.F.x={} by A3,FUNCT_1:def 2
.=F.x by A5,A6,FUNCT_1:def 2;
hence thesis by A2;
end;
suppose x in Seg n;
then x=i by A1,A2,A4,Th8;
hence thesis by TARSKI:def 1;
end;
end;
theorem Th12:
for a,b be Element of F_Real st a = cos r & b = sin r holds
Det block_diagonal(<*(a,b)][(-b,a),1.(F_Real,n)*>,0.F_Real) = 1.F_Real
proof
let a,b be Element of F_Real;
set A=(a,b)][(-b,a);
set ONE=1.(F_Real,n);
set B=block_diagonal(<*A,ONE*>,0.F_Real);
A1: n=0 or n>=1 by NAT_1:14;
A2: Det ONE=1_ F_Real or Det ONE=1.F_Real
by A1,MATRIXR2:41,MATRIX_7:16;
assume a=cos r & b=sin r;
then A3: (cos r)*cos r+(sin r)*sin r=a*a-b*(-b)
.=Det A by MATRIX_9:13;
A4: cos r=cos.r & sin r=sin.r by SIN_COS:def 17,def 19;
thus Det B=Det A*Det ONE by MATRIXJ1:52
.=1.F_Real by A2,A3,A4,SIN_COS:28;
end;
Lm2: 1<=i & i<j & j<=n implies
ex P be Permutation of Seg n st
P.1=i & P.2=j &
for k st k in Seg n & k>2 holds
(k<=i+1 implies P.k=k-2) &
(i+1<k & k<=j implies P.k=k-1) &
(k>j implies P.k=k)
proof
assume that
A1: 1<=i and
A2: i<j and
A3: j<=n;
i<=n by A2,A3,XXREAL_0:2;
then A4: i in Seg n by A1;
1<=j by A1,A2,XXREAL_0:2;
then A5: j in Seg n by A3;
reconsider S=Seg n as non empty Subset of NAT by A1,A2,A3;
defpred P[Nat,Nat] means
($1=1 implies $2=i) &
($1=2 implies $2=j) &
($1>2 implies ($1<=i+1 implies $2=$1-2) &
(i+1<$1 & $1<=j implies $2=$1-1) &
($1>j implies $2=$1));
A6: i+1<j+1 by A2,XREAL_1:8;
A7: for k st k in Seg n ex d be Element of S st P[k,d]
proof
let k;
assume A8: k in Seg n;
then A9: k<=n by FINSEQ_1:1;
A10: k<>0 by A8;
k <= 2 implies k = 0 or... or k = 2;
then per cases by A10;
suppose k=1 or k=2;
hence thesis by A4,A5;
end;
suppose A11: k>2 & k<>1 & k<>2;
then reconsider k2=k-2 as Nat by NAT_1:21;
k2>2-2 by A11,XREAL_1:8;
then A12: k2>=1 by NAT_1:14;
A13: k2<=k-0 by XREAL_1:10;
per cases by A8;
suppose A14: k<=i+1;
then k<j+1 by A6,XXREAL_0:2;
then A15: k<=j by NAT_1:13;
k2<=n by A9,A13,XXREAL_0:2;
then k2 in S by A12;
hence thesis by A11,A14,A15;
end;
suppose A16: k>i+1 & k<=j;
set k1=k2+1;
k1<=k1+1 by NAT_1:11;
then A17: k1<=n by A9,XXREAL_0:2;
k1>=1 by NAT_1:11;
then k1 in S by A17;
hence thesis by A11,A16;
end;
suppose k>i+1 & k>j & k in S;
hence thesis by A11;
end;
end;
end;
consider f be FinSequence of S such that
A18: len f=n & for k st k in Seg n holds P[k,f/.k] from FINSEQ_4:sch 1(A7);
A19: 1<j by A1,A2,XXREAL_0:2;
then 1<=n by A3,XXREAL_0:2;
then A20: 1 in S;
then A21: P[1,f/.1] by A18;
1+1<=j by A19,NAT_1:13;
then 2<=n by A3,XXREAL_0:2;
then A22: 2 in S;
then A23: P[2,f/.2] by A18;
A24: dom f=S by A18,FINSEQ_1:def 3;
then A25: f/.1=f.1 by A20,PARTFUN1:def 6;
A26: rng f c=S by FINSEQ_1:def 4;
then reconsider F=f as Function of S,S by A24,FUNCT_2:2;
A27: f/.2=f.2 by A22,A24,PARTFUN1:def 6;
S c=rng f
proof
let x be object;
assume A28: x in S;
then reconsider k=x as Nat;
set k1=k+1,k2=k1+1;
A29: 1<=k by A28,FINSEQ_1:1;
per cases by XXREAL_0:1;
suppose A30: k<i;
A31: k+2>(0 qua Nat)+2 by A29,XREAL_1:8;
A32: k1<=i by A30,NAT_1:13;
then k1<j by A2,XXREAL_0:2;
then k2<=j by NAT_1:13;
then 1<=k2 & k2<=n by A3,NAT_1:11,XXREAL_0:2;
then A33: k2 in S;
then P[k2,f/.k2] by A18;
then f.k2=k by A24,A31,A32,A33,PARTFUN1:def 6,XREAL_1:6;
hence thesis by A24,A33,FUNCT_1:def 3;
end;
suppose k=i;
hence thesis by A20,A21,A24,A25,FUNCT_1:def 3;
end;
suppose A34: k>i & k<j;
then k>1 by A1,A29,XXREAL_0:1;
then A35: k>=1+1 by NAT_1:13;
k1<=j by A34,NAT_1:13;
then 1<=k1 & k1<=n by A3,NAT_1:11,XXREAL_0:2;
then A36: k1 in S;
then P[k1,f/.k1] by A18;
then f.k1=k by A24,A34,A35,A36,NAT_1:13,PARTFUN1:def 6,XREAL_1:8;
hence thesis by A24,A36,FUNCT_1:def 3;
end;
suppose k=j;
hence thesis by A22,A23,A24,A27,FUNCT_1:def 3;
end;
suppose A37: k>j;
j>1 by A1,A2,XXREAL_0:2;
then A38: j>=1+1 by NAT_1:13;
P[k,f/.k] by A18,A28;
then f.k=k by A24,A37,A38,PARTFUN1:def 6,XXREAL_0:2;
hence thesis by A24,A28,FUNCT_1:def 3;
end;
end;
then rng F=S by A26,XBOOLE_0:def 10;
then A39: F is onto by FUNCT_2:def 3;
card S=card S;
then F is one-to-one by A39,FINSEQ_4:63;
then reconsider F as Permutation of Seg n by A39;
take F;
thus F.1=i & F.2=j by A20,A21,A22,A23,A24,PARTFUN1:def 6;
let k such that
A40: k in Seg n and
A41: k>2;
f/.k=f.k by A24,A40,PARTFUN1:def 6;
hence thesis by A18,A40,A41;
end;
Lm3: 1<=i & i<j & j<=n implies
ex A be Matrix of n,F_Real st Det A=1.F_Real
& A*(i,i)=cos r & A*(j,j)=cos r &
A*(i,j)=sin r & A*(j,i)=-sin r &
for k,m st[k,m] in Indices A holds
(k=m & k<>i & k<>j implies A*(k,k)=1.F_Real) &
(k<>m & {k,m}<>{i,j} implies A*(k,m)=0.F_Real)
proof
A1: now let k;
assume that
A2: k>=1 & k<>1 and
A3: k<>2;
k>1 by A2,XXREAL_0:1;
then k>=1+1 by NAT_1:13;
hence k>2 by A3,XXREAL_0:1;
end;
reconsider s=sin r,c =cos r as Element of F_Real by XREAL_0:def 1;
set S=Seg n;
assume that
A4: 1<=i and
A5: i<j and
A6: j<=n;
A7: 1<j by A4,A5,XXREAL_0:2;
then A8: 1+1<=j by NAT_1:13;
then reconsider n2=n-2 as Nat by A6,NAT_1:21,XXREAL_0:2;
consider P be Permutation of S such that
A9: P.1=i and A10: P.2=j and
for k st k in Seg n & k>2 holds
(k<=i+1 implies P.k=k-2) & (i+1<k & k<=j implies P.k=k-1) &
(k>j implies P.k=k) by A4,A5,A6,Lm2;
reconsider p=P as one-to-one Function;
dom P=S by FUNCT_2:52;
then A11: rng(p")=S by FUNCT_1:33;
rng P=S by FUNCT_2:def 3;
then dom(p")=S by FUNCT_1:33;
then reconsider P1=p" as one-to-one Function of S,S by A11,FUNCT_2:1;
P1 is onto by A11,FUNCT_2:def 3;
then reconsider P1 as Permutation of S;
A12: dom P=S by FUNCT_2:52;
1<=n by A6,A7,XXREAL_0:2;
then A13: 1 in S;
then A14: P1.(P.1)=1 by A12,FUNCT_1:34;
set A=(c,s)][(-s,c),ONE=1.(F_Real,n2),ao=<*A,ONE*>;
set B=block_diagonal(ao,0.F_Real);
A15: len A=2 by MATRIX_0:25;
then Len<*A*>=<*2*> by MATRIXJ1:15;
then A16: Sum Len<*A*>=2 by RVSUM_1:73;
len ONE=n2 by MATRIX_0:25;
then A17: Sum Len ao=2+n2 by A15,MATRIXJ1:16;
then reconsider B as Matrix of n,F_Real;
A18: Indices B=[:S,S:] by MATRIX_0:24;
2<=n by A6,A8,XXREAL_0:2;
then A19: 2 in S;
then A20: P1.(P.2)=2 by A12,FUNCT_1:34;
set pBp=((B*P1)@*P1)@;
A21: dom(P1)=S by FUNCT_2:52;
i<n by A5,A6,XXREAL_0:2;
then A22: i in S by A4;
then [i,i] in Indices B by A18,ZFMISC_1:87;
then A23: pBp*(i,i)=B*(1,1) by A9,A14,Th1;
take pBp;
A24: Indices pBp=[:S,S:] by MATRIX_0:24;
A25: Det B=1.F_Real by A17,Th12;
A26: block_diagonal(<*A*>,0.F_Real)=A by MATRIXJ1:34;
width A=2 by MATRIX_0:24;
then Width<*A*>=<*2*> by MATRIXJ1:19;
then A27: Sum Width<*A*>=2 by RVSUM_1:73;
1<j by A4,A5,XXREAL_0:2;
then A28: j in S by A6;
then [j,j] in Indices B by A18,ZFMISC_1:87;
then A29: pBp*(j,j)=B*(2,2) by A10,A20,Th1;
A30: block_diagonal(<*ONE*>,0.F_Real)=ONE by MATRIXJ1:34;
[1,1] in Indices A by MATRIX_0:48;
then A31: B*(1,1)=A*(1,1) by A26,A30,MATRIXJ1:26;
[2,1] in Indices A by MATRIX_0:48;
then A32: B*(2,1)=A*(2,1) by A26,A30,MATRIXJ1:26;
[1,2] in Indices A by MATRIX_0:48;
then A33: B*(1,2)=A*(1,2) by A26,A30,MATRIXJ1:26;
[2,2] in Indices A by MATRIX_0:48;
then A34: B*(2,2)=A*(2,2) by A26,A30,MATRIXJ1:26;
A35: <*A*>^<*ONE*>=ao;
[i,j] in Indices B by A18,A22,A28,ZFMISC_1:87;
then A36: pBp*(i,j)=B*(1,2) by A9,A10,A14,A20,Th1;
[j,i] in Indices B by A18,A22,A28,ZFMISC_1:87;
then pBp*(j,i)=B*(2,1) by A9,A10,A14,A20,Th1;
hence Det pBp=1.F_Real & pBp*(i,i)=cos r & pBp*(j,j)=cos r &
pBp*(i,j)=sin r & pBp*(j,i)=-sin r
by A23,A25,A29,A34,A33,A32,A31,A36,Th1,MATRIX_0:50;
let k,m such that
A37: [k,m] in Indices pBp;
A38: k in S by A24,A37,ZFMISC_1:87;
set Pk=P1.k,Pm=P1.m;
A39: rng(P1)=S by FUNCT_2:def 3;
then A40: Pk in S by A21,A38,FUNCT_1:def 3;
then A41: Pk>=1 by FINSEQ_1:1;
A42: m in S by A24,A37,ZFMISC_1:87;
then A43: Pm in S by A21,A39,FUNCT_1:def 3;
then A44: [Pk,Pm] in [:S,S:] by A40,ZFMISC_1:87;
A45: pBp*(k,m)=B*(Pk,Pm) by A18,A24,A37,Th1;
thus k=m & k<>i & k<>j implies pBp*(k,k)=1.F_Real
proof
assume that
A46: k=m and
A47: k<>i & k<>j;
Pk<>1 & Pk<>2 by A9,A10,A14,A20,A21,A22,A28,A38,A47,FUNCT_1:def 4;
then A48: Pk>2 by A1,A41;
then reconsider Pk2=Pk-2 as Nat by NAT_1:21;
Pk=Pk2+2 & Pk2>2-2 by A48,XREAL_1:8;
then A49: [Pk2,Pk2] in Indices ONE by A16,A18,A27,A30,A44,A46,MATRIXJ1:27;
then ONE*(Pk2,Pk2)=B*(Pk2+2,Pk2+2) by A16,A27,A30,MATRIXJ1:28;
hence thesis by A45,A46,A49,MATRIX_1:def 3;
end;
A50: Pm>=1 by A43,FINSEQ_1:1;
thus k<>m & {k,m}<>{i,j} implies pBp*(k,m)=0.F_Real
proof
assume that
A51: k<>m and
A52: {k,m}<>{i,j};
A53: Pk<>Pm by A21,A38,A42,A51,FUNCT_1:def 4;
per cases by A52;
suppose A54: k<>i & k<>j & m<>i & m<>j;
then Pk<>1 & Pk<>2 by A9,A10,A14,A20,A21,A22,A28,A38,FUNCT_1:def 4;
then A55: Pk>2 by A1,A41;
Pm<>1 & Pm<>2 by A9,A10,A14,A20,A21,A22,A28,A42,A54,FUNCT_1:def 4;
then A56: Pm>2 by A1,A50;
then reconsider Pk2=Pk-2,Pm2=Pm-2 as Nat by A55,NAT_1:21;
A57: Pk2>2-2 by A55,XREAL_1:8;
A58: Pk=Pk2+2 & Pm=Pm2+2;
Pm2>2-2 by A56,XREAL_1:8;
then A59: [Pk2,Pm2] in Indices ONE
by A16,A18,A27,A30,A44,A58,A57,MATRIXJ1:27;
then ONE*(Pk2,Pm2)=B*(Pk2+2,Pm2+2) by A16,A27,A30,MATRIXJ1:28;
hence thesis by A45,A53,A59,MATRIX_1:def 3;
end;
suppose A60: k=i & m<>j;
then Pm<>2 by A10,A20,A21,A28,A42,FUNCT_1:def 4;
then A61: Pm>2 by A1,A9,A14,A50,A53,A60;
Pk=1 by A9,A12,A13,A60,FUNCT_1:34;
hence thesis by A16,A18,A27,A35,A44,A45,A61,MATRIXJ1:29;
end;
suppose A62: k=j & m<>i;
then Pm<>1 by A9,A14,A21,A22,A42,FUNCT_1:def 4;
then A63: Pm>2 by A1,A10,A20,A50,A53,A62;
Pk=2 by A10,A12,A19,A62,FUNCT_1:34;
hence thesis by A16,A18,A27,A35,A44,A45,A63,MATRIXJ1:29;
end;
suppose A64: m=i & k<>j;
then Pk<>2 by A10,A20,A21,A28,A38,FUNCT_1:def 4;
then A65: Pk>2 by A1,A9,A14,A41,A53,A64;
Pm=1 by A9,A12,A13,A64,FUNCT_1:34;
hence thesis by A16,A18,A27,A35,A44,A45,A65,MATRIXJ1:29;
end;
suppose A66: m=j & k<>i;
then Pk<>1 by A9,A14,A21,A22,A38,FUNCT_1:def 4;
then A67: Pk>2 by A1,A10,A20,A41,A53,A66;
Pm=2 by A10,A12,A19,A66,FUNCT_1:34;
hence thesis by A16,A18,A27,A35,A44,A45,A67,MATRIXJ1:29;
end;
end;
end;
begin :: Proper Rotation
definition
let n; let r be Real;
let i,j such that
A1: 1 <= i & i < j & j <= n;
func Rotation(i,j,n,r) -> invertible Matrix of n,F_Real means :Def3:
it*(i,i) = cos r & it*(j,j) = cos r &
it*(i,j) = sin r & it*(j,i) =-sin r &
for k,m st [k,m] in Indices it holds
(k = m & k <> i & k <> j implies it*(k,k) = 1.F_Real) &
(k <> m & {k,m} <> {i,j} implies it*(k,m) = 0.F_Real);
existence
proof
consider A be Matrix of n,F_Real such that
A2: Det A=1.F_Real and
A3: A*(i,i)=cos r & A*(j,j)=cos r & A*(i,j)=sin r & A*(j,i)=-sin r &
for k,m st[k,m] in Indices A holds
(k=m & k<>i & k<>j implies A*(k,k)=1.F_Real) &
(k<>m & {k,m}<>{i,j} implies A*(k,m)=0.F_Real) by A1,Lm3;
Det A<>0.F_Real by A2;
then Det A is non zero;
then Det A is unital;
then A is invertible by LAPLACE:34;
hence thesis by A3;
end;
uniqueness
proof
let I1,I2 be invertible Matrix of n,F_Real such that
A4: I1*(i,i)=cos r & I1*(j,j)=cos r & I1*(i,j)=sin r & I1*(j,i)=-sin r and
A5: for k,m st[k,m] in Indices I1 holds(k=m & k<>i & k<>j implies
I1*(k,k)= 1.F_Real) & (k<>m & {k,m}<>{i,j} implies I1*(k,m)=0.F_Real) and
A6: I2*(i,i)=cos r & I2*(j,j)=cos r & I2*(i,j)=sin r & I2*(j,i)=-sin r and
A7: for k,m st[k,m] in Indices I2 holds(k=m & k<>i & k<>j implies
I2*(k,k)= 1.F_Real) & (k<>m & {k,m}<>{i,j} implies I2*(k,m)=0.F_Real);
for k,m st[k,m] in Indices I1 holds I1*(k,m)=I2*(k,m)
proof
let k,m;
assume A8: [k,m] in Indices I1;
then A9: [k,m] in Indices I2 by MATRIX_0:26;
per cases;
suppose k=m & (k=i or k=j) or k<>m & (k=i & m=j or k=j & m=i);
hence thesis by A4,A6;
end;
suppose A10: k=m & k<>i & k<>j;
then I1*(k,m)=1.F_Real by A5,A8;
hence thesis by A7,A9,A10;
end;
suppose A11: k<>m &
(k=i & m<>j or k=j & m<>i or m=i & k<>j or
m=j & k<>i or k<>i & k<>j & m<>i & m<>j);
then A12: {k,m}<>{i,j} by ZFMISC_1:6;
then I1*(k,m)=0.F_Real by A5,A8,A11;
hence thesis by A7,A9,A11,A12;
end;
end;
hence thesis by MATRIX_0:27;
end;
end;
theorem Th13:
1 <= i & i < j & j <= n implies Det Rotation(i,j,n,r)=1.F_Real
proof
assume A1: 1<=i & i<j & j<=n;
then consider A be Matrix of n,F_Real such that
A2: Det A=1.F_Real and
A3: A*(i,i)=cos r & A*(j,j)=cos r & A*(i,j)=sin r & A*(j,i)=-sin r &
for k,m st[k,m] in Indices A holds
(k=m & k<>i & k<>j implies A*(k,k)=1.F_Real) &
(k<>m & {k,m}<>{i,j} implies A*(k,m)=0.F_Real) by Lm3;
Det A<>0.F_Real by A2;
then Det A is non zero;
then Det A is unital;
then A is invertible by LAPLACE:34;
hence thesis by A1,A2,A3,Def3;
end;
theorem Th14:
1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j implies
@p"*"Col(Rotation(i,j,n,r),k) = p.k
proof
set S=Seg n;
assume that
A1: 1<=i & i<j & j<=n and
A2: k in Seg n and
A3: k<>i & k<>j;
set O=Rotation(i,j,n,r),C=Col(O,k);
A4: Indices O=[:S,S:] by MATRIX_0:24;
then A5: [k,k] in Indices O by A2,ZFMISC_1:87;
A6: len O=n by MATRIX_0:25;
then A7: dom O=S by FINSEQ_1:def 3;
len C=n by A6,MATRIX_0:def 8;
then A8: dom C=S by FINSEQ_1:def 3;
A9: now let m such that
A10: m in dom C and
A11: m<>k;
A12: [m,k] in Indices O by A2,A4,A8,A10,ZFMISC_1:87;
not k in {i,j} by A3,TARSKI:def 2;
then A13: {m,k}<>{i,j} by TARSKI:def 2;
thus C.m=O*(m,k) by A7,A8,A10,MATRIX_0:def 8
.=0.F_Real by A1,A11,A12,A13,Def3;
end;
len p=n by CARD_1:def 7;
then A14: dom p=S by FINSEQ_1:def 3;
C.k=O*(k,k) by A2,A7,MATRIX_0:def 8
.=1.F_Real by A1,A3,A5,Def3;
hence p.k=Sum(mlt(C,@p)) by A2,A8,A9,A14,MATRIX_3:17
.=@p"*"C by FVSUM_1:64;
end;
theorem Th15:
1 <= i & i < j & j <= n implies
@p"*"Col(Rotation(i,j,n,r),i) = p.i*(cos r)+p.j*(-sin r)
proof
assume that
A1: 1<=i and
A2: i<j and
A3: j<=n;
set O=Rotation(i,j,n,r),C=Col(O,i);
set S=Seg n;
1<=j by A1,A2,XXREAL_0:2;
then A4: j in S by A3;
A5: len O=n by MATRIX_0:25;
then A6: dom O=S by FINSEQ_1:def 3;
then A7: C.j=O*(j,i) by A4,MATRIX_0:def 8;
i<=n by A2,A3,XXREAL_0:2;
then A8: i in S by A1;
then A9: C.i=O*(i,i) by A6,MATRIX_0:def 8;
len p=n & len C=n by A5,CARD_1:def 7;
then A10: len mlt(@p,C)=n by MATRIX_3:6;
then A11: dom mlt(@p,C)=S by FINSEQ_1:def 3;
A12: Indices O=[:S,S:] by MATRIX_0:24;
for k st k in dom mlt(@p,C) & k<>i & k<>j holds mlt(@p,C).k=0.F_Real
proof
let k;
assume that
A13: k in dom mlt(@p,C) and
A14: k<>i and
A15: k<>j;
not k in {i,j} by A14,A15,TARSKI:def 2;
then A16: {k,i}<>{i,j} by TARSKI:def 2;
reconsider pk=@p.k as Element of F_Real by XREAL_0:def 1;
A17: [k,i] in Indices O by A8,A11,A12,A13,ZFMISC_1:87;
C.k=O*(k,i) by A6,A11,A13,MATRIX_0:def 8;
hence mlt(@p,C).k=pk*(O*(k,i)) by A13,FVSUM_1:60
.=pk*0.F_Real by A1,A2,A3,A14,A16,A17,Def3
.=0.F_Real;
end;
then A18: Sum mlt(@p,C)=mlt(@p,C)/.i+mlt(@p,C)/.j
by A2,A4,A8,A11,MATRIX15:7;
A19: i in dom mlt(@p,C) by A8,A10,FINSEQ_1:def 3;
reconsider pii=@p.i,pj=@p.j as Element of F_Real by XREAL_0:def 1;
A20: mlt(@p,C)/.i=mlt(@p,C).i by A8,A11,PARTFUN1:def 6
.=pii*(O*(i,i)) by A9,A19,FVSUM_1:60
.=(p.i)*(cos r) by A1,A2,A3,Def3;
mlt(@p,C)/.j=mlt(@p,C).j by A4,A11,PARTFUN1:def 6
.=pj*(O*(j,i)) by A4,A7,A11,FVSUM_1:60
.=(p.j)*(-sin r) by A1,A2,A3,Def3;
hence thesis by A18,A20;
end;
theorem Th16:
1 <= i & i < j & j <= n implies
@p"*"Col(Rotation(i,j,n,r),j) = p.i*(sin r)+p.j*(cos r)
proof
assume that
A1: 1<=i and
A2: i<j and
A3: j<=n;
set O=Rotation(i,j,n,r),C=Col(O,j);
set S=Seg n;
1<=j by A1,A2,XXREAL_0:2;
then A4: j in S by A3;
A5: len O=n by MATRIX_0:25;
then A6: dom O=S by FINSEQ_1:def 3;
then A7: C.j=O*(j,j) by A4,MATRIX_0:def 8;
A8: i<=n by A2,A3,XXREAL_0:2;
then A9: i in S by A1;
then A10: C.i=O*(i,j) by A6,MATRIX_0:def 8;
len p=n & len C=n by A5,CARD_1:def 7;
then len mlt(@p,C)=n by MATRIX_3:6;
then A11: dom mlt(@p,C)=S by FINSEQ_1:def 3;
then A12: i in dom mlt(@p,C) by A1,A8;
A13: Indices O=[:S,S:] by MATRIX_0:24;
for k st k in dom mlt(@p,C) & k<>i & k<>j holds mlt(@p,C).k=0.F_Real
proof
let k;
assume that
A14: k in dom mlt(@p,C) and
A15: k<>i and
A16: k<>j;
not k in {i,j} by A15,A16,TARSKI:def 2;
then A17: {k,j}<>{i,j} by TARSKI:def 2;
reconsider pk=@p.k as Element of F_Real by XREAL_0:def 1;
A18: [k,j] in Indices O by A4,A11,A13,A14,ZFMISC_1:87;
C.k=O*(k,j) by A6,A11,A14,MATRIX_0:def 8;
hence mlt(@p,C).k=pk*(O*(k,j)) by A14,FVSUM_1:60
.=pk*0.F_Real by A1,A2,A3,A16,A17,A18,Def3
.=0.F_Real;
end;
then A19: Sum mlt(@p,C)=mlt(@p,C)/.i+mlt(@p,C)/.j
by A2,A4,A9,A11,MATRIX15:7;
reconsider pii=@p.i,pj=@p.j as Element of F_Real by XREAL_0:def 1;
A20: mlt(@p,C)/.i=mlt(@p,C).i by A9,A11,PARTFUN1:def 6
.=pii*(O*(i,j)) by A10,A12,FVSUM_1:60
.=(p.i)*(sin r) by A1,A2,A3,Def3;
mlt(@p,C)/.j=mlt(@p,C).j by A4,A11,PARTFUN1:def 6
.=pj*(O*(j,j)) by A4,A7,A11,FVSUM_1:60
.=(p.j)*(cos r) by A1,A2,A3,Def3;
hence thesis by A19,A20;
end;
theorem Th17:
1 <= i & i < j & j <= n implies
Rotation(i,j,n,r1)*Rotation(i,j,n,r2) = Rotation(i,j,n,r1+r2)
proof
assume that
A1: 1<=i and
A2: i<j and
A3: j<=n;
set S=Seg n;
1<=j by A1,A2,XXREAL_0:2;
then A4: j in S by A3;
set O1=Rotation(i,j,n,r1);
set O2=Rotation(i,j,n,r2);
set O=Rotation(i,j,n,r1+r2);
set O12=O1*O2;
A5: width O1=n by MATRIX_0:24;
i<=n by A2,A3,XXREAL_0:2;
then A6: i in S by A1;
A7: Indices O1=[:S,S:] by MATRIX_0:24;
A8: Indices O12=[:S,S:] by MATRIX_0:24;
A9: Indices O=[:S,S:] by MATRIX_0:24;
A10: len O2=n by MATRIX_0:25;
for k,m st[k,m] in Indices O12 holds O12*(k,m)=O*(k,m)
proof
let k,m;
assume A11: [k,m] in Indices O12;
then A12: k in S by A8,ZFMISC_1:87;
A13: O12*(k,m)=Line(O1,k)"*"Col(O2,m) by A5,A10,A11,MATRIX_3:def 4;
len@Line(O1,k)=n by A5,CARD_1:def 7;
then reconsider L=@Line(O1,k) as Element of TOP-REAL n by TOPREAL3:46;
A14: m in S by A8,A11,ZFMISC_1:87;
then A15: L.m=O1*(k,m) by A5,MATRIX_0:def 7;
A16: @L=Line(O1,k);
A17: L.i=O1*(k,i) by A5,A6,MATRIX_0:def 7;
A18: L.j=O1*(k,j) by A4,A5,MATRIX_0:def 7;
per cases;
suppose A19: m=i;
then A20: Line(O1,k)"*"Col(O2,m)=L.i*(cos r2)+L.j*(-sin r2)
by A1,A2,A3,A16,Th15;
per cases;
suppose A21: k=i;
hence O12*(k,m)=(cos r1)*(cos r2)+L.j*(-sin r2)
by A1,A2,A3,A13,A17,A20,Def3
.=(cos r1)*(cos r2)+(sin r1)*(-sin r2) by A1,A2,A3,A18,A21,Def3
.=(cos r1)*(cos r2)-(sin r1)*(sin r2)
.=cos(r1+r2) by SIN_COS:75
.=O*(k,m) by A1,A2,A3,A19,A21,Def3;
end;
suppose A22: k=j;
hence O12*(k,m)=(-sin r1)*(cos r2)+L.j*(-sin r2) by A1,A2,A3,A13,A17
,A20,Def3
.=(-sin r1)*(cos r2)+(cos r1)*(-sin r2) by A1,A2,A3,A18,A22,Def3
.=-((sin r1)*(cos r2)+(cos r1)*(sin r2))
.=-sin(r1+r2) by SIN_COS:75
.=O*(k,m) by A1,A2,A3,A19,A22,Def3;
end;
suppose k<>j & k<>i;
then not k in {i,j} by TARSKI:def 2;
then A23: {k,i}<>{i,j} & {k,j}<>{i,j} by TARSKI:def 2;
A24: [k,j] in [:S,S:] by A4,A12,ZFMISC_1:87;
A25: [k,i] in [:S,S:] by A6,A12,ZFMISC_1:87;
then O1*(k,i)=0.F_Real by A1,A2,A3,A7,A23,Def3;
hence O12*(k,m)=0 *(cos r2)+0 *(-sin r2)
by A1,A2,A3,A7,A13,A17,A18,A20,A23,A24,Def3
.=O*(k,m) by A1,A2,A3,A9,A19,A23,A25,Def3;
end;
end;
suppose A26: m=j;
then A27: Line(O1,k)"*"Col(O2,m)=L.i*(sin r2)+L.j*(cos r2)
by A1,A2,A3,A16,Th16;
per cases;
suppose A28: k=i;
hence O12*(k,m)=(cos r1)*(sin r2)+L.j*(cos r2)
by A1,A2,A3,A13,A17,A27,Def3
.=(cos r1)*(sin r2)+(sin r1)*(cos r2) by A1,A2,A3,A18,A28,Def3
.=sin(r1+r2) by SIN_COS:75
.=O*(k,m) by A1,A2,A3,A26,A28,Def3;
end;
suppose A29: k=j;
hence O12*(k,m)=(-sin r1)*(sin r2)+L.j*(cos r2) by A1,A2,A3,A13,A17
,A27,Def3
.=(cos r1)*(cos r2)-(sin r1)*(sin r2) by A1,A2,A3,A18,A29,Def3
.=cos(r1+r2) by SIN_COS:75
.=O*(k,m) by A1,A2,A3,A26,A29,Def3;
end;
suppose k<>j & k<>i;
then not k in {i,j} by TARSKI:def 2;
then A30: {k,i}<>{i,j} & {k,j}<>{i,j} by TARSKI:def 2;
A31: [k,j] in [:S,S:] by A4,A12,ZFMISC_1:87;
[k,i] in [:S,S:] by A6,A12,ZFMISC_1:87;
then O1*(k,i)=0.F_Real by A1,A2,A3,A7,A30,Def3;
hence O12*(k,m)=0 *(sin r2)+0 *(cos r2)
by A1,A2,A3,A7,A13,A17,A18,A27,A30,A31,Def3
.=O*(k,m) by A1,A2,A3,A9,A26,A30,A31,Def3;
end;
end;
suppose A32: m<>i & m<>j;
then A33: O12*(k,m)=L.m by A1,A2,A3,A13,A14,A16,Th14;
A34: [k,m] in [:S,S:] by A11,MATRIX_0:24;
per cases;
suppose A35: k=m;
then O1*(k,m)=1.F_Real by A1,A2,A3,A7,A8,A11,A32,Def3;
hence thesis by A1,A2,A3,A9,A15,A32,A33,A34,A35,Def3;
end;
suppose A36: k<>m;
not m in {i,j} by A32,TARSKI:def 2;
then A37: {k,m}<>{i,j} by TARSKI:def 2;
then O1*(k,m)=0.F_Real by A1,A2,A3,A7,A8,A11,A36,Def3;
hence thesis by A1,A2,A3,A9,A15,A33,A34,A36,A37,Def3;
end;
end;
end;
hence thesis by MATRIX_0:27;
end;
Lm4: 1<=i & i<j & j<=n implies Rotation(i,j,n,r)@=Rotation(i,j,n,-r)
proof
set O1=Rotation(i,j,n,r),O2=Rotation(i,j,n,-r);
set S=Seg n;
assume A1: 1<=i & i<j & j<=n;
A2: Indices O2=[:S,S:] by MATRIX_0:24;
A3: Indices O1=[:S,S:] by MATRIX_0:24;
A4: Indices(O1@)=[:S,S:] by MATRIX_0:24;
for k,m st[k,m] in [:S,S:] holds O1@*(k,m)=O2*(k,m)
proof
A5: cos r=cos(-r) by SIN_COS:31;
let k,m;
A6: -sin r=sin(-r) by SIN_COS:31;
assume A7: [k,m] in [:S,S:];
then A8: [m,k] in [:S,S:] by A3,A4,MATRIX_0:def 6;
then A9: O1@*(k,m)=O1*(m,k) by A3,MATRIX_0:def 6;
per cases;
suppose A10: k=m & k=i;
then O1*(m,k)=cos r by A1,Def3;
hence thesis by A1,A5,A9,A10,Def3;
end;
suppose A11: k=m & k=j;
then O1*(m,k)=cos r by A1,Def3;
hence thesis by A1,A5,A9,A11,Def3;
end;
suppose A12: k=m & k<>i & k<>j;
then O1*(m,k)=1.F_Real by A1,A3,A7,Def3;
hence thesis by A1,A2,A7,A9,A12,Def3;
end;
suppose A13: k<>m & k=i & m=j;
then O1*(m,k)=-sin r by A1,Def3;
hence thesis by A1,A6,A9,A13,Def3;
end;
suppose A14: k<>m & k=i & m<>j;
then not m in {i,j} by TARSKI:def 2;
then A15: {m,k}<>{i,j} by TARSKI:def 2;
then O1*(m,k)=0.F_Real by A1,A3,A8,A14,Def3;
hence thesis by A1,A2,A7,A9,A14,A15,Def3;
end;
suppose A16: k<>m & k=j & m=i;
then O2*(k,m)=-sin(-r) by A1,Def3;
hence thesis by A1,A6,A9,A16,Def3;
end;
suppose A17: k<>m & k=j & m<>i;
then not m in {i,j} by TARSKI:def 2;
then A18: {m,k}<>{i,j} by TARSKI:def 2;
then O1*(m,k)=0.F_Real by A1,A3,A8,A17,Def3;
hence thesis by A1,A2,A7,A9,A17,A18,Def3;
end;
suppose A19: k<>m & k<>j & k<>i;
then not k in {i,j} by TARSKI:def 2;
then A20: {m,k}<>{i,j} by TARSKI:def 2;
then O1*(m,k)=0.F_Real by A1,A3,A8,A19,Def3;
hence thesis by A1,A2,A7,A9,A19,A20,Def3;
end;
suppose A21: k<>m & m<>j & m<>i;
then not m in {i,j} by TARSKI:def 2;
then A22: {m,k}<>{i,j} by TARSKI:def 2;
then O1*(m,k)=0.F_Real by A1,A3,A8,A21,Def3;
hence thesis by A1,A2,A7,A9,A21,A22,Def3;
end;
end;
hence thesis by A4,MATRIX_0:27;
end;
theorem Th18:
1 <= i & i < j & j <= n implies Rotation(i,j,n,0) = 1.(F_Real,n)
proof
set O=Rotation(i,j,n,0);
assume A1: 1<=i & i<j & j<=n;
A2: for k,m st[k,m] in Indices O & k<>m holds O*(k,m)=0.F_Real
proof
let k,m;
assume that
A3: [k,m] in Indices O and
A4: k<>m;
per cases;
suppose k=i & m=j or k=j & m=i;
then O*(k,m)=sin 0 or O*(k,m)=-sin 0 by A1,Def3;
hence thesis by SIN_COS:31;
end;
suppose k=i & m<>j;
then not m in {i,j} by A4,TARSKI:def 2;
then {k,m}<>{i,j} by TARSKI:def 2;
hence thesis by A1,A3,A4,Def3;
end;
suppose k=j & m<>i;
then not m in {i,j} by A4,TARSKI:def 2;
then {k,m}<>{i,j} by TARSKI:def 2;
hence thesis by A1,A3,A4,Def3;
end;
suppose m=i & k<>j;
then not k in {i,j} by A4,TARSKI:def 2;
then {k,m}<>{i,j} by TARSKI:def 2;
hence thesis by A1,A3,A4,Def3;
end;
suppose m=j & k<>i;
then not k in {i,j} by A4,TARSKI:def 2;
then {k,m}<>{i,j} by TARSKI:def 2;
hence thesis by A1,A3,A4,Def3;
end;
suppose k<>i & k<>j & m<>i & m<>j;
then not m in {i,j} by TARSKI:def 2;
then {k,m}<>{i,j} by TARSKI:def 2;
hence thesis by A1,A3,A4,Def3;
end;
end;
for k st[k,k] in Indices O holds O*(k,k)=1.F_Real
proof
let k;
assume A5: [k,k] in Indices O;
k=i or k=j or k<>i & k<>j;
hence thesis by A1,A5,Def3,SIN_COS:31;
end;
hence thesis by A2,MATRIX_1:def 3;
end;
Lm5: 1<=i & i<j & j<=n implies Rotation(i,j,n,r)~=Rotation(i,j,n,-r)
proof
assume A1: 1<=i & i<j & j<=n;
then A2: Rotation(i,j,n,r)*Rotation(i,j,n,-r)=Rotation(i,j,n,r+-r) by Th17
.=1.(F_Real,n) by A1,Th18;
Rotation(i,j,n,-r)*Rotation(i,j,n,r)=Rotation(i,j,n,-r+r) by A1,Th17
.=1.(F_Real,n) by A1,Th18;
then Rotation(i,j,n,r)is_reverse_of Rotation(i,j,n,-r) by A2,MATRIX_6:def 2;
hence thesis by MATRIX_6:def 4;
end;
theorem Th19:
1 <= i & i < j & j <= n implies
Rotation(i,j,n,r) is Orthogonal &
Rotation(i,j,n,r)~ = Rotation(i,j,n,-r)
proof
assume 1<=i & i<j & j<=n;
then Rotation(i,j,n,r)~ =Rotation(i,j,n,-r) &
Rotation(i,j,n,r)@=Rotation(i,j,n,-r) by Lm4,Lm5;
hence thesis by MATRIX_6:def 7;
end;
theorem Th20:
1 <= i & i < j & j <= n & k <> i & k <> j implies
(Mx2Tran Rotation(i,j,n,r)).p.k=p.k
proof
set O=Rotation(i,j,n,r),M=Mx2Tran O,Mp=M.p,S=Seg n;
assume A1: 1<=i & i<j & j<=n & k<>i & k<>j;
len Mp=n by CARD_1:def 7;
then A2: dom Mp=S by FINSEQ_1:def 3;
len p=n by CARD_1:def 7;
then A3: dom p=S by FINSEQ_1:def 3;
per cases;
suppose A4: k in S;
then 1<=k & k<=n by FINSEQ_1:1;
hence Mp.k=@p"*"Col(O,k) by MATRTOP1:18
.=p.k by A1,A4,Th14;
end;
suppose A5: not k in S;
then Mp.k={} by A2,FUNCT_1:def 2;
hence thesis by A3,A5,FUNCT_1:def 2;
end;
end;
theorem Th21:
1 <= i & i < j & j <= n implies
(Mx2Tran Rotation(i,j,n,r)).p.i=p.i*(cos r)+p.j*(-sin r)
proof
set O=Rotation(i,j,n,r),M=Mx2Tran O,Mp=M.p,S=Seg n;
assume that
A1: 1<=i and
A2: i<j & j<=n;
i<=n by A2,XXREAL_0:2;
hence Mp.i=@p"*"Col(O,i) by A1,MATRTOP1:18
.=p.i*(cos r)+p.j*(-sin r) by A1,A2,Th15;
end;
theorem Th22:
1 <= i & i < j & j <= n implies
(Mx2Tran Rotation(i,j,n,r)).p.j=p.i*(sin r)+p.j*(cos r)
proof
set O=Rotation(i,j,n,r),M=Mx2Tran O,Mp=M.p,S=Seg n;
assume that
A1: 1<=i & i<j and
A2: j<=n;
1<=j by A1,XXREAL_0:2;
hence Mp.j=@p"*"Col(O,j) by A2,MATRTOP1:18
.=p.i*(sin r)+p.j*(cos r) by A1,A2,Th16;
end;
theorem Th23:
1 <= i & i < j & j <= n implies
(Mx2Tran Rotation(i,j,n,r)).p=
(p| (i-' 1)) ^ <*p.i*(cos r)+p.j*(-sin r)*> ^
((p/^i) | (j-' i-' 1)) ^ <*p.i*(sin r)+p.j*(cos r)*> ^ (p/^j)
proof
assume that
A1: 1<=i and
A2: i<j and
A3: j<=n;
set M=Mx2Tran Rotation(i,j,n,r),Mp=M.p,i1=i-' 1,ji=j-' i;
A4: i<n by A2,A3,XXREAL_0:2;
A5: i1<i1+1 & i1=i-1 by A1,NAT_1:13,XREAL_1:233;
A6: now let k;
assume that
1<=k and
A7: k<=i1;
A8: (Mp|i1).k=Mp.k & (p|i1).k=p.k by A7,FINSEQ_3:112;
k<i by A5,A7,XXREAL_0:2;
hence (Mp|i1).k=(p|i1).k by A1,A2,A3,A8,Th20;
end;
A9: len Mp=n by CARD_1:def 7;
then A10: len(Mp|i1)=i1 by A5,A4,FINSEQ_1:59,XXREAL_0:2;
A11: len p=n by CARD_1:def 7;
then A12: len(p/^i)=n-i by A4,RFINSEQ:def 1;
A13: ji=j-i by A2,XREAL_1:233;
then A14: ji-' 1<ji-' 1+1 & ji<=n-i by A3,NAT_1:13,XREAL_1:6;
j-i>i-i by A2,XREAL_1:8;
then A15: ji-' 1=ji-1 by A13,NAT_1:14,XREAL_1:233;
A16: len(p/^j)=n-j by A3,A11,RFINSEQ:def 1;
A17: len(Mp/^i)=n-i by A9,A4,RFINSEQ:def 1;
then A18: len((Mp/^i) | (ji-' 1))=ji-' 1 by A14,A15,FINSEQ_1:59,XXREAL_0:2;
A19: ji-' 1<n-i by A14,A15,XXREAL_0:2;
A20: now let k;
assume that
A21: 1<=k and
A22: k<=ji-' 1;
A23: ((p/^i) | (ji-' 1)).k=(p/^i).k by A22,FINSEQ_3:112;
A24: k<=n-i by A19,A22,XXREAL_0:2;
then k in dom(Mp/^i) by A17,A21,FINSEQ_3:25;
then A25: (Mp/^i).k=Mp.(i+k) by A9,A4,RFINSEQ:def 1;
k<ji-' 1+1 by A22,NAT_1:13;
then A26: i+k<i+ji by A15,XREAL_1:8;
k in dom(p/^i) by A12,A21,A24,FINSEQ_3:25;
then A27: (p/^i).k=p.(i+k) by A11,A4,RFINSEQ:def 1;
k+i<>i & ((Mp/^i) | (ji-' 1)).k=(Mp/^i).k
by A21,A22,FINSEQ_3:112,NAT_1:14;
hence ((Mp/^i) | (ji-' 1)).k=((p/^i) | (ji-' 1)).k
by A1,A2,A3,A13,A25,A26,A27,A23,Th20;
end;
len((p/^i) | (ji-' 1))=ji-' 1 by A14,A15,A12,FINSEQ_1:59,XXREAL_0:2;
then A28: (Mp/^i) | (ji-' 1)=(p/^i) | (ji-' 1) by A20,A18;
A29: len(Mp/^j)=n-j by A3,A9,RFINSEQ:def 1;
now let k;
assume that
A30: 1<=k and
A31: k<=n-j;
k in dom(Mp/^j) by A29,A30,A31,FINSEQ_3:25;
then A32: (Mp/^j).k=Mp.(j+k) by A3,A9,RFINSEQ:def 1;
k in dom(p/^j) by A16,A30,A31,FINSEQ_3:25;
then A33: (p/^j).k=p.(j+k) by A3,A11,RFINSEQ:def 1;
j+k>=j & j+k<>j by A30,NAT_1:11,14;
hence (Mp/^j).k=(p/^j).k by A1,A2,A3,A32,A33,Th20;
end;
then A34: Mp/^j=p/^j by A16,A29;
len(p|i1)=i1 by A5,A11,A4,FINSEQ_1:59,XXREAL_0:2;
then A35: Mp|i1=p|i1 by A6,A10;
A36: Mp.i=p.i*(cos r)+p.j*(-sin r) by A1,A2,A3,Th21;
Mp=@@Mp;
then Mp=(Mp|i1)^<*Mp.i*>^((Mp/^i) | (j-' i-' 1))^<*Mp.j*>^(Mp/^j)
by A1,A2,A3,A9,FINSEQ_7:1;
hence thesis by A1,A2,A3,A34,A28,A35,A36,Th22;
end;
theorem Th24:
1 <= i & i < j & j <= n & s^2 <= (p.i)^2+(p.j)^2 implies
ex r st (Mx2Tran Rotation(i,j,n,r)).p.i = s
proof
set pk=p.i,pj=p.j,pkj=pk^2+pj^2,P=sqrt pkj;
assume that
A1: 1<=i & i<j & j<=n and
A2: s^2<=(p.i)^2+(p.j)^2;
A3: 0<=pk*pk & 0<=pj*pj by XREAL_1:63;
per cases;
suppose A4: pk<>0 or pj<>0;
A5: 0<=pk*pk by XREAL_1:63;
A6: P>0 by A3,A4,SQUARE_1:25;
then A7: s/P*P=s by XCMPLX_1:87;
A8: 0<=pj*pj by XREAL_1:63;
then pk^2+0<=pk^2+pj^2 by XREAL_1:6;
then A9: sqrt(pk^2)<=P by A5,SQUARE_1:26;
now per cases;
suppose A10: pk>=0;
then A11: pk<=P by A9,SQUARE_1:22;
then pk/P<=1 by A6,XREAL_1:185;
hence pk/P in [.-1,1 .] by A10,A11,XXREAL_1:1;
end;
suppose A12: pk<=0;
then -pk<=P by A9,SQUARE_1:23;
then -1<=pk/P by A6,XREAL_1:194;
hence pk/P in [.-1,1 .] by A6,A12,XXREAL_1:1;
end;
end;
then consider x be object such that
A13: x in dom sin and
x in [.-PI/2,PI/2.] and
A14: sin.x=pk/P by FUNCT_1:def 6,SIN_COS6:45;
A15: P*P=P^2
.=pkj by A5,A8,SQUARE_1:def 2;
0<=s*s by XREAL_1:63;
then A16: sqrt(s^2)<=P by A2,SQUARE_1:26;
now per cases;
suppose A17: s>=0;
then A18: s<=P by A16,SQUARE_1:22;
then s/P<=1 by A6,XREAL_1:185;
hence s/P in [.-1,1 .] by A17,A18,XXREAL_1:1;
end;
suppose A19: s<=0;
then -s<=P by A16,SQUARE_1:23;
then -1<=s/P by A6,XREAL_1:194;
hence s/P in [.-1,1 .] by A6,A19,XXREAL_1:1;
end;
end;
then consider y be object such that
y in dom sin and
A20: y in [.-PI/2,PI/2.] and
A21: sin.y=s/P by FUNCT_1:def 6,SIN_COS6:45;
reconsider y as Real by A20;
A22: P*pk/P=pk by A6,XCMPLX_1:89;
reconsider x as Element of REAL by A13,FUNCT_2:def 1;
A23: sin.x=sin x by SIN_COS:def 17;
(pk/P)*(pk/P)=(pk*pk)/pkj by A15,XCMPLX_1:76;
then (cos x)*(cos x)+(pk*pk)/pkj=1 by A14,A23,SIN_COS:29;
then (cos x)*(cos x)=1-(pk*pk)/pkj
.=pkj/pkj-(pk*pk)/pkj by A3,A4,XCMPLX_1:60
.=(pj*pj)/pkj
.=(pj/P)^2 by A15,XCMPLX_1:76;
then A24: (cos x)^2=(pj/P)^2;
per cases by A24,SQUARE_1:40;
suppose A25: cos x=pj/P;
take r=x-y;
-sin y=sin(-x+r) by SIN_COS:31
.=sin(-x)*cos r+cos(-x)*sin r by SIN_COS:75
.=(-sin x)*cos r+cos(-x)*sin r by SIN_COS:31
.=-(sin x)*cos r+(cos x)*sin r by SIN_COS:31
.=-(sin x)*cos r+-(cos x)*(-sin r);
then sin y=(sin x)*cos r+(cos x)*(-sin r);
hence s=P*(pk/P*cos r+pj/P*(-sin r))
by A7,A14,A21,A23,A25,SIN_COS:def 17
.=P*pk/P*cos r+P*pj/P*(-sin r)
.=pk*(cos r)+pj*(-sin r) by A6,A22,XCMPLX_1:89
.=(Mx2Tran Rotation(i,j,n,r)).p.i by A1,Th21;
end;
suppose A26: cos x=-(pj/P);
take r=y-x;
sin y=sin(x+r)
.=(sin x)*cos r+(cos x)*sin r by SIN_COS:75
.=pk/P*(cos r)+(pj/P)*(-sin r) by A14,A26,SIN_COS:def 17;
hence s=P*(pk/P*(cos r)+(pj/P)*(-sin r)) by A7,A21,SIN_COS:def 17
.=(P*pk/P)*cos r+(P*pj/P)*(-sin r)
.=pk*(cos r)+pj*(-sin r) by A6,A22,XCMPLX_1:89
.=(Mx2Tran Rotation(i,j,n,r)).p.i by A1,Th21;
end;
end;
suppose A27: pk=0 & pj=0;
take r=0;
set M=Mx2Tran Rotation(i,j,n,r);
M=Mx2Tran 1.(F_Real,n) by A1,Th18;
then A28: M=id TOP-REAL n by MATRTOP1:33;
s=0 by A2,A27,XREAL_1:63;
hence thesis by A27,A28;
end;
end;
Lm6: 1<=i & i<j & j<=n implies
(Mx2Tran Rotation(i,j,n,r)).p.i *
(Mx2Tran Rotation(i,j,n,r)).p.i +
(Mx2Tran Rotation(i,j,n,r)).p.j *
(Mx2Tran Rotation(i,j,n,r)).p.j
=p.i*p.i+p.j*p.j
proof
set pk=p.i,pj=p.j,pkj=pk^2+pj^2;
set M=Mx2Tran Rotation(i,j,n,r),S=sin r,C=cos r,Mp=M.p;
A1: C*C+S*S=1 by SIN_COS:29;
assume A2: 1<=i & i<j & j<=n;
then Mp.i=pk*C+pj*(-S) by Th21;
then A3: (Mp.i)*(Mp.i)=pk*pk*C*C-2*pk*pj*C*S+pj*pj*S*S;
Mp.j=pk*S+pj*C by A2,Th22;
then Mp.j*Mp.j=pk*pk*S*S+2*(pk*pj)*(C*S)+(pj*pj)*(C*C);
hence (Mp.i)*(Mp.i)+(Mp.j)*(Mp.j)=pk*pk*(C*C+S*S)+pj*pj*(C*C+S*S) by A3
.=pk*pk+pj*pj by A1;
end;
theorem Th25:
1 <= i & i < j & j <= n & s^2 <= (p.i)^2+(p.j)^2 implies
ex r st (Mx2Tran Rotation(i,j,n,r)).p.j = s
proof
set pk=p.i,pj=p.j,pkj=pk^2+pj^2,ps=pkj-s^2;
assume that
A1: 1<=i & i<j & j<=n and
A2: s^2<=pk^2+pj^2;
0<=s*s by XREAL_1:63;
then A3: ps<=pkj-0 by XREAL_1:6;
A4: s^2-s^2<=ps by A2,XREAL_1:6;
then (sqrt ps)^2=ps by SQUARE_1:def 2;
then consider r such that
A5: (Mx2Tran Rotation(i,j,n,r)).p.i=sqrt ps by A1,A3,Th24;
set M=Mx2Tran Rotation(i,j,n,r),Mp=M.p;
pkj=(sqrt ps)^2+(Mp.j)*(Mp.j) by A5,A1,Lm6
.=ps+(Mp.j)*(Mp.j) by A4,SQUARE_1:def 2;
then A6: s^2=(Mp.j)^2;
per cases by A6,SQUARE_1:40;
suppose Mp.j=s;
hence thesis;
end;
suppose A7: Mp.j=-s;
take R=r+PI;
thus(Mx2Tran Rotation(i,j,n,R)).p.j=p.i*(sin R)+p.j*(cos R) by A1,Th22
.=p.i*(-sin r)+p.j*(cos R) by SIN_COS:79
.=p.i*(-sin r)+p.j*(-cos r) by SIN_COS:79
.=-(p.i*(sin r)+p.j*(cos r))
.=-Mp.j by A1,Th22
.=s by A7;
end;
end;
theorem Th26:
1 <= i & i < j & j <= n implies
Mx2Tran Rotation(i,j,n,r) is {i,j}-support-yielding
proof
set M=Mx2Tran Rotation(i,j,n,r);
assume A1: 1<=i & i<j & j<=n;
let f be Function,x be set;
assume that
A2: f in dom M and
A3: M.f.x<>f.x;
reconsider p=f as Point of TOP-REAL n by A2,FUNCT_2:52;
len p=n by CARD_1:def 7;
then A4: dom p=Seg n by FINSEQ_1:def 3;
len(M.p)=n by CARD_1:def 7;
then A5: dom(M.p)=Seg n by FINSEQ_1:def 3;
per cases;
suppose A6: not x in Seg n;
then M.p.x={} by A5,FUNCT_1:def 2;
hence thesis by A3,A4,A6,FUNCT_1:def 2;
end;
suppose A7: x in Seg n;
M.p.x<>p.x by A3;
then x=i or x=j by A1,A7,Th20;
hence thesis by TARSKI:def 2;
end;
end;
begin :: Length-Preserving Linear Transformations
definition
let n;
let f be Function of TOP-REAL n,TOP-REAL n;
attr f is rotation means :Def4:
|.p.| = |.f.p.|;
end;
theorem Th27:
i in Seg n implies Mx2Tran AxialSymmetry(i,n) is rotation
proof
set S=Seg n,M=Mx2Tran AxialSymmetry(i,n);
assume A1: i in S;
let p be Point of TOP-REAL n;
len p=n by CARD_1:def 7;
then A2: i in dom p by A1,FINSEQ_1:def 3;
thus|.M.p.|=sqrt Sum sqr(p+*(i,-p.i)) by A1,Th10
.=sqrt((Sum sqr p)-(p.i)^2+(-p.i)^2) by A2,Th3
.=|.p.|;
end;
definition
let n;
let f be Function of TOP-REAL n,TOP-REAL n;
attr f is base_rotation means :Def5:
ex F be FinSequence of GFuncs the carrier of TOP-REAL n st
f = Product F &
for k st k in dom F ex i,j,r st
1 <= i & i < j & j <= n & F.k = Mx2Tran Rotation(i,j,n,r);
end;
registration
let n;
cluster id TOP-REAL n -> base_rotation;
coherence
proof
set S=the carrier of TOP-REAL n,G=GFuncs S;
take F=<*>the carrier of G;
thus Product F=1_G by GROUP_4:8
.=the_unity_wrt the multF of G by GROUP_1:22
.=id TOP-REAL n by MONOID_0:75;
let k;
assume k in dom F;
hence thesis;
end;
end;
registration
let n;
cluster base_rotation for Function of TOP-REAL n,TOP-REAL n;
existence
proof
id TOP-REAL n is base_rotation;
hence thesis;
end;
end;
registration
let n;
let f,g be base_rotation Function of TOP-REAL n,TOP-REAL n;
cluster f*g -> base_rotation for Function of TOP-REAL n,TOP-REAL n;
coherence
proof
consider F be FinSequence of GFuncs the carrier of TOP-REAL n such that
A1: f=Product F and
A2: for k st k in dom F ex i,j,r st 1<=i & i<j & j<=n &
F.k=(Mx2Tran Rotation(i,j,n,r)) by Def5;
consider G be FinSequence of GFuncs the carrier of TOP-REAL n such that
A3: g=Product G and
A4: for k st k in dom G ex i,j,r st 1<=i & i<j & j<=n &
G.k=(Mx2Tran Rotation(i,j,n,r)) by Def5;
f*g is base_rotation
proof
take GF=G^F;
thus Product GF=(Product G)*(Product F) by GROUP_4:5
.=f*g by A3,A1,MONOID_0:70;
let k;
assume A5: k in dom GF;
per cases by A5,FINSEQ_1:25;
suppose A6: k in dom G;
then G.k=GF.k by FINSEQ_1:def 7;
hence thesis by A4,A6;
end;
suppose ex m st m in dom F & k=len G+m;
then consider m such that
A7: m in dom F and
A8: k=len G+m;
GF.k=F.m by A7,A8,FINSEQ_1:def 7;
hence thesis by A2,A7;
end;
end;
hence thesis;
end;
end;
Lm7: 1<=i & i<j & j<=n implies Mx2Tran Rotation(i,j,n,r) is rotation
proof
assume A1: 1<=i & i<j & j<=n;
let p;
p=@@p;
then reconsider P=p as FinSequence of REAL;
set M=Mx2Tran Rotation(i,j,n,r),
Mp=M.p,p1=P| (i-' 1),p2=(P/^i) | (j-' i-' 1),
p3=P/^j,s=sin r,c =cos r;
reconsider pk=P.i,pj=P.j as Element of REAL by XREAL_0:def 1;
A2: sqr<*pk*>=<*pk^2*> by RVSUM_1:55;
reconsider pij1=pk*c+pj*(-s),pij2=pk*s+pj*c as Element of REAL
by XREAL_0:def 1;
A3: sqr<*pij1*>=<*pij1^2*> by RVSUM_1:55;
A4: sqr<*pij2*>=<*pij2^2*> by RVSUM_1:55;
A5: sqr<*pj*>=<*pj^2*> by RVSUM_1:55;
len p=n by CARD_1:def 7;
then p=p1^<*pk*>^p2^<*pj*>^p3 by A1,FINSEQ_7:1;
then sqr p=sqr(p1^<*pk*>^p2^<*pj*>)^sqr p3 by RVSUM_1:144
.=sqr(p1^<*pk*>^p2)^sqr<*pj*>^sqr p3 by RVSUM_1:144
.=sqr(p1^<*pk*>)^sqr p2^sqr<*pj*>^sqr p3 by RVSUM_1:144
.=sqr p1^sqr<*pk*>^sqr p2^sqr<*pj*>^sqr p3 by RVSUM_1:144;
then A6: Sum sqr p=Sum(sqr p1^sqr<*pk*>^sqr p2^sqr<*pj*>)+Sum sqr p3
by RVSUM_1:75
.=Sum(sqr p1^sqr<*pk*>^sqr p2)+pj^2+Sum sqr p3 by A5,RVSUM_1:74
.=Sum(sqr p1^sqr<*pk*>)+Sum sqr p2+pj^2+Sum sqr p3 by RVSUM_1:75
.=Sum sqr p1+pk^2+Sum sqr p2+pj^2+Sum sqr p3 by A2,RVSUM_1:74;
A7: c*c+s*s=1 by SIN_COS:29;
A8: pij1^2+pij2^2=pk*pk*(c*c+s*s)+pj*pj*(c*c+s*s)
.=pk^2+pj^2 by A7;
Mp=p1^<*pij1*>^p2^<*pij2*>^p3 by A1,Th23;
then sqr Mp=sqr(p1^<*pij1*>^p2^<*pij2*>)^sqr p3 by RVSUM_1:144
.=sqr(p1^<*pij1*>^p2)^sqr<*pij2*>^sqr p3 by RVSUM_1:144
.=sqr(p1^<*pij1*>)^sqr p2^sqr<*pij2*>^sqr p3 by RVSUM_1:144
.=sqr p1^sqr<*pij1*>^sqr p2^sqr<*pij2*>^sqr p3 by RVSUM_1:144;
then Sum sqr Mp=Sum(sqr p1^sqr<*pij1*>^sqr p2^sqr<*pij2*>)+Sum sqr p3
by RVSUM_1:75
.=Sum(sqr p1^sqr<*pij1*>^sqr p2)+pij2^2+Sum sqr p3 by A4,RVSUM_1:74
.=Sum(sqr p1^sqr<*pij1*>)+Sum sqr p2+pij2^2+Sum sqr p3 by RVSUM_1:75
.=Sum sqr p1+pij1^2+Sum sqr p2+pij2^2+Sum sqr p3 by A3,RVSUM_1:74;
hence |.p.| = |.Mp.| by A6,A8;
end;
theorem Th28:
1 <= i & i < j & j <= n implies Mx2Tran Rotation(i,j,n,r) is base_rotation
proof
assume A1: 1<=i & i<j & j<=n;
set S=the carrier of TOP-REAL n,G=GFuncs S;
reconsider M=Mx2Tran Rotation(i,j,n,r) as Element of G by MONOID_0:73;
take F=<*M*>;
thus Product F=Mx2Tran Rotation(i,j,n,r) by GROUP_4:9;
let k;
assume k in dom F;
then k in {1} by FINSEQ_1:2,38;
then A2: k=1 by TARSKI:def 1;
thus thesis by A1,A2;
end;
Lm8: for f,g be Function of TOP-REAL n,TOP-REAL n st
f is rotation & g is rotation holds f*g is rotation
proof
set TR=TOP-REAL n;
let f,g be Function of TR,TR such that
A1: f is rotation and
A2: g is rotation;
let p;
dom(f*g)=the carrier of TR by FUNCT_2:52;
hence |.(f*g).p.|=|.f.(g.p).| by FUNCT_1:12
.=|.g.p.| by A1
.=|.p.| by A2;
end;
registration
let n;
cluster base_rotation -> homogeneous additive rotation being_homeomorphism
for Function of TOP-REAL n,TOP-REAL n;
coherence
proof
set TR=TOP-REAL n,G=GFuncs the carrier of TR;
let f be Function of TR,TR;
assume f is base_rotation;
then consider F be FinSequence of G such that
A1: f=Product F and
A2: for k st k in dom F ex i,j,r st 1<=i & i<j & j<=n &
F.k=Mx2Tran Rotation(i,j,n,r);
defpred P[Nat] means
$1<=len F implies for g be Function of TR,TR st g=Product(F|$1) holds
g is homogeneous additive being_homeomorphism rotation;
A3: for m st P[m] holds P[m+1]
proof
let m;
assume A4: P[m];
set m1=m+1;
reconsider P=Product(F|m) as Function of TR,TR by MONOID_0:73;
assume A5: m1<=len F;
1<=m1 by NAT_1:11;
then A6: m1 in dom F by A5,FINSEQ_3:25;
then consider i,j,r such that
A7: 1<=i & i<j & j<=n and
A8: F.m1=(Mx2Tran Rotation(i,j,n,r)) by A2;
reconsider M=Mx2Tran Rotation(i,j,n,r) as Element of G by MONOID_0:73;
A9: F|m1=(F|m)^<*M*> by A6,A8,FINSEQ_5:10;
let g be Function of TR,TR such that
A10: g=Product(F|m1);
A11: g=Product(F|m)*M by A9,A10,GROUP_4:6
.=Mx2Tran Rotation(i,j,n,r)*P by MONOID_0:70;
A12: Mx2Tran Rotation(i,j,n,r) is rotation by A7,Lm7;
P is homogeneous additive being_homeomorphism rotation by A4,A5,NAT_1:13;
hence thesis by A11,A12,Lm8,TOPS_2:57;
end;
A13: F| (len F)=F by FINSEQ_1:58;
A14: P[0]
proof
assume 0<=len F;
let g be Function of TR,TR;
assume A15: g=Product(F|0);
F|0=<*>the carrier of G;
then g=1_G by A15,GROUP_4:8
.=the_unity_wrt the multF of G by GROUP_1:22
.=id TR by MONOID_0:75;
hence thesis;
end;
for m holds P[m] from NAT_1:sch 2(A14,A3);
hence thesis by A1,A13;
end;
end;
registration
let n;
let f be base_rotation Function of TOP-REAL n,TOP-REAL n;
cluster f" -> base_rotation;
coherence
proof
set TR=TOP-REAL n,G=GFuncs the carrier of TR;
defpred P[Nat] means
for F be FinSequence of G for f be Function of TR,TR st
len F=$1 & Product F=f &
(for k st k in dom F ex i,j,r st
1<=i & i<j & j<=n & F.k =(Mx2Tran Rotation(i,j,n,r)))
holds f" is base_rotation;
consider F be FinSequence of G such that
A1: f=Product F & for k st k in dom F ex i,j,r st 1<=i & i<j & j<=n &
F.k=(Mx2Tran Rotation(i,j,n,r)) by Def5;
A2: for i st P[i] holds P[i+1]
proof
let z be Nat such that
A3: P[z];
set z1=z+1;
let F be FinSequence of G;
let f be Function of TR,TR such that
A4: len F=z1 and
A5: Product F=f and
A6: for k st k in dom F ex i,j,r st 1<=i & i<j & j<=n &
F.k=(Mx2Tran Rotation(i,j,n,r));
set Fz=F|z;
reconsider fz=Product Fz as Function of TR,TR by MONOID_0:73;
1<=z1 by NAT_1:11;
then z1 in dom F by A4,FINSEQ_3:25;
then consider i,j,r such that
A7: 1<=i & i<j & j<=n and
A8: F.z1=Mx2Tran Rotation(i,j,n,r) by A6;
set m=Mx2Tran Rotation(i,j,n,r);
reconsider M=m as Element of G by MONOID_0:73;
F=Fz^<*M*> by A4,A8,FINSEQ_3:55;
then A9: f=(Product Fz)*M by A5,GROUP_4:6
.=m*fz by MONOID_0:70;
A10: dom Fz c=dom F by RELAT_1:60;
A11: now let k;
assume A12: k in dom Fz;
then Fz.k=F.k by FUNCT_1:47;
hence ex i,j,r st 1<=i & i<j & j<=n &
Fz.k=(Mx2Tran Rotation(i,j,n,r)) by A6,A10,A12;
end;
then A13: fz is base_rotation;
Det Rotation(i,j,n,r)<>0.F_Real &
Rotation(i,j,n,r)~=Rotation(i,j,n,-r) by A7,Lm5,Th13;
then A14: (m qua Function)"=Mx2Tran Rotation(i,j,n,-r) by MATRTOP1:43;
A15: rng m=[#]TR & m is one-to-one & dom m = [#]TR by TOPS_2:def 5;
then m is onto by FUNCT_2:def 3;
then A16: m"=(m qua Function)" by A15,TOPS_2:def 4;
len Fz=z by A4,FINSEQ_1:59,NAT_1:11;
then A17: fz" is base_rotation by A3,A11;
(fz is one-to-one) & dom fz=[#]TR & rng fz =[#]TR by A13,TOPS_2:def 5;
then A18: f"=fz"*m" by A9,A15,TOPS_2:53;
Mx2Tran Rotation(i,j,n,-r) is base_rotation by A7,Th28;
hence thesis by A14,A16,A17,A18;
end;
A19: P[0]
proof
let F be FinSequence of G;
let f be Function of TR,TR;
assume that
A20: len F=0 and
A21: Product F=f;
F=<*>the carrier of G by A20;
then A22: f=1_G by A21,GROUP_4:8
.=the_unity_wrt the multF of G by GROUP_1:22
.=id TR by MONOID_0:75;
then rng f=[#]TR;
then f is onto by FUNCT_2:def 3;
then f/"=(f qua Function)" by A22,TOPS_2:def 4;
hence thesis by A22,FUNCT_1:45;
end;
for i holds P[i] from NAT_1:sch 2(A19,A2);
then P[len F];
hence thesis by A1;
end;
end;
registration
let n;
let f,g be rotation Function of TOP-REAL n,TOP-REAL n;
cluster f*g -> rotation for Function of TOP-REAL n,TOP-REAL n;
coherence by Lm8;
end;
reserve f,f1,f2 for homogeneous additive Function of TOP-REAL n,TOP-REAL n;
definition
let n;
let f;
func AutMt f -> Matrix of n,F_Real means :Def6:
f = Mx2Tran it;
existence
proof
set T=n-VectSp_over F_Real;
set TR=TOP-REAL n;
reconsider B=MX2FinS 1.(F_Real,n) as OrdBasis of T by MATRLIN2:45;
A1: the carrier of T=REAL n by MATRIX13:102
.=the carrier of TR by EUCLID:22;
then reconsider F=f as Function of T,T;
now let v1,v2 be Vector of T;
reconsider P1=v1,P2=v2,FP1=F.v1,FP2=F.v2 as
Element of n-tuples_on the carrier of F_Real by MATRIX13:102;
A2: @@FP1=FP1 & @@FP2=FP2;
reconsider p1=v1,p2=v2 as Point of TR by A1;
A3: @@P1=P1 & @@P2=P2;
v1+v2=P1+P2 by MATRIX13:102
.=p1+p2 by A3,MATRTOP1:1;
hence F.(v1+v2)=f.p1+f.p2 by VECTSP_1:def 20
.=FP1+FP2 by A2,MATRTOP1:1
.=F.v1+F.v2 by MATRIX13:102;
end;
then A4: F is additive;
len B=n by MATRTOP1:19;
then reconsider A=AutMt(F,B,B) as Matrix of n,F_Real;
take A;
now let r be Scalar of F_Real,v be Vector of T;
reconsider p=v as Point of TR by A1;
reconsider P=v,FP=F.v as Element of n-tuples_on the carrier of F_Real
by MATRIX13:102;
r*v=r*P by MATRIX13:102
.=r*p by MATRIXR1:17;
hence F.(r*v)=r*f.p by TOPREAL9:def 4
.=r*FP by MATRIXR1:17
.=r*F.v by MATRIX13:102;
end;
then A5: F is homogeneous by MOD_2:def 2;
Mx2Tran A=Mx2Tran(AutMt(F,B,B),B,B) by MATRTOP1:20
.=f by A5,A4,MATRLIN2:34;
hence thesis;
end;
uniqueness by MATRTOP1:34;
end;
theorem Th29:
AutMt (f1*f2) = (AutMt f2) * (AutMt f1)
proof
set A1=AutMt f1,A2=AutMt f2;
A1:width A1=n & width A2 =n & len A2=n by MATRIX_0:24;
n =0 implies n=0;
then Mx2Tran(A2*A1)=(Mx2Tran A1) * (Mx2Tran A2) by A1,MATRTOP1:32
.= f1 *(Mx2Tran A2) by Def6
.= f1 *f2 by Def6;
hence thesis by Def6;
end;
theorem Th30:
k in X & k in Seg n implies
ex f st f is X-support-yielding base_rotation &
(card (X/\Seg n) > 1 implies f.p.k>=0) &
for i st i in X/\Seg n & i <> k holds f.p.i = 0
proof
assume that
A1: k in X and
A2: k in Seg n;
set TR=TOP-REAL n;
defpred P[Nat] means
$1<=n implies ex f be base_rotation Function of TR,TR st
f is(X/\Seg$1)\/{k}-support-yielding &
(card((X/\Seg$1)\/{k})>1 implies f.p.k>=0) &
for i st i in X/\Seg $1 & i<>k holds f.p.i=0;
A3: for z be Nat st P[z] holds P[z+1]
proof
let z be Nat;
set z1=z+1;
assume A4: P[z];
A5: Seg z1=Seg z\/{z1} by FINSEQ_1:9;
A6: Seg z1=Seg z\/{z1} by FINSEQ_1:9;
A7: z1 in X implies ((X/\Seg z)\/{k})\/{z1,k}=(X/\Seg z1)\/{k}
proof
assume z1 in X;
then A8: X\/{z1}=X by ZFMISC_1:40;
{z1,k}={z1}\/{k} by ENUMSET1:1;
hence ((X/\Seg z)\/{k})\/{z1,k}=(X/\Seg z)\/({k}\/({k}\/{z1}))
by XBOOLE_1:4
.=(X/\Seg z)\/({k}\/{k}\/{z1}) by XBOOLE_1:4
.=((X/\Seg z)\/{z1})\/{k} by XBOOLE_1:4
.=(X/\Seg z1)\/{k} by A6,A8,XBOOLE_1:24;
end;
assume A9: z1<=n;
then consider f be base_rotation Function of TR,TR such that
A10: f is(X/\Seg z)\/{k}-support-yielding and
A11: card((X/\Seg z)\/{k})>1 implies f.p.k>=0 and
A12: for m st m in X/\Seg z & m<>k holds f.p.m=0 by A4,NAT_1:13;
set z1=z+1;
per cases by XXREAL_0:1;
suppose A13: z1=k;
take f;
Seg z1\/{z1}=Seg z\/({z1}\/{z1}) by A5,XBOOLE_1:4
.=Seg z\/{z1};
then A14: (X/\Seg z1)\/{k}=(X\/{k})/\(Seg z\/{k}) by A13,XBOOLE_1:24
.=(X/\Seg z)\/{k} by XBOOLE_1:24;
hence f is (X/\Seg z1)\/{k}-support-yielding by A10;
thus card((X/\Seg z1)\/{k})>1 implies f.p.k>=0 by A11,A14;
let m;
assume that
A15: m in X/\Seg z1 and
A16: m<>k;
A17: m in Seg z1 by A15,XBOOLE_0:def 4;
A18: m in X by A15,XBOOLE_0:def 4;
not m in {z1} by A13,A16,TARSKI:def 1;
then m in Seg z by A5,A17,XBOOLE_0:def 3;
then m in X/\Seg z by A18,XBOOLE_0:def 4;
hence f.p.m=0 by A12,A16;
end;
suppose A19: not z1 in X;
take f;
A20: {z1}misses X by A19,ZFMISC_1:50;
A21: X/\Seg z1=(X/\Seg z)\/(X/\{z1}) by A5,XBOOLE_1:23
.=(X/\Seg z)\/{} by A20,XBOOLE_0:def 7
.=X/\Seg z;
hence f is(X/\Seg z1)\/{k}-support-yielding by A10;
thus card((X/\Seg z1)\/{k})>1 implies f.p.k>=0 by A11,A21;
let m;
assume that
A22: m in X/\Seg z1 and
A23: m<>k;
A24: m in Seg z1 by A22,XBOOLE_0:def 4;
A25: m in X by A22,XBOOLE_0:def 4;
then not m in {z1} by A19,TARSKI:def 1;
then m in Seg z by A5,A24,XBOOLE_0:def 3;
then m in X/\Seg z by A25,XBOOLE_0:def 4;
hence f.p.m=0 by A12,A23;
end;
suppose A26: z1<k & z1 in X;
set fp=f.p;
set S=(fp.z1)^2+(fp.k)^2;
A27: z1>=1 & k<=n by A2,FINSEQ_1:1,NAT_1:11;
A28: (fp.k)^2>=0 & (fp.z1)^2>=0 by XREAL_1:63;
then A29: (sqrt S)^2=S by SQUARE_1:def 2;
then consider r such that
A30: (Mx2Tran Rotation(z1,k,n,r)).fp.k=sqrt S by A26,A27,Th25;
reconsider M=Mx2Tran Rotation(z1,k,n,r) as
base_rotation Function of TR,TR by A26,A27,Th28;
take Mf=M*f;
A31: M is{z1,k}-support-yielding by A26,A27,Th26;
hence Mf is(X/\Seg z1)\/{k}-support-yielding by A7,A10,A26;
A32: dom Mf=the carrier of TR by FUNCT_2:52;
then A33: fp in dom M by FUNCT_1:11;
A34: Mf.p=M.fp by A32,FUNCT_1:12;
hence card((X/\Seg z1)\/{k})>1 implies Mf.p.k>=0
by A28,A30,SQUARE_1:def 2;
let i;
assume that
A35: i in X/\Seg z1 and
A36: i<>k;
A37: i in X by A35,XBOOLE_0:def 4;
i in Seg z1 by A35,XBOOLE_0:def 4;
then A38: i in Seg z or i in {z1} by A5,XBOOLE_0:def 3;
per cases by A38,TARSKI:def 1;
suppose A39: i in Seg z;
then A40: i in X/\Seg z by A37,XBOOLE_0:def 4;
i<=z by A39,FINSEQ_1:1;
then i<z1 by NAT_1:13;
then not i in {z1,k} by A36,TARSKI:def 2;
hence Mf.p.i=fp.i by A31,A33,A34
.=0 by A12,A36,A40;
end;
suppose i=z1;
then A41: (M.fp.i)*(M.fp.i)+S=S by A26,A27,A29,A30,Lm6;
thus Mf.p.i=M.fp.i by A32,FUNCT_1:12
.=0 by A41;
end;
end;
suppose A42: z1>k & z1 in X;
set fp=f.p;
set S=(fp.z1)^2+(fp.k)^2;
A43: 1<=k by A2,FINSEQ_1:1;
A44: (fp.k)^2>=0 & (fp.z1)^2>=0 by XREAL_1:63;
then A45: (sqrt S)^2=S by SQUARE_1:def 2;
then consider r such that
A46: (Mx2Tran Rotation(k,z1,n,r)).fp.k=sqrt S by A9,A42,A43,Th24;
reconsider M=Mx2Tran Rotation(k,z1,n,r) as
base_rotation Function of TR,TR by A9,A42,A43,Th28;
take Mf=M*f;
A47: M is{k,z1}-support-yielding by A9,A42,A43,Th26;
hence Mf is(X/\Seg z1)\/{k}-support-yielding by A7,A10,A42;
A48: dom Mf=the carrier of TR by FUNCT_2:52;
then A49: Mf.p=M.fp by FUNCT_1:12;
hence card((X/\Seg z1)\/{k})>1 implies Mf.p.k>=0
by A44,A46,SQUARE_1:def 2;
let i;
assume that
A50: i in X/\Seg z1 and
A51: i<>k;
A52: i in X by A50,XBOOLE_0:def 4;
i in Seg z1 by A50,XBOOLE_0:def 4;
then A53: i in Seg z or i in {z1} by A5,XBOOLE_0:def 3;
per cases by A53,TARSKI:def 1;
suppose A54: i in Seg z;
then i<=z by FINSEQ_1:1;
then i<z1 by NAT_1:13;
then A55: not i in {z1,k} by A51,TARSKI:def 2;
A56: i in X/\Seg z by A52,A54,XBOOLE_0:def 4;
fp in dom M by A48,FUNCT_1:11;
hence Mf.p.i=fp.i by A47,A49,A55
.=0 by A12,A51,A56;
end;
suppose i=z1;
then A57: (M.fp.i)*(M.fp.i)+S=S by A9,A42,A43,A45,A46,Lm6;
thus Mf.p.i=M.fp.i by A48,FUNCT_1:12
.=0 by A57;
end;
end;
end;
A58: P[0]
proof
assume 0<=n;
take f=id TR;
A59: f is{}-support-yielding
by FUNCT_1:17;
thus f is(X/\Seg 0)\/{k}-support-yielding by A59;
thus card((X/\Seg 0)\/{k})>1 implies f.p.k>=0 by CARD_2:42;
let m;
assume m in (X/\Seg 0);
hence thesis;
end;
for z be Nat holds P[z] from NAT_1:sch 2(A58,A3);
then consider f be base_rotation Function of TR,TR such that
A60: (f is(X/\Seg n)\/{k}-support-yielding) &
(card((X/\Seg n)\/{k})>1 implies f.p.k>=0) &
for i st i in X/\Seg n & i<>k holds f.p.i=0;
take f;
A61: (X/\Seg n)c=X by XBOOLE_1:17;
{k}c=X & {k}c=Seg n by A1,A2,ZFMISC_1:31;
then (X/\Seg n)\/{k}=X/\Seg n by XBOOLE_1:12,19;
hence thesis by A60,A61;
end;
theorem Th31:
for A be Subset of TOP-REAL n st f|A = id A holds f|Lin A = id Lin A
proof
set TR=TOP-REAL n;
let A be Subset of TOP-REAL n such that
A1: f|A=id A;
defpred P[Nat] means
for L be Linear_Combination of A st card Carrier L<=$1 holds
f.(Sum L)=Sum L;
A2: for i st P[i] holds P[i+1]
proof
let i;
assume A3: P[i];
set i1=i+1;
let L be Linear_Combination of A;
assume A4: card Carrier L<=i1;
per cases by A4,NAT_1:8;
suppose card Carrier L<=i;
hence thesis by A3;
end;
suppose A5: card Carrier L=i1;
then Carrier L is non empty;
then consider x be object such that
A6: x in Carrier L by XBOOLE_0:def 1;
reconsider x as Point of TR by A6;
reconsider X={x} as Subset of TR by ZFMISC_1:31;
consider K be Linear_Combination of X such that
A7: K.x=L.x by RLVECT_4:37;
L.x<>0 by A6,RLVECT_2:19;
then Carrier K c={x} & x in Carrier K by A7,RLVECT_2:19,def 6;
then A8: Carrier K={x} by ZFMISC_1:33;
{x}\/Carrier L=Carrier L by A6,ZFMISC_1:40;
then A9: Carrier(L-K)c=Carrier L by A8,RLVECT_2:55;
(L-K).x=L.x-K.x by RLVECT_2:54
.=0 by A7;
then not x in Carrier(L-K) by RLVECT_2:19;
then Carrier(L-K)c<Carrier L by A6,A9,XBOOLE_0:def 8;
then card Carrier(L-K)<i1 by A5,CARD_2:48;
then A10: card Carrier(L-K)<=i by NAT_1:13;
ZeroLC(TR)=-K--K by RLVECT_2:57
.=-K+--K by RLVECT_2:def 13
.=-K+K by RLVECT_2:53;
then L=L+(-K+K) by RLVECT_2:41
.=(L+-K)+K by RLVECT_2:40
.=(L-K)+K by RLVECT_2:def 13;
then A11: Sum L=Sum(L-K)+Sum K by RLVECT_3:1;
A12: Carrier L c=A by RLVECT_2:def 6;
then (f|A).x=f.x by A6,FUNCT_1:49;
then A13: f.x=x by A1,A6,A12,FUNCT_1:17;
Carrier(L-K)c=A by A9,A12;
then L-K is Linear_Combination of A by RLVECT_2:def 6;
then A14: f.Sum(L-K)=Sum(L-K) by A3,A10;
Sum K=L.x*x by A7,RLVECT_2:32;
then f.Sum K =Sum K by A13,TOPREAL9:def 4;
hence f.Sum L=Sum L by A11,A14,VECTSP_1:def 20;
end;
end;
set L=Lin A,cL=the carrier of L;
cL c=the carrier of TR by RLSUB_1:def 2;
then A15: f|L=f|cL by TMAP_1:def 3;
A16: P[0]
proof
let L be Linear_Combination of A;
assume card Carrier L<=0;
then Carrier L={};
then L is Linear_Combination of{}(the carrier of TR) by RLVECT_2:def 6;
then A17: Sum L=0.TR by RLVECT_2:31;
f.(0.TR)=f.((0 qua Real)*0.TR) by RLVECT_1:10
.=(0 qua Real)*f.(0.TR) by TOPREAL9:def 4
.=0.TR by RLVECT_1:10;
hence thesis by A17;
end;
A18: for i holds P[i] from NAT_1:sch 2(A16,A2);
A19: for x being object st x in cL holds(f|L).x=(id L).x
proof
let x be object;
assume A20: x in cL;
then x in L;
then consider K be Linear_Combination of A such that
A21: Sum K=x by RLVECT_3:14;
P[card Carrier K] by A18;
then A22: f.x=x by A21;
(f|L).x=f.x by A15,A20,FUNCT_1:49;
hence thesis by A20,A22,FUNCT_1:17;
end;
dom(f|L)=cL & dom(id L)=cL by FUNCT_2:def 1;
hence thesis by A19,FUNCT_1:2;
end;
theorem Th32:
for A be Subset of TOP-REAL n st f is rotation & f|A = id A
for i st i in Seg n & Base_FinSeq(n,i) in Lin A holds f.p.i = p.i
proof
set TR=TOP-REAL n;
let A be Subset of TR such that
A1: f is rotation and
A2: f|A=id A;
set L=Lin A,n0=0*n;
A3: f|L=id L by A2,Th31;
A4: len n0=n by CARD_1:def 7;
then A5: dom n0=Seg n by FINSEQ_1:def 3;
let k such that
A6: k in Seg n and
A7: Base_FinSeq(n,k) in L;
set n0k=n0+*(k,1);
A8: n0k=Base_FinSeq(n,k) by MATRIXR2:def 4;
set pk=p.k;
the carrier of L c=the carrier of TR by RLSUB_1:def 2;
then A9: f|L=f| (the carrier of L) by TMAP_1:def 3;
dom n0k=dom n0 by FUNCT_7:30;
then A10: len n0k=n by A4,FINSEQ_3:29;
A11: n0k=@@n0k;
then reconsider N0k=n0k as Point of TR by A10,TOPREAL3:46;
A12: n0k is Element of n-tuples_on REAL by A10,A11,FINSEQ_2:92;
A13: for p st p.k<>0 holds f.p.k=p.k
proof
let p;
assume A14: p.k<>0;
set fp=f.p,pk=p.k;
set pN=pk*N0k;
set ppN=p-pN;
A15: f.ppN+f.pN=f.(ppN+pN) by VECTSP_1:def 20;
len(f.ppN)=n & len(f.pN)=n by CARD_1:def 7;
then A16: |.f.(ppN+pN).|^2=|.f.ppN.|^2+2*|(f.pN,f.ppN)|+|.f.pN.|^2
by A15,EUCLID_2:11;
A17: (n|->pk).k=pk by A6,FINSEQ_2:57;
A18: pk*n0k=mlt(n|->pk,n0k) by A12,RVSUM_1:63
.=0*n+*(k,pk*1) by A17,TOPREALC:15
.=0*n+*(k,pk);
len fp=n by CARD_1:def 7;
then A19: dom fp=Seg n by FINSEQ_1:def 3;
A20: len ppN=n by CARD_1:def 7;
then dom ppN=Seg n by FINSEQ_1:def 3;
then A21: ppN.k=pk-pN.k by A6,VALUED_1:13;
len pN=n by CARD_1:def 7;
then A22: |.ppN+pN.|^2=|.ppN.|^2+2*|(pN,ppN)|+|.pN.|^2 by A20,EUCLID_2:11;
pN in L by A7,A8,RLSUB_1:21;
then A23: pN in the carrier of L;
then A24: pN=(f|L).pN by A3,FUNCT_1:17
.=f.pN by A9,A23,FUNCT_1:49;
|.ppN+pN.|=|.f.(ppN+pN).| & |.ppN.|=|.f.ppN.| by A1;
then |(pN,ppN)| =pk*((f.ppN).k) by A18,A16,A22,A24,TOPREALC:16;
then A25: pk*(ppN.k)=pk*((f.ppN).k) by A18,TOPREALC:16;
pN.k=pk by A6,A5,A18,FUNCT_7:31;
then A26: (f.ppN).k=0 by A14,A21,A25;
ppN+pN=p-(pN-pN) by RLVECT_1:29
.=p-0.TR by RLVECT_1:5
.=p by RLVECT_1:13;
then fp.k=(f.ppN.k)+f.pN.k by A6,A15,A19,VALUED_1:def 1
.=(f.ppN.k)+pk by A6,A5,A18,A24,FUNCT_7:31;
hence thesis by A26;
end;
per cases;
suppose p.k<>0;
hence thesis by A13;
end;
suppose p.k=0;
len(f.p)=n by CARD_1:def 7;
then A27: |.f.p+N0k.|^2=|.f.p.|^2+2*|(N0k,f.p)|+|.N0k.|^2
by A10,EUCLID_2:11;
len p=n by CARD_1:def 7;
then A28: |.p+N0k.|^2=|.p.|^2+2*|(N0k,p)|+|.N0k.|^2 by A10,EUCLID_2:11;
A29: N0k in the carrier of L by A7,A8;
then N0k=(f|L).N0k by A3,FUNCT_1:17
.=f.N0k by A9,A29,FUNCT_1:49;
then A30: f.(p+N0k)=f.p+N0k by VECTSP_1:def 20;
|.p+N0k.|=|.f.(p+N0k).| & |.f.p.|=|.p.| by A1;
then |(N0k,f.p)| =1*(p.k) by A27,A28,A30,TOPREALC:16;
then p.k=1*(f.p.k) by TOPREALC:16;
hence thesis;
end;
end;
theorem Th33:
for f be rotation Function of TOP-REAL n,TOP-REAL n st
f is X-support-yielding &
for i st i in X/\Seg n holds p.i = 0
holds f.p = p
proof
set TR=TOP-REAL n;
let f be rotation Function of TR,TR such that
A1: f is X-support-yielding and
A2: for i st i in X/\Seg n holds p.i=0;
set sp=sqr p,sfp=sqr(f.p);
A3: Sum sp>=0 by RVSUM_1:86;
Sum sfp>=0 & |.f.p.|=|.p.| by Def4,RVSUM_1:86;
then A4: Sum sp=Sum sfp by A3,SQUARE_1:28;
A5: len p=n by CARD_1:def 7; then
A6: len sp=n by RVSUM_1:143;
A7: len(f.p)=n by CARD_1:def 7; then
len sfp=n by RVSUM_1:143;
then reconsider sp,sfp as Element of n-tuples_on REAL by A6,FINSEQ_2:92;
A8: dom f=the carrier of TR by FUNCT_2:52;
A9: for i st i in Seg n holds sp.i<=sfp.i
proof
let i;
A10: sp.i=(p.i)^2 & sfp.i=(f.p.i)^2 by VALUED_1:11;
assume A11: i in Seg n;
per cases;
suppose i in X;
then i in X/\Seg n by A11,XBOOLE_0:def 4;
then p.i=0 by A2;
hence thesis by A10,XREAL_1:63;
end;
suppose not i in X;
hence thesis by A1,A8,A10;
end;
end;
for i st 1<=i & i<=n holds p.i=f.p.i
proof
let i;
A12: sp.i=(p.i)^2 by VALUED_1:11;
assume 1<=i & i<=n;
then A13: i in Seg n;
then A14: sp.i>=sfp.i & sp.i<=sfp.i by A4,A9,RVSUM_1:83;
per cases;
suppose i in X;
then A15: i in X/\Seg n by A13,XBOOLE_0:def 4;
then p.i=0 by A2;
then (f.p.i)^2=0 by A12,A14,VALUED_1:11;
then f.p.i=0;
hence thesis by A2,A15;
end;
suppose not i in X;
hence thesis by A1,A8;
end;
end;
hence thesis by A5,A7;
end;
theorem Th34:
i in Seg n & n >= 2 implies ex f st f is base_rotation & f.p = p+*(i,-p.i)
proof
set TR=TOP-REAL n;
assume that
A1: i in Seg n and
A2: n>=2;
A3: {i}c=Seg n by A1,ZFMISC_1:31;
A4: 1<=i by A1,FINSEQ_1:1;
card Seg n=n & card{i}=1 by CARD_2:42,FINSEQ_1:57;
then {i}<>Seg n by A2;
then {i}c<Seg n by A3,XBOOLE_0:def 8;
then consider j be object such that
A5: j in Seg n and
A6: not j in {i} by XBOOLE_0:6;
reconsider j as Nat by A5;
A7: j<>i by A6,TARSKI:def 1;
A8: 1<=j by A5,FINSEQ_1:1;
set p0=p+*(i,-p.i);
A9: len p0=len p by FUNCT_7:97;
A10: len p=n by CARD_1:def 7;
then A11: dom p=Seg n by FINSEQ_1:def 3;
A12: i<=n by A1,FINSEQ_1:1;
(p.i)*(p.i)>=0 & (p.j)*(p.j)>=0 by XREAL_1:63;
then A13: 0^2=0*0 & 0<=(p.i)^2+(p.j)^2;
A14: j<=n by A5,FINSEQ_1:1;
per cases by A7,XXREAL_0:1;
suppose A15: i<j;
then consider r such that
A16: (Mx2Tran Rotation(i,j,n,r)).p.i=0 by A4,A13,A14,Th24;
set s=sin r,c =cos r;
A17: 0=p.i*c+p.j*(-s) by A4,A14,A15,A16,Th21;
reconsider M=Mx2Tran Rotation(i,j,n,r+r) as
base_rotation Function of TR,TR by A4,A14,A15,Th28;
set Mp=M.p;
A18: cos(r+r)=c*c-s*s & sin(r+r)=s*c+s*c by SIN_COS:75;
A19: M is{i,j}-support-yielding by A4,A14,A15,Th26;
A20: for k st 1<=k & k<=n holds p0.k=Mp.k
proof
let k;
assume 1<=k & k<=n;
then A21: k in Seg n;
per cases;
suppose A22: i=k;
hence p0.k= -p.i*1 by A11,A21,FUNCT_7:31
.=-p.i*(s*s+c*c) by SIN_COS:29
.=p.i*(c*c-s*s)-(p.i*c*c)-(p.i*c*c)
.=p.i*(c*c-s*s)-(p.j*s*c)-(p.j*s*c) by A17
.=p.i*(c*c-s*s)+p.j*(-(s*c+s*c))
.=Mp.k by A4,A14,A15,A18,A22,Th21;
end;
suppose A23: j=k;
hence p0.k=p.j*1 by A15,FUNCT_7:32
.=p.j*(s*s+c*c) by SIN_COS:29
.=p.j*s*s+p.j*s*s+p.j*(c*c-s*s)
.=(p.i*c*s)+(p.i*c*s)+p.j*(c*c-s*s) by A17
.=p.i*(s*c+s*c)+p.j*(c*c-s*s)
.=Mp.k by A4,A14,A15,A18,A23,Th22;
end;
suppose A24: i<>k & j<>k;
A25: dom M=the carrier of TR by FUNCT_2:52;
p0.k=p.k & not k in {i,j} by A24,FUNCT_7:32,TARSKI:def 2;
hence thesis by A19,A25;
end;
end;
take M;
len Mp=n by CARD_1:def 7;
hence thesis by A9,A10,A20;
end;
suppose A26: j<i;
then consider r such that
A27: (Mx2Tran Rotation(j,i,n,r)).p.i=0 by A8,A12,A13,Th25;
set s=sin r,c =cos r;
A28: 0=p.j*s+p.i*c by A8,A12,A26,A27,Th22;
reconsider M=Mx2Tran Rotation(j,i,n,r+r) as
base_rotation Function of TR,TR by A8,A12,A26,Th28;
set Mp=M.p;
A29: cos(r+r)=c*c-s*s & sin(r+r)=s*c+s*c by SIN_COS:75;
A30: M is{i,j}-support-yielding by A8,A12,A26,Th26;
A31: for k st 1<=k & k<=n holds p0.k=Mp.k
proof
let k;
assume 1<=k & k<=n;
then A32: k in Seg n;
per cases;
suppose A33: i=k;
hence p0.k =-p.i*1 by A11,A32,FUNCT_7:31
.=-p.i*(s*s+c*c) by SIN_COS:29
.=(-p.i*c*c)+(-p.i*c)*c+p.i*(c*c-s*s)
.=p.j*s*c+p.j*s*c+p.i*(c*c-s*s) by A28
.=p.j*(s*c+s*c)+p.i*(c*c-s*s)
.=Mp.k by A8,A12,A26,A29,A33,Th22;
end;
suppose A34: j=k;
hence p0.k=p.j*1 by A26,FUNCT_7:32
.=p.j*(s*s+c*c) by SIN_COS:29
.=p.j*(c*c-s*s)+(p.j*s)*s+(p.j*s)*s
.=p.j*(c*c-s*s)+(-p.i*c)*s+(-p.i*c)*s by A28
.=p.j*(c*c-s*s)+p.i*(-(s*c+s*c))
.=Mp.k by A8,A12,A26,A29,A34,Th21;
end;
suppose A35: i<>k & j<>k;
A36: dom M=the carrier of TR by FUNCT_2:52;
p0.k=p.k & not k in {i,j} by A35,FUNCT_7:32,TARSKI:def 2;
hence thesis by A30,A36;
end;
end;
take M;
len Mp=n by CARD_1:def 7;
hence thesis by A9,A10,A31;
end;
end;
Lm9: for f be homogeneous additive rotation Function of TOP-REAL n,TOP-REAL n
st f is X-support-yielding & not i in X
holds f.Base_FinSeq(n,i) = Base_FinSeq(n,i)
proof
let f be homogeneous additive rotation Function of TOP-REAL n,TOP-REAL n;
set B=Base_FinSeq(n,i);
assume that
A1: f is X-support-yielding and
A2: not i in X;
A3: now let j;
assume A4: j in X/\Seg n;
then j in Seg n by XBOOLE_0:def 4;
then A5: 1<=j & j<=n by FINSEQ_1:1;
j<>i by A2,A4,XBOOLE_0:def 4;
hence B.j=0 by A5,MATRIXR2:76;
end;
len B=n by MATRIXR2:74;
then B is Point of TOP-REAL n by TOPREAL3:46;
hence thesis by A1,A3,Th33;
end;
theorem Th35:
f is {i}-support-yielding rotation implies
AutMt f = AxialSymmetry(i,n) or AutMt f = 1.(F_Real,n)
proof
set TR=TOP-REAL n;
set S={Base_FinSeq(n,j) where j is Element of NAT:1<=j & j<=n};
S c=the carrier of TR
proof
let x be object;
assume x in S;
then consider j be Element of NAT such that
A1: x=Base_FinSeq(n,j) and 1<=j & j<=n;
len Base_FinSeq(n,j)=n by MATRIXR2:74;
hence thesis by A1,TOPREAL3:46;
end;
then reconsider S as Subset of TR;
set M=Mx2Tran AxialSymmetry(n,i);
assume A2: f is{i}-support-yielding rotation;
A3: id TR=Mx2Tran 1.(F_Real,n) by MATRTOP1:33;
then A4: AutMt id TR=1.(F_Real,n) by Def6;
A5: dom f=the carrier of TR by FUNCT_2:52;
per cases;
suppose A6: not i in Seg n;
now let p be Point of TR;
A7: now let j;
assume 1<=j & j<=n;
then j<>i by A6;
then not j in {i} by TARSKI:def 1;
hence f.p.j=p.j by A2,A5;
end;
len(f.p)=n & len p=n by CARD_1:def 7;
hence f.p=p by A7;
end;
then f =id TR by FUNCT_2:124;
hence thesis by A3,Def6;
end;
suppose A8: i in Seg n;
then 1<=i & i<=n by FINSEQ_1:1;
then Base_FinSeq(n,i) in S by A8;
then reconsider B=Base_FinSeq(n,i) as Point of TR;
B=0*n+*(i,1) by MATRIXR2:def 4;
then A9: |.B.|=|.1 .| by A8,TOPREALC:13
.=1 by ABSVALUE:def 1;
set B0=0*n+*(i,f.B.i);
A10: len(0*n)=n by CARD_1:def 7;
A11: for j st 1<=j & j<=n holds f.B.j=B0.j
proof
let j;
assume A12: 1<=j & j<=n;
A13: j in dom(0*n) by A10,A12,FINSEQ_3:25;
per cases;
suppose j=i;
hence B0.j=f.B.j by A13,FUNCT_7:31;
end;
suppose A14: j<>i;
then A15: not j in {i} by TARSKI:def 1;
thus B0.j=(0*n).j by A14,FUNCT_7:32
.=0
.=B.j by A12,A14,MATRIXR2:76
.=f.B.j by A2,A5,A15;
end;
end;
len B0=len(0*n) & len(f.B)=n by CARD_1:def 7,FUNCT_7:97;
then A16: f.B=B0 by A10,A11;
then A17: |.B.|=|.B0.| by A2
.=|.f.B.i.| by A8,TOPREALC:13;
A18: for h be homogeneous additive rotation Function of TR,TR st
h|S = id S holds h = id TR
proof
let h be homogeneous additive rotation Function of TR,TR;
assume A19: h|S=id S;
A20: for x being object st x in dom id TR holds(id TR).x=h.x
proof
let x be object;
assume x in dom id TR;
then reconsider p=x as Point of TR;
set hp=h.p;
A21: len p=n & len hp=n by CARD_1:def 7;
A22: now let j;
assume A23: 1<=j & j<=n;
then A24: j in Seg n;
then Base_FinSeq(n,j) in S by A23;
then Base_FinSeq(n,j) in Lin S by RLVECT_3:15;
hence p.j=hp.j by A19,A24,Th32;
end;
thus thesis by A21,A22;
end;
dom h=the carrier of TR by FUNCT_2:def 1;
hence thesis by A20,FUNCT_1:2;
end;
per cases;
suppose A25: f.B.i>=0;
A26: dom(f|S)=S by A5,RELAT_1:62;
A27: f.B.i=1 by A9,A17,A25,ABSVALUE:def 1;
A28: for x being object st x in S holds(f|S).x=(id S).x
proof
let x be object;
assume A29: x in S;
then consider j be Element of NAT such that
A30: x=Base_FinSeq(n,j) and
1<=j and
j<=n;
A31: (f|S).x=f.x & (id S).x=x by A26,A29,FUNCT_1:17,47;
per cases;
suppose j=i;
hence thesis by A16,A27,A30,A31,MATRIXR2:def 4;
end;
suppose j<>i;
then not j in {i} by TARSKI:def 1;
hence thesis by A2,A30,A31,Lm9;
end;
end;
dom(id S)=S;
hence thesis by A2,A4,A18,A26,A28,FUNCT_1:2;
end;
suppose A32: f.B.i<0;
set MA=Mx2Tran AxialSymmetry(i,n);
MA is rotation by A8,Th27;
then reconsider MAf=MA*f as
homogeneous additive rotation Function of TR,TR by A2;
A33: dom MAf=the carrier of TR by FUNCT_2:52;
then A34: dom(MAf|S)=S by RELAT_1:62;
A35: (MA is{i}-support-yielding) & {i}\/{i}={i} by A8,Th11;
A36: for x being object st x in S holds(MAf|S).x=(id S).x
proof
let x be object;
assume A37: x in S;
then consider j be Element of NAT such that
A38: x=Base_FinSeq(n,j) and 1<=j & j<=n;
A39: (MAf|S).x=MAf.x & (id S).x=x by A34,A37,FUNCT_1:17,47;
per cases;
suppose A40: j=i;
A41: for k st 1<=k & k<=n holds MAf.B.k=B.k
proof
let k;
assume A42: 1<=k & k<=n;
then A43: k in Seg n;
per cases;
suppose A44: k=i;
thus MAf.B.k=MA.(f.B).k by A33,FUNCT_1:12
.=-(f.B).k by A43,A44,Th9
.=--1 by A9,A17,A32,A44,ABSVALUE:def 1
.=B.k by A42,A44,MATRIXR2:75;
end;
suppose A45: k<>i;
then A46: not k in {i} by TARSKI:def 1;
thus MAf.B.k=MA.(f.B).k by A33,FUNCT_1:12
.=(f.B).k by A8,A45,Th8
.=B.k by A2,A5,A46;
end;
end;
len(MAf.B)=n & len B=n by CARD_1:def 7;
hence thesis by A38,A39,A40,A41,FINSEQ_1:14;
end;
suppose j<>i;
then not j in {i} by TARSKI:def 1;
hence thesis by A2,A35,A38,A39,Lm9;
end;
end;
dom(id S)=S;
then A47: MAf=id TR by A18,A34,A36,FUNCT_1:2;
A48: dom MA=[#]TR by TOPS_2:def 5;
set R=AutMt f;
A49: rng MA=[#]TR by TOPS_2:def 5;
A50: MA is one-to-one by TOPS_2:def 5;
A51: the carrier of TR c=rng f
proof
let x be object;
assume A52: x in the carrier of TR;
then A53: MA.x in rng MA by A48,FUNCT_1:def 3;
then A54: MAf.(MA.x)=MA.(f.(MA.x)) by A33,A49,FUNCT_1:12;
f.(MA.x) in dom MA & MAf.(MA.x)=MA.x by A33,A47,A49,A53,FUNCT_1:11,18;
then x=f.(MA.x) by A48,A50,A52,A54,FUNCT_1:def 4;
hence thesis by A5,A49,A53,FUNCT_1:def 3;
end;
rng f c=the carrier of TR by RELAT_1:def 19;
then rng f=the carrier of TR by A51,XBOOLE_0:def 10;
then A55: f=(MA qua Function)" by A47,A49,A48,A50,FUNCT_1:42;
Det AxialSymmetry(i,n) = -1.F_Real by A8,Th4;
then f=Mx2Tran R & Det AxialSymmetry(i,n)<>0.F_Real by Def6;
then R=AxialSymmetry(i,n)~ by A55,MATRTOP1:43
.=AxialSymmetry(i,n) by A8,Th7;
hence thesis;
end;
end;
end;
theorem Th36:
f1 is rotation implies
ex f2 st f2 is base_rotation & f2*f1 is {n}-support-yielding
proof
set TR=TOP-REAL n;
assume A1: f1 is rotation;
set cTR=the carrier of TR;
set f=f1;
A2: dom f=cTR by FUNCT_2:52;
A3: rng f c=cTR by RELAT_1:def 19;
per cases;
suppose A4: n=0;
take I=id TR;
A5: dom id cTR=cTR;
A6:for h be Function,x be set st h in dom I & I.h.x<>h.x
holds x in {n} by FUNCT_1:17;
A7: cTR ={0.TR} by A4,EUCLID:22,77;
then rng id cTR=cTR & rng f=cTR by A3,ZFMISC_1:33;
then f=id cTR by A2,A5,A7,FUNCT_1:7;
then I*f=I by A2,RELAT_1:52;
hence thesis by A6;
end;
suppose n>0;
then reconsider n1=n-1 as Nat;
defpred P[Nat] means
$1<=n-1 implies for S be Subset of TR st S={Base_FinSeq(n,i) where i is
Element of NAT:1<=i & i<=$1}ex g be base_rotation Function of TR,TR st
(g*f) |S=id S;
set S={Base_FinSeq(n,i) where i is Element of NAT:1<=i & i<=n1};
S c=the carrier of TR
proof
let x be object;
assume x in S;
then consider j be Element of NAT such that
A8: x=Base_FinSeq(n,j) and
1<=j and
j<=n1;
len Base_FinSeq(n,j)=n by MATRIXR2:74;
hence thesis by A8,TOPREAL3:46;
end;
then reconsider S as Subset of TR;
A9: for k st P[k] holds P[k+1]
proof
let z be Nat;
assume A10: P[z];
set z1=z+1;
set SS={Base_FinSeq(n,i) where i is Element of NAT:1<=i & i<=z};
assume A11: z1<=n-1;
then reconsider n1=n-1 as Element of NAT by INT_1:3;
A12: n1<n1+1 by NAT_1:13;
then A13: z1<n by A11,XXREAL_0:2;
set B=Base_FinSeq(n,z1);
set X={i where i is Element of NAT:z1<=i & i<=n};
let S be Subset of TR such that
A14: S={Base_FinSeq(n,i) where i is Element of NAT:1<=i & i<=z1};
SS c=S
proof
let x be object;
assume x in SS;
then consider i be Element of NAT such that
A15: x=Base_FinSeq(n,i) & 1<=i and
A16: i<=z;
i<z1 by A16,NAT_1:13;
hence thesis by A14,A15;
end;
then reconsider SS as Subset of TR by XBOOLE_1:1;
z<n1 by A11,NAT_1:13;
then consider g be base_rotation Function of TR,TR such that
A17: (g*f) |SS=id SS by A10;
n in NAT by ORDINAL1:def 12;
then A18: n in X by A13;
n>=1 by A12,NAT_1:14;
then n in Seg n;
then A19: n in X/\Seg n by A18,XBOOLE_0:def 4;
A20: card{z1,n}=2 by A11,A12,CARD_2:57;
A21: 1<=z1 by NAT_1:11;
then A22: z1 in Seg n by A13;
B in S by A14,A21;
then reconsider B as Point of TR;
set gfB=(g*f).B;
A23: z1 in X by A13;
then consider h be homogeneous additive Function of TR,TR such that
A24: h is X-support-yielding base_rotation and
A25: card(X/\Seg n)>1 implies h.gfB.z1>=0 and
A26: for i st i in X/\Seg n & i<>z1 holds h.gfB.i=0 by A22,Th30;
reconsider hg=h*g as base_rotation Function of TR,TR by A24;
A27: dom(hg*f)=the carrier of TR by FUNCT_2:52;
A28: for x st x in SS holds(h*g*f).x=x & h.x=x
proof
let x such that
A29: x in SS;
reconsider B=x as Point of TR by A29;
((g*f) |SS).x=(g*f).x by A29,FUNCT_1:49;
then A30: (g*f).x=x by A17,A29,FUNCT_1:17;
A31: ex i be Element of NAT st x=Base_FinSeq(n,i) & 1<=i & i<=z by A29;
A32: for j st j in X/\Seg n holds B.j=0
proof
let j;
assume A33: j in X/\Seg n;
then j in X by XBOOLE_0:def 4;
then ex I be Element of NAT st I=j & z1<=I & I<=n;
then A34: z<j by NAT_1:13;
j in Seg n by A33,XBOOLE_0:def 4;
then 1<=j & j<=n by FINSEQ_1:1;
hence thesis by A31,A34,MATRIXR2:76;
end;
A35: hg*f=h*(g*f) by RELAT_1:36;
then (h*(g*f)).x=h.((g*f).x) by A27,A29,FUNCT_1:12;
hence thesis by A24,A30,A32,A35,Th33;
end;
z1 in X/\Seg n by A22,A23,XBOOLE_0:def 4;
then {z1,n}c=X/\Seg n by A19,ZFMISC_1:32;
then A36: 1+1<=card(X/\Seg n) by A20,NAT_1:43;
A37: for x being object st x in S holds((hg*f) |S).x=(id S).x
proof
let x be object such that
A38: x in S;
A39: (id S).x=x by A38,FUNCT_1:17;
A40: hg*f=h*(g*f) by RELAT_1:36;
A41: ((hg*f) |S).x=(hg*f).x by A38,FUNCT_1:49;
consider i be Element of NAT such that
A42: x=Base_FinSeq(n,i) and
A43: 1<=i and
A44: i<=z1 by A14,A38;
per cases by A44,NAT_1:8;
suppose i<=z;
then x in SS by A42,A43;
hence thesis by A28,A39,A41;
end;
suppose A45: i=z1;
set H=h.gfB;
A46: (h*(g*f)).x=h.gfB by A27,A40,A42,A45,FUNCT_1:12;
A47: len H=n by CARD_1:def 7;
A48: for j st j in Seg n & j<z1 holds h.gfB.j=0
proof
let j;
assume that
A49: j in Seg n and
A50: j<z1;
A51: 1<=j by A49,FINSEQ_1:1;
j<=z by A50,NAT_1:13;
then A52: Base_FinSeq(n,j) in SS by A49,A51;
then reconsider Bnj=Base_FinSeq(n,j) as Point of TR;
(h*g*f).Bnj=Bnj by A28,A52;
then A53: Bnj+H=(h*g*f).(Bnj+B) by A40,A42,A45,A46,VECTSP_1:def 20;
A54: len Bnj=n by CARD_1:def 7;
|.(h*g*f).(Bnj+B).|=|.Bnj+B.| by A1,A24,Def4;
then A55: |.Bnj+B.|^2=|.Bnj.|^2+2*|(H,Bnj)|+|.H.|^2
by A47,A53,A54,EUCLID_2:11;
A56: Bnj=0*n+*(j,1) by MATRIXR2:def 4;
len B=n by CARD_1:def 7;
then A57: |.Bnj+B.|^2=|.Bnj.|^2+2*|(B,Bnj)|+|.B.|^2
by A54,EUCLID_2:11;
A58: j<=n by A49,FINSEQ_1:1;
|.H.|=|.B.| by A1,A24,A42,A45,A46,Def4;
then (B.j)*1=|(H,Bnj)| by A55,A56,A57,TOPREALC:16
.=(H.j)*1 by A56,TOPREALC:16;
hence thesis by A50,A51,A58,MATRIXR2:76;
end;
set H=h.gfB;
set 0H=0*n+*(z1,H.z1);
A59: len(0*n)=n by CARD_1:def 7;
A60: for j st j in Seg n & j>z1 holds h.gfB.j=0
proof
let j;
assume that
A61: j in Seg n and
A62: j>z1;
j<=n by A61,FINSEQ_1:1;
then j in X by A61,A62;
then j in X/\Seg n by A61,XBOOLE_0:def 4;
hence thesis by A26,A62;
end;
A63: for j st 1<=j & j<=n holds H.j=0H.j
proof
let j;
assume 1<=j & j<=n;
then A64: j in Seg n;
then A65: j in dom(0*n) by A59,FINSEQ_1:def 3;
per cases;
suppose j=z1;
hence thesis by A65,FUNCT_7:31;
end;
suppose A66: j<>z1;
then j>z1 or j<z1 by XXREAL_0:1;
then A67: H.j=0 by A48,A60,A64;
0H.j=(0*n).j by A66,FUNCT_7:32;
hence thesis by A67;
end;
end;
len H=n & len 0H=len(0*n) by CARD_1:def 7,FUNCT_7:97;
then A68: 0H=H by A59,A63;
A69: |.gfB.|=|.B.| by A1,Def4;
A70: B=0*n+*(z1,1) by MATRIXR2:def 4;
then A71: |.B.|=|.1 .| by A22,TOPREALC:13
.=1 by ABSVALUE:def 1;
|.H.|=|.gfB.| & |.H.z1.|=H.z1
by A24,A25,A36,Def4,ABSVALUE:def 1,NAT_1:13;
then H=B by A22,A68,A70,A71,A69,TOPREALC:13;
hence thesis by A38,A39,A40,A42,A45,A46,FUNCT_1:49;
end;
end;
take hg;
dom(id S)=S & dom((hg*f) |S)=S by A27,RELAT_1:62;
hence thesis by A37,FUNCT_1:2;
end;
A72: P[0]
proof
assume 0<=n-1;
let S be Subset of TR such that
A73: S={Base_FinSeq(n,i) where i is Element of NAT:1<=i & i<=0};
A74: S={}
proof
assume S<>{};
then consider x be object such that
A75: x in S by XBOOLE_0:def 1;
ex i be Element of NAT st x=Base_FinSeq(n,i) & 1<=i & i<=0 by A73,A75;
hence contradiction;
end;
take g=id TOP-REAL n;
(g*f) |S={} by A74;
hence thesis by A74;
end;
for k holds P[k] from NAT_1:sch 2(A72,A9);
then consider g be base_rotation Function of TR,TR such that
A76: (g*f) |S=id S;
take g;
set gf=g*f;
thus g is base_rotation;
let p be Function;
let x be set;
assume that
A77: p in dom gf and
A78: gf.p.x<>p.x;
reconsider p as Point of TR by A77,FUNCT_2:52;
len(gf.p)=n by CARD_1:def 7;
then dom(gf.p)=Seg n by FINSEQ_1:def 3;
then A79: not x in Seg n implies (gf.p).x={} by FUNCT_1:def 2;
len p=n by CARD_1:def 7;
then dom p=Seg n by FINSEQ_1:def 3;
then A80: x in Seg n by A78,A79,FUNCT_1:def 2;
assume A81: not x in {n};
reconsider x as Nat by A80;
A82: x<=n by A80,FINSEQ_1:1;
x<>n by A81,TARSKI:def 1;
then x<n1+1 by A82,XXREAL_0:1;
then A83: x<=n1 by NAT_1:13;
x in NAT & 1<=x by A80,FINSEQ_1:1;
then Base_FinSeq(n,x) in S by A83;
then Base_FinSeq(n,x) in Lin S by RLVECT_3:15;
then gf.p.x=p.x by A1,A76,A80,Th32;
hence contradiction by A78;
end;
end;
Lm10: for M be Matrix of n,F_Real st Mx2Tran M is base_rotation holds
Det M=1.F_Real
proof
let M be Matrix of n,F_Real;
set TR=TOP-REAL n,G=GFuncs the carrier of TR;
assume Mx2Tran M is base_rotation;
then consider F be FinSequence of G such that
A1: Mx2Tran M=Product F and
A2: for k st k in dom F ex i,j,r st 1<=i & i<j & j<=n &
F.k=(Mx2Tran Rotation(i,j,n,r));
defpred P[Nat] means
$1<=len F implies Product(F|$1) is base_rotation Function of TR,TR &
for M be Matrix of n,F_Real st Mx2Tran M=Product(F|$1) holds Det M=1.F_Real;
A3: for m st P[m] holds P[m+1]
proof
let m;
A4: n=0 implies n=0;
set m1=m+1;
assume A5: P[m];
assume A6: m1<=len F;
then reconsider P=Product(F|m) as base_rotation Function of TR,TR
by A5,NAT_1:13;
set R=AutMt P;
A7: width R=n & len R=n by MATRIX_0:24;
1<=m1 by NAT_1:11;
then A8: m1 in dom F by A6,FINSEQ_3:25;
then consider i,j,r such that
A9: 1<=i & i<j & j<=n and
A10: F.m1=(Mx2Tran Rotation(i,j,n,r)) by A2;
set O=Rotation(i,j,n,r);
reconsider MO=Mx2Tran O as Element of G by MONOID_0:73;
F|m1=(F|m)^<*MO*> by A8,A10,FINSEQ_5:10;
then A11: Product(F|m1)=Product(F|m)*MO by GROUP_4:6
.=(Mx2Tran O)*P by MONOID_0:70;
Mx2Tran O is base_rotation by A9,Th28;
hence Product(F|m1) is base_rotation Function of TR,TR by A11;
A12: width O=n & len O=n by MATRIX_0:24;
let M be Matrix of n,F_Real such that
A13: Mx2Tran M=Product(F|m1);
Mx2Tran M=(Mx2Tran O)*Mx2Tran R by A11,A13,Def6
.=Mx2Tran(R*O) by A4,A12,A7,MATRTOP1:32;
then A14: M=R*O by MATRTOP1:34;
P=Mx2Tran R by Def6;
then A15: Det R=1.F_Real by A5,A6,NAT_1:13;
len R=n & Det O=1.F_Real by A9,Th13,MATRIX_0:25;
hence Det M=(1.F_Real)*1.F_Real by A14,A15,MATRIXR2:45
.=1.F_Real*1
.=1.F_Real;
end;
A16: F|len F=F by FINSEQ_1:58;
A17: P[0]
proof
assume 0<=len F;
A18: Mx2Tran 1.(F_Real,n)=id TR by MATRTOP1:33;
F|0=<*>the carrier of G;
then A19: Product(F|0)=1_G by GROUP_4:8
.=the_unity_wrt the multF of G by GROUP_1:22
.=id TR by MONOID_0:75;
hence Product(F|0) is base_rotation Function of TR,TR;
n=0 or n>=1 by NAT_1:14;
then A20: Det 1.(F_Real,n)=1_F_Real & n>=1 or Det 1.(F_Real,n)=1.F_Real &
n=0 by MATRIXR2:41,MATRIX_7:16;
let M be Matrix of n,F_Real;
thus thesis by A18,A19,A20,MATRTOP1:34;
end;
for m holds P[m] from NAT_1:sch 2(A17,A3);
hence thesis by A1,A16;
end;
begin :: Rotation Matrix Classification
theorem Th37:
f is rotation implies
(Det AutMt f = 1.F_Real iff f is base_rotation)
proof
set TR=TOP-REAL n,cTR=the carrier of TR;
set M=AutMt f;
set MM=Mx2Tran M;
A1: len M=n & width M=n by MATRIX_0:24;
A2: n=0 implies n=0;
A3: MM=f by Def6;
assume A4: f is rotation;
then consider h be homogeneous additive Function of TR,TR such that
A5: h is base_rotation and
A6: h*MM is{n}-support-yielding by A3,Th36;
set R=AutMt h;
A7: width R=n by MATRIX_0:24;
A8: h=Mx2Tran R by Def6;
A9: AutMt(h*MM)=1.(F_Real,n) or AutMt(h*MM)=AxialSymmetry(n,n)
by A4,A3,A5,A6,Th35;
Det M=1.F_Real implies MM is base_rotation
proof
assume A10: Det M=1.F_Real;
Det R=1.F_Real & n in NAT by A5,A8,Lm10,ORDINAL1:def 12;
then
A11: Det(M*R)=(1.F_Real)*(1.F_Real) by A10,MATRIXR2:45
.=1*1.F_Real
.=1.F_Real
.= 1;
A12: rng MM c=cTR by RELAT_1:def 19;
A13: rng h=[#]TR by A5,TOPS_2:def 5;
A14: dom h=[#]TR & h is one-to-one by A5,TOPS_2:def 5;
A15: dom(h")=[#]TR by A5,TOPS_2:def 5;
A16: id TR=Mx2Tran 1.(F_Real,n) by MATRTOP1:33;
h*MM=id cTR
proof
assume A17: h*MM<>id cTR;
n<>0
proof
A18: dom(h*MM)=cTR & dom id cTR=cTR by FUNCT_2:52;
assume n=0;
then A19: cTR ={0.TR} by EUCLID:22,77;
rng(h*MM)c=cTR by RELAT_1:def 19;
then rng id cTR=cTR & rng(h*MM)=cTR by A19,ZFMISC_1:33;
hence contradiction by A17,A18,A19,FUNCT_1:7;
end;
then A20: n in Seg n by FINSEQ_1:3;
Mx2Tran AutMt(h*MM)=h*MM by Def6;
then Mx2Tran AxialSymmetry(n,n)=Mx2Tran(M*R)
by A1,A2,A9,A8,A7,A16,A17,MATRTOP1:32;
then AxialSymmetry(n,n)=M*R by MATRTOP1:34;
then Det AxialSymmetry(n,n)= Det(M*R);
hence contradiction by A11,A20,Th4;
end;
then h"*(h*MM) =h" by A15,RELAT_1:52;
then h"=(h"*h)*MM by RELAT_1:36
.=(id cTR)*MM by A14,A13,TOPS_2:52
.=MM by A12,RELAT_1:53;
hence thesis by A5;
end;
hence thesis by A3,Lm10;
end;
theorem Th38:
f is rotation implies
(Det AutMt f = 1.F_Real or Det AutMt f = -1.F_Real)
proof
set M=AutMt f;
set MM=Mx2Tran M,TR=TOP-REAL n;
A1: len M=n & width M=n by MATRIX_0:24;
A2: n=0 implies n=0;
n=0 or n>=1 by NAT_1:14;
then A3: Det 1.(F_Real,n)=1_F_Real & n>=1 or Det 1.(F_Real,n)=1.F_Real & n=0
by MATRIXR2:41,MATRIX_7:16;
assume f is rotation;
then A4: MM is rotation by Def6;
then consider h be homogeneous additive Function of TR,TR such that
A5: h is base_rotation and
A6: h*MM is{n}-support-yielding by Th36;
set R=AutMt h;
A7: h=Mx2Tran R by Def6;
then n in NAT & Det R=1.F_Real by A5,Lm10,ORDINAL1:def 12;
then A8: Det(M*R)=Det M*(1.F_Real) by MATRIXR2:45
.=Det M*1
.=Det M;
width R=n by MATRIX_0:24;
then A9: h*MM=Mx2Tran(M*R) by A1,A2,A7,MATRTOP1:32;
per cases by A4,A5,A6,Th35;
suppose AutMt(h*MM)=1.(F_Real,n);
hence thesis by A3,A8,A9,Def6;
end;
suppose A10: AutMt(h*MM)<>1.(F_Real,n) & AutMt(h*MM)=AxialSymmetry(n,n);
set cTR=the carrier of TR;
n<>0
proof
A11: dom(h*MM)=cTR & dom id cTR=cTR by FUNCT_2:52;
assume n=0;
then A12: cTR ={0.TR} by EUCLID:22,77;
rng(h*MM)c=cTR by RELAT_1:def 19;
then rng id cTR=cTR & rng(h*MM)=cTR by A12,ZFMISC_1:33;
then h*MM=id TR by A11,A12,FUNCT_1:7
.=Mx2Tran 1.(F_Real,n) by MATRTOP1:33;
hence contradiction by A10,Def6;
end;
then n in Seg n by FINSEQ_1:3;
then Det AxialSymmetry(n,n)=-1.F_Real by Th4;
hence thesis by A8,A9,A10,Def6;
end;
end;
theorem Th39:
f1 is rotation & Det AutMt f1 = -1.F_Real & i in Seg n &
AutMt f2 = AxialSymmetry(i,n) implies f1*f2 is base_rotation
proof
set M=AutMt f1;
set A=AutMt f2;
assume that
A1: f1 is rotation and
A2: Det M=-1.F_Real and
A3: i in Seg n and
A4: A=AxialSymmetry(i,n);
A5: f2=Mx2Tran AxialSymmetry(i,n) by A4,Def6;
reconsider MF=(Mx2Tran M)*f2 as homogeneous additive Function of TOP-REAL n,
TOP-REAL n;
set A=AxialSymmetry(i,n);
set R=AutMt MF;
A6: n=0 implies n=0;
A7: MF=Mx2Tran R & width M=n by Def6,MATRIX_0:24;
len A=n & width A=n by MATRIX_0:24;
then Mx2Tran R=Mx2Tran(A*M) by A5,A6,A7,MATRTOP1:32;
then A8: R=A*M by MATRTOP1:34;
n in NAT & Det A=-1.F_Real by A3,Th4,ORDINAL1:def 12;
then A9: Det R=(-1.F_Real)*(-1.F_Real) by A2,A8,MATRIXR2:45
.=(-1.F_Real)*(-1)
.=1.F_Real;
A10: Mx2Tran M=f1 by Def6;
f2 is rotation by A3,A5,Th27;
hence thesis by A10,A1,A9,Th37;
end;
Lm11:f is base_rotation implies
AutMt f is Orthogonal
proof
set TR=TOP-REAL n,G=GFuncs the carrier of TR;
assume f is base_rotation;
then consider F be FinSequence of G such that
A1: f=Product F and
A2: for k st k in dom F ex i,j,r st 1<=i & i<j & j<=n &
F.k=(Mx2Tran Rotation(i,j,n,r));
A3:f = Mx2Tran AutMt f by Def6;
defpred P[Nat] means
$1<=len F implies Product(F|$1) is base_rotation Function of TR,TR &
for M be Matrix of n,F_Real st Mx2Tran M=Product(F|$1) holds M is Orthogonal;
A4: for m st P[m] holds P[m+1]
proof
let m;
A5: n=0 implies n=0;
set m1=m+1;
assume A6: P[m];
assume A7: m1<=len F;
then reconsider P=Product(F|m) as base_rotation Function of TR,TR
by A6,NAT_1:13;
set R=AutMt P;
A8: width R=n & len R = n by MATRIX_0:24;
1<=m1 by NAT_1:11;
then A9: m1 in dom F by A7,FINSEQ_3:25;
then consider i,j,r such that
A10: 1<=i & i<j & j<=n and
A11: F.m1=(Mx2Tran Rotation(i,j,n,r)) by A2;
set O=Rotation(i,j,n,r);
reconsider MO=Mx2Tran O as Element of G by MONOID_0:73;
F|m1=(F|m)^<*MO*> by A9,A11,FINSEQ_5:10;
then A12: Product(F|m1)=Product(F|m)*MO by GROUP_4:6
.=(Mx2Tran O) * P by MONOID_0:70;
Mx2Tran O is base_rotation by A10,Th28;
hence Product(F|m1) is base_rotation Function of TR,TR by A12;
A13: width O=n & len O=n by MATRIX_0:24;
let M be Matrix of n,F_Real such that
A14: Mx2Tran M=Product(F|m1);
Mx2Tran M=(Mx2Tran O)* (Mx2Tran R) by A12,A14,Def6
.=Mx2Tran(R*O) by A5,A13,A8,MATRTOP1:32;
then A15: M=R*O by MATRTOP1:34;
P=Mx2Tran R by Def6;
then A16: R is Orthogonal & n > i by A10,A6,A7,NAT_1:13,XXREAL_0:2;
len R=n & O is Orthogonal & n > 0 by A10,Th19,MATRIX_0:25;
hence M is Orthogonal by A15,A16,MATRIX_6:46;
end;
A17: F|len F=F by FINSEQ_1:58;
A18: P[0]
proof
assume 0<=len F;
A19: Mx2Tran 1.(F_Real,n)=id TR by MATRTOP1:33;
F|0=<*>the carrier of G;
then A20: Product(F|0)=1_G by GROUP_4:8
.=the_unity_wrt the multF of G by GROUP_1:22
.=id TR by MONOID_0:75;
hence Product(F|0) is base_rotation Function of TR,TR;
A21: 1.(F_Real,n) is Orthogonal by MATRIX_6:58;
let M be Matrix of n,F_Real;
thus thesis by A19,A20,A21,MATRTOP1:34;
end;
for m holds P[m] from NAT_1:sch 2(A18,A4);
hence thesis by A1,A17,A3;
end;
registration
let n;
let f be rotation homogeneous additive Function of TOP-REAL n,TOP-REAL n;
cluster AutMt f -> Orthogonal;
coherence
proof
set TR=TOP-REAL n,cTR=the carrier of TR,M=AutMt f;
per cases by Th37,Th38;
suppose Det M=1.F_Real;
then f is base_rotation by Th37;
hence thesis by Lm11;
end;
suppose A1: Det M=-1.F_Real & not f is base_rotation;
A2:n>0
proof
A3: dom f=cTR & dom id cTR=cTR by FUNCT_2:52;
assume n <= 0;
then n=0;
then A4: cTR = {0.TR} by EUCLID:22,77;
rng f c=cTR by RELAT_1:def 19;
then rng id cTR=cTR & rng f=cTR by A4,ZFMISC_1:33;
then f=id TR by A3,A4,FUNCT_1:7;
hence contradiction by A1;
end;
then A5: n in Seg n by FINSEQ_1:3;
set A=AxialSymmetry(n,n),MA=Mx2Tran A;
AutMt MA=A by Def6;
then A6: f*MA is base_rotation by A1,A5,Th39;
A is diagonal & A~=A by A5,Th7;
then A@ = A~ by Th2;
then A7:A is Orthogonal & AutMt (f*MA) is Orthogonal
by A6,Lm11,MATRIX_6:def 7;
A8:AutMt (f*MA) = AutMt (MA)*M by Th29
.= A*M by Def6;
A~ is_reverse_of A by MATRIX_6:def 4;
then A9:A~*A = 1.(F_Real,n) by MATRIX_6:def 2;
width (A~)=n & len A= n & width A = n & len M = n by MATRIX_0:24;
then A~*(A*M) = (A~*A)*M by MATRIX_3:33
.= M by A9,MATRIX_3:18;
hence thesis by A2,A7,A8,MATRIX_6:59;
end;
end;
end;
registration
let n;
cluster homogeneous additive rotation -> being_homeomorphism for
Function of TOP-REAL n,TOP-REAL n;
coherence
proof
set TR=TOP-REAL n,cTR=the carrier of TR;
let f be Function of TR,TR;
assume A1: f is homogeneous additive rotation;
then reconsider F=f as homogeneous additive Function of TR,TR;
set M=AutMt F;
per cases by A1,Th37,Th38;
suppose Det M=1.F_Real;
then f is base_rotation by A1,Th37;
hence thesis;
end;
suppose A2: Det M=-1.F_Real & not f is base_rotation;
n<>0
proof
A3: dom f=cTR & dom id cTR=cTR by FUNCT_2:52;
assume n=0;
then A4: cTR = {0.TR} by EUCLID:22,77;
rng f c=cTR by RELAT_1:def 19;
then rng id cTR=cTR & rng f=cTR by A4,ZFMISC_1:33;
then f=id TR by A3,A4,FUNCT_1:7;
hence contradiction by A2;
end;
then A5: n in Seg n by FINSEQ_1:3;
A6: dom f=cTR by FUNCT_2:52;
set A=AxialSymmetry(n,n),MA=Mx2Tran A;
A7: MA" is being_homeomorphism by TOPS_2:56;
A8: (MA is one-to-one) & rng MA=[#]TR by TOPS_2:def 5;
AutMt MA=A by Def6;
then A9: f*MA is base_rotation by A1,A2,A5,Th39;
f*MA*MA"=f*(MA*MA") by RELAT_1:36
.=f*id cTR by A8,TOPS_2:52
.=f by A6,RELAT_1:51;
hence thesis by A9,A7,TOPS_2:57;
end;
end;
end;
begin :: The Rotation Mapping a Given Point to Another Point
theorem
n = 1 & |.p.| = |.q.| implies
ex f st f is rotation & f.p=q &
(AutMt f = AxialSymmetry(n,n) or AutMt f = 1.(F_Real,n))
proof
set TR=TOP-REAL n;
assume that
A1: n=1 and
A2: |.p.|=|.q.|;
per cases;
suppose A3: p=q;
take I=id TR;
id TR=Mx2Tran 1.(F_Real,1) by A1,MATRTOP1:33;
hence thesis by A1,A3,Def6;
end;
suppose A4: p<>q;
A5: len p=1 by A1,CARD_1:def 7;
then A6: p=<*p.1*> by FINSEQ_1:40;
A7: 1 in Seg 1;
then reconsider f=Mx2Tran AxialSymmetry(1,1) as
homogeneous additive rotation Function of TR,TR by A1,Th27;
take f;
A8: (q.1)^2>=0 & (p.1)^2>=0 by XREAL_1:63;
reconsider pk =(p.1)^2, qk = (q.1)^2 as Real;
A9: |.p.|=sqrt Sum sqr<*p.1*> by A5,FINSEQ_1:40
.=sqrt Sum<*pk*> by RVSUM_1:55
.=sqrt((p.1)^2) by RVSUM_1:73;
A10: len q=1 by A1,CARD_1:def 7;
then A11: q=<*q.1*> by FINSEQ_1:40;
|.q.|=sqrt Sum sqr<*q.1*> by A10,FINSEQ_1:40
.=sqrt Sum<*qk*> by RVSUM_1:55
.=sqrt((q.1)^2) by RVSUM_1:73;
then A12: (q.1)^2=(p.1)^2 by A2,A8,A9,SQUARE_1:28;
len(f.p)=1 by A1,CARD_1:def 7;
then f.p=<*f.p.1*> by FINSEQ_1:40
.=<*-p.1*> by A1,A7,Th9
.=q by A4,A6,A11,A12,SQUARE_1:40;
hence thesis by A1,Def6;
end;
end;
theorem
n <> 1 & |.p.| = |.q.| implies ex f st f is base_rotation & f.p = q
proof
set TR=TOP-REAL n;
assume A1: n<>1;
assume A2: |.p.|=|.q.|;
per cases;
suppose A3: p=q;
take I=id TR;
thus thesis by A3;
end;
suppose A4: p<>q;
A5: n<>0
proof
assume A6: n=0;
then p=0.TR by EUCLID:77;
hence thesis by A4,A6;
end;
then A7: n>=1 by NAT_1:14;
defpred P[Nat] means
$1+1<=n implies ex f be base_rotation Function of TR,TR,X be set st
card X=$1 & X c=Seg n & for k st k in X holds f.p.k=q.k;
A8: Sum sqr q>=0 by RVSUM_1:86;
A9: card Seg n=n by FINSEQ_1:57;
A10: for m st P[m] holds P[m+1]
proof
let m such that
A11: P[m];
set m1=m+1;
assume A12: m1+1<=n;
then consider f be base_rotation Function of TR,TR,Xm be set such that
A13: card Xm=m and
A14: Xm c=Seg n and
A15: for k st k in Xm holds f.p.k=q.k by A11,NAT_1:13;
set fp=f.p,sfp=sqr fp,sq=sqr q;
A16: m1<n by A12,NAT_1:13;
per cases;
suppose ex k st k in (Seg n)\Xm & sfp.k>=sq.k;
then consider k such that
A17: k in (Seg n)\Xm and
A18: sfp.k>=sq.k;
A19: k in Seg n by A17,XBOOLE_0:def 5;
then A20: 1<=k by FINSEQ_1:1;
set Xmk=Xm\/{k};
A21: sfp.k=(fp.k)^2 & sq.k=(q.k)^2 by VALUED_1:11;
A22: {k}c=Seg n by A19,ZFMISC_1:31;
then A23: Xmk c=Seg n by A14,XBOOLE_1:8;
A24: not k in Xm by A17,XBOOLE_0:def 5;
then card Xmk=m1 by A13,A14,CARD_2:41;
then Xmk c<Seg n by A9,A16,A23,XBOOLE_0:def 8;
then consider z be object such that
A25: z in Seg n and
A26: not z in Xmk by XBOOLE_0:6;
reconsider z as Nat by A25;
A27: 1<=z by A25,FINSEQ_1:1;
(fp.z)^2>=0 by XREAL_1:63;
then A28: 0+(q.k)^2<=(fp.z)^2+(fp.k)^2 by A18,A21,XREAL_1:7;
A29: z<=n by A25,FINSEQ_1:1;
A30: k<=n by A19,FINSEQ_1:1;
not z in {k} by A26,XBOOLE_0:def 3;
then A31: z<>k by TARSKI:def 1;
now per cases by A31,XXREAL_0:1;
suppose A32: z<k;
then consider r such that
A33: (Mx2Tran Rotation(z,k,n,r)).fp.k=q.k by A27,A28,A30,Th25;
Mx2Tran Rotation(z,k,n,r) is{k,z}-support-yielding base_rotation
by A27,A30,A32,Th28,Th26;
hence ex g be base_rotation Function of TR,TR st g is
{k,z}-support-yielding & g.fp.k=q.k by A33;
end;
suppose A34: z>k;
then consider r such that
A35: (Mx2Tran Rotation(k,z,n,r)).fp.k=q.k by A20,A28,A29,Th24;
Mx2Tran Rotation(k,z,n,r) is{z,k}-support-yielding base_rotation
by A20,A29,A34,Th28,Th26;
hence ex g be base_rotation Function of TR,TR st g is
{k,z}-support-yielding & g.fp.k=q.k by A35;
end;
end;
then consider g be base_rotation Function of TR,TR such that
A36: g is{k,z}-support-yielding and
A37: g.fp.k=q.k;
take gf=g*f,Xmk;
thus card Xmk=m1 & Xmk c=Seg n
by A13,A14,A22,A24,CARD_2:41,XBOOLE_1:8;
let m;
A38: dom gf=the carrier of TR by FUNCT_2:52;
A39: dom g=the carrier of TR by FUNCT_2:52;
assume A40: m in Xmk;
then A41: m in Xm or m in {k} by XBOOLE_0:def 3;
per cases by A41,TARSKI:def 1;
suppose A42: m in Xm;
then m<>k by A17,XBOOLE_0:def 5;
then not m in {k,z} by A26,A40,TARSKI:def 2;
then g.(fp).m=fp.m by A36,A39;
hence gf.p.m=fp.m by A38,FUNCT_1:12
.=q.m by A15,A42;
end;
suppose m=k;
hence gf.p.m=q.m by A37,A38,FUNCT_1:12;
end;
end;
suppose A43: for k st k in (Seg n)\Xm holds sfp.k<sq.k;
A44: Sum sfp>=0 by RVSUM_1:86;
Sum sq>=0 & |.p.|=|.fp.| by Def4,RVSUM_1:86;
then A45: Sum sfp=Sum sq by A2,A44,SQUARE_1:28;
A46: len sfp=len fp by RVSUM_1:143;
A47: len sq=len q by RVSUM_1:143;
len fp=n & len q=n by CARD_1:def 7;
then reconsider sfp,sq as Element of n-tuples_on REAL
by A46,A47,FINSEQ_2:92;
m<n by A16,NAT_1:13;
then Xm<>Seg n by A13,FINSEQ_1:57;
then Xm c<Seg n by A14,XBOOLE_0:def 8;
then consider z be object such that
A48: z in Seg n and
A49: not z in Xm by XBOOLE_0:6;
reconsider z as Nat by A48;
A50: z in (Seg n)\Xm by A48,A49,XBOOLE_0:def 5;
for k st k in Seg n holds sfp.k<=sq.k
proof
let k such that
A51: k in Seg n;
per cases by A51,XBOOLE_0:def 5;
suppose k in (Seg n)\Xm;
hence thesis by A43;
end;
suppose k in Xm;
then fp.k=q.k by A15;
then sfp.k=(q.k)^2 by VALUED_1:11
.=sq.k by VALUED_1:11;
hence thesis;
end;
end;
then sfp.z>=sq.z by A45,A48,RVSUM_1:83;
hence thesis by A43,A50;
end;
end;
reconsider n1=n-1 as Nat by A5;
A52: n1+1=n;
A53: P[0]
proof
assume 0+1<=n;
take f=id TR,X={};
thus card X=0 & X c=Seg n;
let k;
assume k in X;
hence thesis;
end;
for m holds P[m] from NAT_1:sch 2(A53,A10);
then consider f be base_rotation Function of TR,TR,X be set such that
A54: card X=n1 & X c=Seg n and
A55: for k st k in X holds f.p.k=q.k by A52;
card((Seg n)\X)=n-n1 by A9,A54,CARD_2:44;
then consider z be object such that
A56: {z}=(Seg n)\X by CARD_2:42;
set fp=f.p;
Sum sqr fp>=0 & |.p.|=|.fp.| by Def4,RVSUM_1:86;
then A57: Sum sqr q=Sum sqr fp by A2,A8,SQUARE_1:28;
A58: z in {z} by TARSKI:def 1;
then A59: z in Seg n by A56,XBOOLE_0:def 5;
reconsider z as Nat by A56,A58;
set fpz=fp+*(z,q.z);
A60: len fp=n by CARD_1:def 7;
then A61: dom fp=Seg n by FINSEQ_1:def 3;
A62: for k st 1<=k & k<=n holds fpz.k=q.k
proof
let k;
assume 1<=k & k<=n;
then A63: k in Seg n;
per cases;
suppose k=z;
hence thesis by A61,A63,FUNCT_7:31;
end;
suppose A64: k<>z;
then not k in (Seg n)\X by A56,TARSKI:def 1;
then A65: k in X by A63,XBOOLE_0:def 5;
fpz.k=fp.k by A64,FUNCT_7:32;
hence thesis by A55,A65;
end;
end;
A66: len fpz=len fp & len q=n by CARD_1:def 7,FUNCT_7:97;
then A67: fpz=q by A60,A62;
then A68: Sum sqr q=(Sum sqr fp)-(fp.z)^2+(q.z)^2 by A59,A61,Th3;
per cases by A68,A57,SQUARE_1:40;
suppose fp.z=q.z;
then fp=q by A67,FUNCT_7:35;
hence thesis;
end;
suppose A69: fp.z=-q.z;
1<n by A1,A7,XXREAL_0:1;
then 1+1<=n by NAT_1:13;
then consider h be homogeneous additive Function of TR,TR such that
A70: h is base_rotation and
A71: h.fp=fp+*(z,-fp.z) by A59,Th34;
dom(h*f)=the carrier of TR by FUNCT_2:52;
then (h*f).p=fp+*(z,-fp.z) by A71,FUNCT_1:12
.=q by A60,A62,A66,A69;
hence thesis by A70;
end;
end;
end;