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_0:24;
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:1;

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:87;
hence ((SwapDiagonal (K,n,i0)) @) * (i,j) = (SwapDiagonal (K,n,i0)) * (j,i) by MATRIX_0:def 6
.= 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:87;
hence ((SwapDiagonal (K,n,i0)) @) * (i,j) = (SwapDiagonal (K,n,i0)) * (j,i) by MATRIX_0:def 6
.= 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:87;
hence ((SwapDiagonal (K,n,i0)) @) * (i,j) = (SwapDiagonal (K,n,i0)) * (j,i) by MATRIX_0:def 6
.= 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:87;
hence ((SwapDiagonal (K,n,i0)) @) * (i,j) = (SwapDiagonal (K,n,i0)) * (j,i) by MATRIX_0:def 6
.= 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:87;

A15: now :: thesis: ( i = j implies ((SwapDiagonal (K,n,i0)) @) * (i,j) = 1. K )

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

end;

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

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_0:def 6
.= 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_0:24;
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:1;
then A22: [j,i] in Indices (SwapDiagonal (K,n,i0)) by A19, ZFMISC_1:87;

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_0:def 6
.= 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_0:def 6
.= 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;