let K be Field; for n, i0 being Element of NAT
for A being Matrix of n,K st i0 = 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) holds
A = SwapDiagonal (K,n,i0)
let n, i0 be Element of NAT ; for A being Matrix of n,K st i0 = 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) holds
A = SwapDiagonal (K,n,i0)
let A be Matrix of n,K; ( i0 = 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) implies A = SwapDiagonal (K,n,i0) )
assume A1:
i0 = 1
; ( ex i, j being Nat st
( 1 <= i & i <= n & 1 <= j & j <= n & not ( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) or A = SwapDiagonal (K,n,i0) )
assume A2:
for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) )
; A = SwapDiagonal (K,n,i0)
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = (SwapDiagonal (K,n,i0)) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices A implies A * (i,j) = (SwapDiagonal (K,n,i0)) * (i,j) )
assume A3:
[i,j] in Indices A
;
A * (i,j) = (SwapDiagonal (K,n,i0)) * (i,j)
Indices A = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
i in Seg n
by A3, ZFMISC_1:87;
then A4:
( 1
<= i &
i <= n )
by FINSEQ_1:1;
then A5:
(
i = j implies
A * (
i,
j)
= 1. K )
by A2;
width A = n
by MATRIX_0:24;
then
j in Seg n
by A3, ZFMISC_1:87;
then A6:
( 1
<= j &
j <= n )
by FINSEQ_1:1;
then
(
i <> j implies
A * (
i,
j)
= 0. K )
by A2, A4;
hence
A * (
i,
j)
= (SwapDiagonal (K,n,i0)) * (
i,
j)
by A1, A4, A6, A5, Th44, Th45;
verum
end;
hence
A = SwapDiagonal (K,n,i0)
by MATRIX_0:27; verum