let n be Nat; for K being Field
for M being Matrix of n,K holds diagonal_of_Matrix M = diagonal_of_Matrix (M @)
let K be Field; for M being Matrix of n,K holds diagonal_of_Matrix M = diagonal_of_Matrix (M @)
let M be Matrix of n,K; diagonal_of_Matrix M = diagonal_of_Matrix (M @)
set DM = diagonal_of_Matrix M;
set DM9 = diagonal_of_Matrix (M @);
A1:
len (diagonal_of_Matrix M) = n
by MATRIX_3:def 10;
A2:
now for i being Nat st 1 <= i & i <= len (diagonal_of_Matrix M) holds
(diagonal_of_Matrix M) . i = (diagonal_of_Matrix (M @)) . ilet i be
Nat;
( 1 <= i & i <= len (diagonal_of_Matrix M) implies (diagonal_of_Matrix M) . i = (diagonal_of_Matrix (M @)) . i )assume that A3:
1
<= i
and A4:
i <= len (diagonal_of_Matrix M)
;
(diagonal_of_Matrix M) . i = (diagonal_of_Matrix (M @)) . iA5:
i in Seg n
by A1, A3, A4;
then A6:
(diagonal_of_Matrix (M @)) . i = (M @) * (
i,
i)
by MATRIX_3:def 10;
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A7:
[i,i] in Indices M
by A5, ZFMISC_1:87;
(diagonal_of_Matrix M) . i = M * (
i,
i)
by A5, MATRIX_3:def 10;
hence
(diagonal_of_Matrix M) . i = (diagonal_of_Matrix (M @)) . i
by A7, A6, MATRIX_0:def 6;
verum end;
len (diagonal_of_Matrix (M @)) = n
by MATRIX_3:def 10;
hence
diagonal_of_Matrix M = diagonal_of_Matrix (M @)
by A1, A2; verum