let r be Real; :: thesis: for n being Nat
for a, b being 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
let n be Nat; :: thesis: for a, b being 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
let a, b be Element of F_Real; :: thesis: ( a = cos r & b = sin r implies Det (block_diagonal (<*((a,b) ][ ((- b),a)),(1. (F_Real,n))*>,(0. F_Real))) = 1. F_Real )
set A = (a,b) ][ ((- b),a);
set ONE = 1. (F_Real,n);
set B = block_diagonal (<*((a,b) ][ ((- b),a)),(1. (F_Real,n))*>,(0. F_Real));
A1: ( n = 0 or n >= 1 ) by NAT_1:14;
A2: ( Det (1. (F_Real,n)) = 1_ F_Real or Det (1. (F_Real,n)) = 1. F_Real ) by A1, MATRIXR2:41, MATRIX_7:16;
assume ( a = cos r & b = sin r ) ; :: thesis: Det (block_diagonal (<*((a,b) ][ ((- b),a)),(1. (F_Real,n))*>,(0. F_Real))) = 1. F_Real
then A3: ((cos r) * (cos r)) + ((sin r) * (sin r)) = (a * a) - (b * (- b))
.= Det ((a,b) ][ ((- b),a)) by MATRIX_9:13 ;
A4: ( cos r = cos . r & sin r = sin . r ) by SIN_COS:def 17, SIN_COS:def 19;
thus Det (block_diagonal (<*((a,b) ][ ((- b),a)),(1. (F_Real,n))*>,(0. F_Real))) = (Det ((a,b) ][ ((- b),a))) * (Det (1. (F_Real,n))) by MATRIXJ1:52
.= 1. F_Real by A2, A3, A4, SIN_COS:28 ; :: thesis: verum