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 A2: 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

A3: Indices (SwapDiagonal K,n,i0) = [:(Seg n),(Seg n):] by MATRIX_1:25;
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 that
A4: 1 <= i and
A5: i <= n and
A6: 1 <= j and
A7: 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 ) ) ) )
A8: ( i in Seg n & j in Seg n ) by A4, A5, A6, A7, FINSEQ_1:3;

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 A9: ( i = 1 & j = i0 ) ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K
[j,i] in Indices (SwapDiagonal K,n,i0) by A8, A3, ZFMISC_1:106;
hence ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by MATRIX_1:def 7
.= 1. K by A2, A5, A6, A7, A9, Th43 ;
:: 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 A10: ( i = i0 & j = 1 ) ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 1. K
[j,i] in Indices (SwapDiagonal K,n,i0) by A8, A3, ZFMISC_1:106;
hence ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by MATRIX_1:def 7
.= 1. K by A2, A4, A5, A7, A10, Th43 ;
:: 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 A11: ( i = 1 & j = 1 ) ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K
[j,i] in Indices (SwapDiagonal K,n,i0) by A8, A3, ZFMISC_1:106;
hence ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by MATRIX_1:def 7
.= 0. K by A1, A2, A5, A11, Th43 ;
:: 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 A12: ( i = i0 & j = i0 ) ; :: thesis: ((SwapDiagonal K,n,i0) @ ) * i,j = 0. K
[j,i] in Indices (SwapDiagonal K,n,i0) by A8, A3, ZFMISC_1:106;
hence ((SwapDiagonal K,n,i0) @ ) * i,j = (SwapDiagonal K,n,i0) * j,i by MATRIX_1:def 7
.= 0. K by A2, A4, A5, A12, Th43 ;
:: thesis: verum

end;

hereby :: thesis: verum

assume A13: ( ( 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 ) )
A14: [j,i] in Indices (SwapDiagonal K,n,i0) by A8, A3, ZFMISC_1:106;

A15: now

assume A16: 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 A14, MATRIX_1:def 7
.= 1. K by A1, A2, A4, A5, A13, A16, Th43 ; :: thesis: verum

end;

now

assume A17: 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 A14, MATRIX_1:def 7
.= 0. K by A1, A2, A4, A5, A6, A7, A13, A17, Th43 ; :: 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 A15; :: thesis: verum

end;

end;

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

end;

suppose A18: 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

A19: Indices (SwapDiagonal K,n,i0) = [:(Seg n),(Seg n):] by MATRIX_1:25;
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 that
A20: ( 1 <= i & i <= n ) and
A21: ( 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 ) )
( i in Seg n & j in Seg n ) by A20, A21, FINSEQ_1:3;
then A22: [j,i] in Indices (SwapDiagonal K,n,i0) by A19, ZFMISC_1:106;

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

assume A23: 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 A22, MATRIX_1:def 7
.= 1. K by A18, A20, A23, Th44 ; :: thesis: verum

end;

hereby :: thesis: verum

assume A24: 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 A22, MATRIX_1:def 7
.= 0. K by A18, A20, A21, A24, Th45 ; :: thesis: verum

end;

end;

hence (SwapDiagonal K,n,i0) @ = SwapDiagonal K,n,i0 by A18, Th46; :: thesis: verum

end;

end;