let n be Element of NAT ; :: thesis: for K being Field
for i0 being Element of NAT st 1 <= i0 & i0 <= n holds
(SwapDiagonal K,n,i0) @ = SwapDiagonal K,n,i0
let K be Field; :: thesis: for i0 being Element of NAT st 1 <= i0 & i0 <= n holds
(SwapDiagonal K,n,i0) @ = SwapDiagonal K,n,i0
let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 <= n implies (SwapDiagonal K,n,i0) @ = SwapDiagonal K,n,i0 )
assume A1: ( 1 <= i0 & i0 <= n ) ; :: thesis: (SwapDiagonal K,n,i0) @ = SwapDiagonal K,n,i0

per cases ( i0 <> 1 or i0 = 1 ) ;

suppose S: i0 <> 1 ; :: thesis: (SwapDiagonal K,n,i0) @ = SwapDiagonal K,n,i0

for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( ( i = 1 & j = i0 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i = i0 & j = 1 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i = 1 & j = 1 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( i = i0 & j = i0 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) ) ) )

proof

let i, j be Nat; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies ( ( i = 1 & j = i0 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i = i0 & j = 1 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i = 1 & j = 1 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( i = i0 & j = i0 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) ) ) ) )
assume B1: ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: ( ( i = 1 & j = i0 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i = i0 & j = 1 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i = 1 & j = 1 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( i = i0 & j = i0 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) ) ) )
B2: ( i in Seg n & j in Seg n ) by B1, FINSEQ_1:3;
A5: ( len (SwapDiagonal K,n,i0) = n & width (SwapDiagonal K,n,i0) = n & Indices (SwapDiagonal K,n,i0) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;

hereby :: thesis: ( ( i = i0 & j = 1 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i = 1 & j = 1 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( i = i0 & j = i0 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) ) ) )

assume C0: ( i = 1 & j = i0 ) ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K
[j,i] in Indices (SwapDiagonal K,n,i0) by B2, A5, ZFMISC_1:106;
hence ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by MATRIX_1:def 7
.= 1. K by S, C0, XA, B1 ;
:: thesis: verum

end;

hereby :: thesis: ( ( i = 1 & j = 1 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( i = i0 & j = i0 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) ) ) )

assume C0: ( i = i0 & j = 1 ) ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K
[j,i] in Indices (SwapDiagonal K,n,i0) by B2, A5, ZFMISC_1:106;
hence ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by MATRIX_1:def 7
.= 1. K by S, C0, XA, B1 ;
:: thesis: verum

end;

hereby :: thesis: ( ( i = i0 & j = i0 implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) ) ) )

assume C0: ( i = 1 & j = 1 ) ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K
[j,i] in Indices (SwapDiagonal K,n,i0) by B2, A5, ZFMISC_1:106;
hence ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by MATRIX_1:def 7
.= 0. K by S, C0, XA, A1, B1 ;
:: thesis: verum

end;

hereby :: thesis: ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) ) )

assume C0: ( i = i0 & j = i0 ) ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K
[j,i] in Indices (SwapDiagonal K,n,i0) by B2, A5, ZFMISC_1:106;
hence ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by MATRIX_1:def 7
.= 0. K by S, C0, XA, B1 ;
:: thesis: verum

end;

hereby :: thesis: verum

assume C0: ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) ; :: thesis: ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) )
C1: [j,i] in Indices (SwapDiagonal K,n,i0) by B2, A5, ZFMISC_1:106;

C2: now

assume D0: i = j ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K
thus ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by C1, MATRIX_1:def 7
.= 1. K by S, C0, XA, A1, B1, D0 ; :: thesis: verum

end;

now

assume D0: i <> j ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K
thus ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by C1, MATRIX_1:def 7
.= 0. K by S, C0, XA, A1, B1, D0 ; :: thesis: verum

end;

hence ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) ) by C2; :: thesis: verum

end;

end;

hence (SwapDiagonal K,n,i0) @ = SwapDiagonal K,n,i0 by AA400X, A1, S; :: thesis: verum

end;

suppose S: i0 = 1 ; :: thesis: (SwapDiagonal K,n,i0) @ = SwapDiagonal K,n,i0

for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) )

proof

let i, j be Nat; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) ) )
assume B1: ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: ( ( i = j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K ) & ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K ) )
B2: ( i in Seg n & j in Seg n ) by B1, FINSEQ_1:3;
A5: ( len (SwapDiagonal K,n,i0) = n & width (SwapDiagonal K,n,i0) = n & Indices (SwapDiagonal K,n,i0) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
C1: [j,i] in Indices (SwapDiagonal K,n,i0) by B2, A5, ZFMISC_1:106;

hereby :: thesis: ( i <> j implies ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K )

assume C0: i = j ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K
thus ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by C1, MATRIX_1:def 7
.= 1. K by S, C0, XB, B1 ; :: thesis: verum

end;

hereby :: thesis: verum

assume C0: i <> j ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K
thus ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by C1, MATRIX_1:def 7
.= 0. K by S, C0, XC, B1 ; :: thesis: verum

end;

end;

hence (SwapDiagonal K,n,i0) @ = SwapDiagonal K,n,i0 by AA4000, A1, S; :: thesis: verum

end;

end;