let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
(((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n
let K be Field; :: thesis: for M being Matrix of n,K st Det M <> 0. K holds
(((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n
let M be Matrix of n,K; :: thesis: ( Det M <> 0. K implies (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n )
set D = Det M;
set D' = (Det M) " ;
set C = Matrix_of_Cofactor M;
set DC = ((Det M) " ) * ((Matrix_of_Cofactor M) @ );
set CM = (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M;
set ID = 1. K,n;
assume A1:
Det M <> 0. K
; :: thesis: (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n
now let i,
j be
Nat;
:: thesis: ( [i,j] in Indices ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) implies (1. K,n) * b1,b2 = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * b1,b2 )assume A2:
[i,j] in Indices ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M)
;
:: thesis: (1. K,n) * b1,b2 = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * b1,b2reconsider i' =
i,
j' =
j as
Element of
NAT by ORDINAL1:def 13;
Indices ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) = [:(Seg n),(Seg n):]
by MATRIX_1:25;
then A3:
(
i in Seg n &
j in Seg n &
width (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) = n &
len M = n &
len ((Matrix_of_Cofactor M) @ ) = n )
by A2, MATRIX_1:25, ZFMISC_1:106;
reconsider N =
n as
Element of
NAT by ORDINAL1:def 13;
reconsider COL =
Col M,
j,
L =
Line ((Matrix_of_Cofactor M) @ ),
i as
Element of
N -tuples_on the
carrier of
K by MATRIX_1:25;
( 1
<= i &
i <= len ((Matrix_of_Cofactor M) @ ) )
by A3, FINSEQ_1:3;
then
Line (((Det M) " ) * ((Matrix_of_Cofactor M) @ )),
i = ((Det M) " ) * L
by MATRIXR1:20;
then
mlt (Line (((Det M) " ) * ((Matrix_of_Cofactor M) @ )),i),
(Col M,j) = ((Det M) " ) * (mlt L,COL)
by FVSUM_1:83;
then A4:
(Line (((Det M) " ) * ((Matrix_of_Cofactor M) @ )),i) "*" (Col M,j) =
((Det M) " ) * ((Line ((Matrix_of_Cofactor M) @ ),i) "*" (Col M,j))
by FVSUM_1:92
.=
((Det M) " ) * (Det (RLine (M @ ),i',(Line (M @ ),j')))
by A3, Th32
;
then A5:
((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * i,
j = ((Det M) " ) * (Det (RLine (M @ ),i,(Line (M @ ),j)))
by A2, A3, MATRIX_3:def 4;
A6:
Indices ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) = Indices (1. K,n)
by MATRIX_1:27;
per cases
( i = j or i <> j )
;
suppose
i = j
;
:: thesis: (1. K,n) * b1,b2 = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * b1,b2then
(
RLine (M @ ),
i,
(Line (M @ ),j) = M @ &
(1. K,n) * i,
j = 1_ K &
((Det M) " ) * (Det M) = 1_ K &
Det M = Det (M @ ) )
by A1, A2, A6, MATRIX11:30, MATRIXR2:43, MATRIX_1:def 12, VECTSP_1:def 22;
hence
(1. K,n) * i,
j = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * i,
j
by A2, A3, A4, MATRIX_3:def 4;
:: thesis: verum end; suppose
i <> j
;
:: thesis: (1. K,n) * b1,b2 = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * b1,b2then
(
Det (RLine (M @ ),i',(Line (M @ ),j')) = 0. K &
(1. K,n) * i,
j = 0. K )
by A2, A3, A6, MATRIX11:51, MATRIX_1:def 12;
hence
(1. K,n) * i,
j = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * i,
j
by A5, VECTSP_1:36;
:: thesis: verum end; end;
hence
(((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n
by MATRIX_1:28; :: thesis: verum