let n be Element of NAT ; 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; 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 ; ( 1 <= i0 & i0 <= n implies (SwapDiagonal (K,n,i0)) @ = SwapDiagonal (K,n,i0) )
assume A1:
( 1 <= i0 & i0 <= n )
; (SwapDiagonal (K,n,i0)) @ = SwapDiagonal (K,n,i0)
per cases
( i0 <> 1 or i0 = 1 )
;
suppose A2:
i0 <> 1
;
(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;
( 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
;
( ( 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 ( ( 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 )
;
((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
;
verum
end;
hereby ( ( 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 )
;
((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
;
verum
end;
hereby ( ( 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 )
;
((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
;
verum
end;
hereby ( ( ( 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 )
;
((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
;
verum
end;
hereby verum
assume A13:
( ( not
i = 1 & not
i = i0 ) or ( not
j = 1 & not
j = i0 ) )
;
( ( 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 ( i = j implies ((SwapDiagonal (K,n,i0)) @) * (i,j) = 1. K )assume A16:
i = j
;
((SwapDiagonal (K,n,i0)) @) * (i,j) = 1. Kthus ((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
;
verum end; now ( i <> j implies ((SwapDiagonal (K,n,i0)) @) * (i,j) = 0. K )assume A17:
i <> j
;
((SwapDiagonal (K,n,i0)) @) * (i,j) = 0. Kthus ((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
;
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;
verum
end;
end; hence
(SwapDiagonal (K,n,i0)) @ = SwapDiagonal (
K,
n,
i0)
by A1, A2, Th47;
verum end; suppose A18:
i0 = 1
;
(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;
( 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 )
;
( ( 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 ( i <> j implies ((SwapDiagonal (K,n,i0)) @) * (i,j) = 0. K )
assume A23:
i = j
;
((SwapDiagonal (K,n,i0)) @) * (i,j) = 1. Kthus ((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
;
verum
end;
hereby verum
assume A24:
i <> j
;
((SwapDiagonal (K,n,i0)) @) * (i,j) = 0. Kthus ((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
;
verum
end;
end; hence
(SwapDiagonal (K,n,i0)) @ = SwapDiagonal (
K,
n,
i0)
by A18, Th46;
verum end; end;