let n be Nat; for K being Field
for M being Matrix of n,K
for I being Element of Permutations n st I = idseq n holds
diagonal_of_Matrix M = Path_matrix (I,M)
let K be Field; for M being Matrix of n,K
for I being Element of Permutations n st I = idseq n holds
diagonal_of_Matrix M = Path_matrix (I,M)
let M be Matrix of n,K; for I being Element of Permutations n st I = idseq n holds
diagonal_of_Matrix M = Path_matrix (I,M)
let I be Element of Permutations n; ( I = idseq n implies diagonal_of_Matrix M = Path_matrix (I,M) )
assume A1:
I = idseq n
; diagonal_of_Matrix M = Path_matrix (I,M)
set P = Path_matrix (I,M);
set D = diagonal_of_Matrix M;
A2:
len (Path_matrix (I,M)) = n
by MATRIX_3:def 7;
A3:
now for i being Nat st 1 <= i & i <= n holds
(Path_matrix (I,M)) . i = (diagonal_of_Matrix M) . ilet i be
Nat;
( 1 <= i & i <= n implies (Path_matrix (I,M)) . i = (diagonal_of_Matrix M) . i )assume that A4:
1
<= i
and A5:
i <= n
;
(Path_matrix (I,M)) . i = (diagonal_of_Matrix M) . iA6:
i in Seg n
by A4, A5;
then A7:
I . i = i
by A1, FINSEQ_2:49;
i in dom (Path_matrix (I,M))
by A2, A6, FINSEQ_1:def 3;
then
(Path_matrix (I,M)) . i = M * (
i,
i)
by A7, MATRIX_3:def 7;
hence
(Path_matrix (I,M)) . i = (diagonal_of_Matrix M) . i
by A6, MATRIX_3:def 10;
verum end;
len (diagonal_of_Matrix M) = n
by MATRIX_3:def 10;
hence
diagonal_of_Matrix M = Path_matrix (I,M)
by A2, A3; verum