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