let r be Real; :: thesis: for i, j, n being Nat st 1 <= i & i < j & j <= n holds

Det (Rotation (i,j,n,r)) = 1. F_Real

let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies Det (Rotation (i,j,n,r)) = 1. F_Real )

assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: Det (Rotation (i,j,n,r)) = 1. F_Real

then consider A being 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 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 ) ) ) ) by Lm3;

Det A <> 0. F_Real by A2;

then A is invertible by LAPLACE:34;

hence Det (Rotation (i,j,n,r)) = 1. F_Real by A1, A2, A3, Def3; :: thesis: verum

Det (Rotation (i,j,n,r)) = 1. F_Real

let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies Det (Rotation (i,j,n,r)) = 1. F_Real )

assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: Det (Rotation (i,j,n,r)) = 1. F_Real

then consider A being 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 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 ) ) ) ) by Lm3;

Det A <> 0. F_Real by A2;

then A is invertible by LAPLACE:34;

hence Det (Rotation (i,j,n,r)) = 1. F_Real by A1, A2, A3, Def3; :: thesis: verum