let n be Nat; 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; 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; ( Det M <> 0. K implies (((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n) )
set D = Det M;
set D9 = (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
; (((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n)
now for i, j being Nat st [i,j] in Indices ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) holds
(1. (K,n)) * (i,j) = ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (i,j)A2:
Indices ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) = Indices (1. (K,n))
by MATRIX_0:26;
reconsider N =
n as
Element of
NAT by ORDINAL1:def 12;
let i,
j be
Nat;
( [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 A3:
[i,j] in Indices ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M)
;
(1. (K,n)) * (b1,b2) = ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (b1,b2)reconsider COL =
Col (
M,
j),
L =
Line (
((Matrix_of_Cofactor M) @),
i) as
Element of
N -tuples_on the
carrier of
K by MATRIX_0:24;
reconsider i9 =
i,
j9 =
j as
Element of
NAT by ORDINAL1:def 12;
A4:
len M = n
by MATRIX_0:24;
A5:
Indices ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A6:
i in Seg n
by A3, ZFMISC_1:87;
then A7:
1
<= i
by FINSEQ_1:1;
A8:
j in Seg n
by A3, A5, ZFMISC_1:87;
len ((Matrix_of_Cofactor M) @) = n
by MATRIX_0:24;
then
i <= len ((Matrix_of_Cofactor M) @)
by A6, FINSEQ_1:1;
then
Line (
(((Det M) ") * ((Matrix_of_Cofactor M) @)),
i)
= ((Det M) ") * L
by A7, MATRIXR1:20;
then
mlt (
(Line ((((Det M) ") * ((Matrix_of_Cofactor M) @)),i)),
(Col (M,j)))
= ((Det M) ") * (mlt (L,COL))
by FVSUM_1:69;
then A9:
(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:73
.=
((Det M) ") * (Det (RLine ((M @),i9,(Line ((M @),j9)))))
by A6, A8, Th32
;
A10:
width (((Det M) ") * ((Matrix_of_Cofactor M) @)) = n
by MATRIX_0:24;
then A11:
((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (
i,
j)
= ((Det M) ") * (Det (RLine ((M @),i,(Line ((M @),j)))))
by A3, A4, A9, MATRIX_3:def 4;
per cases
( i = j or i <> j )
;
suppose A12:
i = j
;
(1. (K,n)) * (b1,b2) = ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (b1,b2)then A13:
RLine (
(M @),
i,
(Line ((M @),j)))
= M @
by MATRIX11:30;
A14:
Det M = Det (M @)
by MATRIXR2:43;
A15:
((Det M) ") * (Det M) = 1_ K
by A1, VECTSP_1:def 10;
(1. (K,n)) * (
i,
j)
= 1_ K
by A3, A2, A12, MATRIX_1:def 3;
hence
(1. (K,n)) * (
i,
j)
= ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (
i,
j)
by A3, A10, A4, A9, A13, A15, A14, MATRIX_3:def 4;
verum end; suppose A16:
i <> j
;
(1. (K,n)) * (b1,b2) = ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (b1,b2)then A17:
(1. (K,n)) * (
i,
j)
= 0. K
by A3, A2, MATRIX_1:def 3;
Det (RLine ((M @),i9,(Line ((M @),j9)))) = 0. K
by A6, A8, A16, MATRIX11:51;
hence
(1. (K,n)) * (
i,
j)
= ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (
i,
j)
by A11, A17;
verum end; end;
hence
(((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n)
by MATRIX_0:27; verum