let V be free finite-rank Z_Module; for b1, b2 being OrdBasis of V
for M being Matrix of rank V,F_Real holds
( not M = AutMt ((id V),b1,b2) or ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )
let b1, b2 be OrdBasis of V; for M being Matrix of rank V,F_Real holds
( not M = AutMt ((id V),b1,b2) or ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )
let M be Matrix of rank V,F_Real; ( not M = AutMt ((id V),b1,b2) or ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )
assume AS1:
M = AutMt ((id V),b1,b2)
; ( ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )
set n = rank V;
per cases
( rank V = 0 or rank V > 0 )
;
suppose AS2:
rank V > 0
;
( ( Det M = 1 & Det (M @) = 1 ) or ( Det M = - 1 & Det (M @) = - 1 ) )B0:
len b1 = rank V
by ZMATRLIN:49;
B1:
len (AutMt ((id V),b2,b1)) =
len b2
by ZMATRLIN:def 8
.=
rank V
by ZMATRLIN:49
;
len b2 = rank V
by ZMATRLIN:49;
then
width (AutMt ((id V),b2,b1)) = len b1
by AS2, ZMATRLIN:34;
then reconsider M2 =
AutMt (
(id V),
b2,
b1) as
Matrix of
rank V,
INT.Ring by AS2, B0, B1, MATRIX_0:20;
(
AutMt (
(id V),
b1,
b2) is
Matrix of
rank V,
INT.Ring &
AutMt (
(id V),
b2,
b1) is
Matrix of
rank V,
INT.Ring )
by ZMATRLIN:50;
then A1:
M * (inttorealM M2) =
(AutMt ((id V),b1,b2)) * (AutMt ((id V),b2,b1))
by AS1, AS2, MLT1
.=
1. (
INT.Ring,
(rank V))
by ZMATRLIN:54, AS2
.=
1. (
F_Real,
(rank V))
by MLT2
;
then reconsider MM2 =
M * (inttorealM M2) as
Matrix of
rank V,
F_Real ;
A2:
(Det M) * (Det (inttorealM M2)) =
Det MM2
by MATRIXR2:45
.=
1_ F_Real
by AS2, A1, NAT_1:14, MATRIX_7:16
.=
1
;
reconsider i =
Det M as
Integer by AS1, ZMATRLIN:51, INT_1:def 2;
Det (inttorealM M2) in INT
by ZMATRLIN:51;
then reconsider j =
Det (inttorealM M2) as
Integer ;
i * j = 1
by A2;
then
(
Det M = 1 or
Det M = - 1 )
by INT_1:9;
hence
( (
Det M = 1 &
Det (M @) = 1 ) or (
Det M = - 1 &
Det (M @) = - 1 ) )
by AS2, MATRIX_7:37, NAT_1:14;
verum end;