let K be Field; for n, i0 being Element of NAT
for A being Matrix of n,K st 1 <= i0 & i0 <= n & i0 <> 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( ( i = 1 & j = i0 implies A * (i,j) = 1. K ) & ( i = i0 & j = 1 implies A * (i,j) = 1. K ) & ( i = 1 & j = 1 implies A * (i,j) = 0. K ) & ( i = i0 & j = i0 implies A * (i,j) = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( 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 1 <= i0 & i0 <= n & i0 <> 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( ( i = 1 & j = i0 implies A * (i,j) = 1. K ) & ( i = i0 & j = 1 implies A * (i,j) = 1. K ) & ( i = 1 & j = 1 implies A * (i,j) = 0. K ) & ( i = i0 & j = i0 implies A * (i,j) = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( 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; ( 1 <= i0 & i0 <= n & i0 <> 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( ( i = 1 & j = i0 implies A * (i,j) = 1. K ) & ( i = i0 & j = 1 implies A * (i,j) = 1. K ) & ( i = 1 & j = 1 implies A * (i,j) = 0. K ) & ( i = i0 & j = i0 implies A * (i,j) = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) ) ) implies A = SwapDiagonal (K,n,i0) )
assume A1:
( 1 <= i0 & i0 <= n & i0 <> 1 )
; ( ex i, j being Nat st
( 1 <= i & i <= n & 1 <= j & j <= n & not ( ( i = 1 & j = i0 implies A * (i,j) = 1. K ) & ( i = i0 & j = 1 implies A * (i,j) = 1. K ) & ( i = 1 & j = 1 implies A * (i,j) = 0. K ) & ( i = i0 & j = i0 implies A * (i,j) = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( 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 = 1 & j = i0 implies A * (i,j) = 1. K ) & ( i = i0 & j = 1 implies A * (i,j) = 1. K ) & ( i = 1 & j = 1 implies A * (i,j) = 0. K ) & ( i = i0 & j = i0 implies A * (i,j) = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( 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 A4:
i in Seg n
by A3, ZFMISC_1:87;
then A5:
1
<= i
by FINSEQ_1:1;
A6:
(
i = i0 &
j = i0 implies
(SwapDiagonal (K,n,i0)) * (
i,
j)
= 0. K )
by A1, Th43;
width A = n
by MATRIX_0:24;
then A7:
j in Seg n
by A3, ZFMISC_1:87;
then A8:
1
<= j
by FINSEQ_1:1;
A9:
i <= n
by A4, FINSEQ_1:1;
then A10:
(
i = i0 &
j = i0 implies
A * (
i,
j)
= 0. K )
by A2, A5;
A11:
j <= n
by A7, FINSEQ_1:1;
then A12:
(
i = 1 &
j = i0 implies
A * (
i,
j)
= 1. K )
by A2, A9, A8;
A13:
(
i = 1 &
j = 1 implies
(SwapDiagonal (K,n,i0)) * (
i,
j)
= 0. K )
by A1, A9, Th43;
A14:
(
i = 1 &
j = 1 implies
A * (
i,
j)
= 0. K )
by A2, A9;
A15:
(
i = i0 &
j = 1 implies
A * (
i,
j)
= 1. K )
by A2, A5, A9, A11;
( ( ( not
i = 1 & not
i = i0 ) or ( not
j = 1 & not
j = i0 ) ) implies ( (
i = j implies
A * (
i,
j)
= 1. K ) & (
i <> j implies
A * (
i,
j)
= 0. K ) ) )
by A2, A5, A9, A8, A11;
hence
A * (
i,
j)
= (SwapDiagonal (K,n,i0)) * (
i,
j)
by A1, A5, A9, A8, A11, A12, A15, A14, A10, A13, A6, Th43;
verum
end;
hence
A = SwapDiagonal (K,n,i0)
by MATRIX_0:27; verum