let r be Real; :: thesis: for i, j, n being Nat st 1 <= i & i < j & j <= n holds
ex A being 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 being Nat 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 ) ) ) )
let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies ex A being 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 being Nat 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 ) ) ) ) )
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 ; :: thesis: ex A being 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 being Nat 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 ) ) ) )
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 being Permutation of (Seg n) such that
A9: P . 1 = i and
A10: P . 2 = j and
for k being Nat 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 = Seg n by FUNCT_2:52;
then A11: rng (p ") = Seg n by FUNCT_1:33;
rng P = Seg n by FUNCT_2:def 3;
then dom (p ") = Seg n by FUNCT_1:33;
then reconsider P1 = p " as one-to-one Function of (Seg n),(Seg n) by A11, FUNCT_2:1;
P1 is onto by A11, FUNCT_2:def 3;
then reconsider P1 = P1 as Permutation of (Seg n) ;
A12: dom P = Seg n by FUNCT_2:52;
1 <= n by A6, A7, XXREAL_0:2;
then A13: 1 in Seg n ;
then A14: P1 . (P . 1) = 1 by A12, FUNCT_1:34;
set A = (c,s) ][ ((- s),c);
set ONE = 1. (F_Real,n2);
set ao = <*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*>;
set B = block_diagonal (<*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*>,(0. F_Real));
A15: len ((c,s) ][ ((- s),c)) = 2 by MATRIX_0:25;
then Len <*((c,s) ][ ((- s),c))*> = <*2*> by MATRIXJ1:15;
then A16: Sum (Len <*((c,s) ][ ((- s),c))*>) = 2 by RVSUM_1:73;
len (1. (F_Real,n2)) = n2 by MATRIX_0:25;
then A17: Sum (Len <*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*>) = 2 + n2 by A15, MATRIXJ1:16;
then reconsider B = block_diagonal (<*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*>,(0. F_Real)) as Matrix of n,F_Real ;
A18: Indices B = [:(Seg n),(Seg n):] by MATRIX_0:24;
2 <= n by A6, A8, XXREAL_0:2;
then A19: 2 in Seg n ;
then A20: P1 . (P . 2) = 2 by A12, FUNCT_1:34;
set pBp = (((B * P1) @) * P1) @ ;
A21: dom P1 = Seg n by FUNCT_2:52;
i < n by A5, A6, XXREAL_0:2;
then A22: i in Seg n by A4;
then [i,i] in Indices B by A18, ZFMISC_1:87;
then A23: ((((B * P1) @) * P1) @) * (i,i) = B * (1,1) by A9, A14, Th1;
take (((B * P1) @) * P1) @ ; :: thesis: ( Det ((((B * P1) @) * P1) @) = 1. F_Real & ((((B * P1) @) * P1) @) * (i,i) = cos r & ((((B * P1) @) * P1) @) * (j,j) = cos r & ((((B * P1) @) * P1) @) * (i,j) = sin r & ((((B * P1) @) * P1) @) * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices ((((B * P1) @) * P1) @) holds
( ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) ) ) )
A24: Indices ((((B * P1) @) * P1) @) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A25: Det B = 1. F_Real by A17, Th12;
A26: block_diagonal (<*((c,s) ][ ((- s),c))*>,(0. F_Real)) = (c,s) ][ ((- s),c) by MATRIXJ1:34;
width ((c,s) ][ ((- s),c)) = 2 by MATRIX_0:24;
then Width <*((c,s) ][ ((- s),c))*> = <*2*> by MATRIXJ1:19;
then A27: Sum (Width <*((c,s) ][ ((- s),c))*>) = 2 by RVSUM_1:73;
1 < j by A4, A5, XXREAL_0:2;
then A28: j in Seg n by A6;
then [j,j] in Indices B by A18, ZFMISC_1:87;
then A29: ((((B * P1) @) * P1) @) * (j,j) = B * (2,2) by A10, A20, Th1;
A30: block_diagonal (<*(1. (F_Real,n2))*>,(0. F_Real)) = 1. (F_Real,n2) by MATRIXJ1:34;
[1,1] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A31: B * (1,1) = ((c,s) ][ ((- s),c)) * (1,1) by A26, A30, MATRIXJ1:26;
[2,1] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A32: B * (2,1) = ((c,s) ][ ((- s),c)) * (2,1) by A26, A30, MATRIXJ1:26;
[1,2] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A33: B * (1,2) = ((c,s) ][ ((- s),c)) * (1,2) by A26, A30, MATRIXJ1:26;
[2,2] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A34: B * (2,2) = ((c,s) ][ ((- s),c)) * (2,2) by A26, A30, MATRIXJ1:26;
A35: <*((c,s) ][ ((- s),c))*> ^ <*(1. (F_Real,n2))*> = <*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*> ;
[i,j] in Indices B by A18, A22, A28, ZFMISC_1:87;
then A36: ((((B * P1) @) * P1) @) * (i,j) = B * (1,2) by A9, A10, A14, A20, Th1;
[j,i] in Indices B by A18, A22, A28, ZFMISC_1:87;
then ((((B * P1) @) * P1) @) * (j,i) = B * (2,1) by A9, A10, A14, A20, Th1;
hence ( Det ((((B * P1) @) * P1) @) = 1. F_Real & ((((B * P1) @) * P1) @) * (i,i) = cos r & ((((B * P1) @) * P1) @) * (j,j) = cos r & ((((B * P1) @) * P1) @) * (i,j) = sin r & ((((B * P1) @) * P1) @) * (j,i) = - (sin r) ) by A23, A25, A29, A34, A33, A32, A31, A36, Th1, MATRIX_0:50; :: thesis: for k, m being Nat st [k,m] in Indices ((((B * P1) @) * P1) @) holds
( ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) )
let k, m be Nat; :: thesis: ( [k,m] in Indices ((((B * P1) @) * P1) @) implies ( ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) ) )
assume A37: [k,m] in Indices ((((B * P1) @) * P1) @) ; :: thesis: ( ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) )
A38: k in Seg n by A24, A37, ZFMISC_1:87;
set Pk = P1 . k;
set Pm = P1 . m;
A39: rng P1 = Seg n by FUNCT_2:def 3;
then A40: P1 . k in Seg n by A21, A38, FUNCT_1:def 3;
then A41: P1 . k >= 1 by FINSEQ_1:1;
A42: m in Seg n by A24, A37, ZFMISC_1:87;
then A43: P1 . m in Seg n by A21, A39, FUNCT_1:def 3;
then A44: [(P1 . k),(P1 . m)] in [:(Seg n),(Seg n):] by A40, ZFMISC_1:87;
A45: ((((B * P1) @) * P1) @) * (k,m) = B * ((P1 . k),(P1 . m)) by A18, A24, A37, Th1;
thus ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) :: thesis: ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) A50: P1 . m >= 1 by A43, FINSEQ_1:1;
thus ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) :: thesis: verum