let n be Nat; for MR being Matrix of n,REAL holds
( MR is diagonal iff for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i )
let MR be Matrix of n,REAL; ( MR is diagonal iff for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i )
A1:
width MR = n
by MATRIX_0:24;
len MR = n
by MATRIX_0:24;
then A2:
dom MR = Seg (width MR)
by A1, FINSEQ_1:def 3;
hereby ( ( for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i ) implies MR is diagonal )
assume A3:
MR is
diagonal
;
for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in inow for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in ilet i be
Nat;
( i in dom MR implies Line (MR,i) has_onlyone_value_in i )assume A4:
i in dom MR
;
Line (MR,i) has_onlyone_value_in iA5:
len (Line (MR,i)) = width MR
by MATRIX_0:def 7;
A6:
now for j being Nat st j in dom (Line (MR,i)) & j <> i holds
(Line (MR,i)) . j = 0 let j be
Nat;
( j in dom (Line (MR,i)) & j <> i implies (Line (MR,i)) . j = 0 )assume that A7:
j in dom (Line (MR,i))
and A8:
j <> i
;
(Line (MR,i)) . j = 0
j in dom (MR . i)
by A4, A7, MATRIX_0:60;
then A9:
[i,j] in Indices MR
by A4, MATRPROB:13;
j in Seg (width MR)
by A5, A7, FINSEQ_1:def 3;
hence (Line (MR,i)) . j =
MR * (
i,
j)
by MATRIX_0:def 7
.=
0
by A3, A8, A9
;
verum end;
i in dom (Line (MR,i))
by A2, A4, A5, FINSEQ_1:def 3;
hence
Line (
MR,
i)
has_onlyone_value_in i
by A6;
verum end; hence
for
i being
Nat st
i in dom MR holds
Line (
MR,
i)
has_onlyone_value_in i
;
verum
end;
assume A10:
for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i
; MR is diagonal
for i, j being Nat st [i,j] in Indices MR & MR * (i,j) <> 0 holds
i = j
proof
let i,
j be
Nat;
( [i,j] in Indices MR & MR * (i,j) <> 0 implies i = j )
assume that A11:
[i,j] in Indices MR
and A12:
MR * (
i,
j)
<> 0
;
i = j
A13:
i in dom MR
by A11, MATRPROB:13;
then A14:
Line (
MR,
i)
has_onlyone_value_in i
by A10;
j in dom (MR . i)
by A11, MATRPROB:13;
then A15:
j in dom (Line (MR,i))
by A13, MATRIX_0:60;
assume A16:
i <> j
;
contradiction
len (Line (MR,i)) = width MR
by MATRIX_0:def 7;
then
dom (Line (MR,i)) = Seg (width MR)
by FINSEQ_1:def 3;
then MR * (
i,
j) =
(Line (MR,i)) . j
by A15, MATRIX_0:def 7
.=
0
by A16, A15, A14
;
hence
contradiction
by A12;
verum
end;
hence
MR is diagonal
; verum