let K be Field; for n being Element of NAT
for i0 being Nat
for A being Matrix of n,K st 1 <= i0 & i0 <= n & A = SwapDiagonal (K,n,i0) holds
for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i0 <> 1 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 ) ) ) )
let n be Element of NAT ; for i0 being Nat
for A being Matrix of n,K st 1 <= i0 & i0 <= n & A = SwapDiagonal (K,n,i0) holds
for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i0 <> 1 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 ) ) ) )
let i0 be Nat; for A being Matrix of n,K st 1 <= i0 & i0 <= n & A = SwapDiagonal (K,n,i0) holds
for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i0 <> 1 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 ) ) ) )
let A be Matrix of n,K; ( 1 <= i0 & i0 <= n & A = SwapDiagonal (K,n,i0) implies for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i0 <> 1 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 ) ) ) ) )
assume A1:
( 1 <= i0 & i0 <= n )
; ( not A = SwapDiagonal (K,n,i0) or for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i0 <> 1 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 ) ) ) ) )
assume A2:
A = SwapDiagonal (K,n,i0)
; for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i0 <> 1 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 ) ) ) )
let i, j be Nat; ( 1 <= i & i <= n & 1 <= j & j <= n & i0 <> 1 implies ( ( 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 ) ) ) ) )
assume that
A3:
1 <= i
and
A4:
i <= n
and
A5:
1 <= j
and
A6:
j <= n
; ( not i0 <> 1 or ( ( 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 ) ) ) ) )
A7:
[i,j] in Indices A
by A3, A4, A5, A6, MATRIX_0:31;
assume A8:
i0 <> 1
; ( ( 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 ) ) ) )
thus
( 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 ) ) ) )proof
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
assume that A9:
i = 1
and A10:
j = i0
;
A * (i,j) = 1. K
reconsider qq =
f /. i0 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
i0 <= len f
by A6, A10, MATRIX_0:def 2;
then f /. i0 =
f . i0
by A5, A10, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,
i0)
by A5, A6, A10, Th26
;
then A11:
qq . j = 1. K
by A5, A6, A10, Th24;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
A12:
len f = n
by MATRIX_0:def 2;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
len (<*(f /. i0)*> ^ h) =
(len <*(f /. i0)*>) + (len h)
by FINSEQ_1:22
.=
1
+ (len h)
by FINSEQ_1:39
;
then A13:
1
<= len (<*(f /. i0)*> ^ h)
by NAT_1:11;
A14:
1
= len <*(f /. i0)*>
by FINSEQ_1:39;
1
< i0
by A5, A8, A10, XXREAL_0:1;
then A . i =
(((<*(f /. i0)*> ^ h) ^ <*(f /. 1)*>) ^ (f /^ i0)) . i
by A2, A6, A10, A12, FINSEQ_7:28
.=
((<*(f /. i0)*> ^ h) ^ (<*(f /. 1)*> ^ (f /^ i0))) . i
by FINSEQ_1:32
.=
(<*(f /. i0)*> ^ h) . 1
by A9, A13, FINSEQ_1:64
.=
<*(f /. i0)*> . 1
by A14, FINSEQ_1:64
.=
f /. i0
by FINSEQ_1:def 8
;
hence
A * (
i,
j)
= 1. K
by A7, A11, MATRIX_0:def 5;
verum
end;
A15:
len A = n
by MATRIX_0:24;
A16:
1 <= n
by A3, A4, XXREAL_0:2;
thus
( 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 ) ) ) )proof
reconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
assume that A17:
i = i0
and A18:
j = 1
;
A * (i,j) = 1. K
reconsider qq =
f /. 1 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
A19:
len f = n
by MATRIX_0:def 2;
then f /. 1 =
f . 1
by A16, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,1)
by A16, Th26
;
then A20:
qq . j = 1. K
by A6, A18, Th24;
A . i =
A /. i
by A15, A3, A4, FINSEQ_4:15
.=
f /. 1
by A2, A3, A4, A6, A17, A18, A19, FINSEQ_7:31
;
hence
A * (
i,
j)
= 1. K
by A7, A20, MATRIX_0:def 5;
verum
end;
thus
( 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 ) ) ) )proof
reconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
assume that A21:
i = 1
and A22:
j = 1
;
A * (i,j) = 0. K
reconsider qq =
f /. i0 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
A23:
len f = n
by MATRIX_0:def 2;
then f /. i0 =
f . i0
by A1, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,
i0)
by A1, Th26
;
then A24:
qq . j = 0. K
by A4, A8, A21, A22, Th25;
A . i =
A /. i
by A15, A3, A4, FINSEQ_4:15
.=
f /. i0
by A1, A2, A4, A21, A23, FINSEQ_7:31
;
hence
A * (
i,
j)
= 0. K
by A7, A24, MATRIX_0:def 5;
verum
end;
thus
( 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 ) ) )proof
reconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
assume that A25:
i = i0
and A26:
j = i0
;
A * (i,j) = 0. K
reconsider qq =
f /. 1 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
A27:
len f = n
by MATRIX_0:def 2;
then f /. 1 =
f . 1
by A16, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,1)
by A16, Th26
;
then A28:
qq . j = 0. K
by A1, A8, A26, Th25;
A . i =
A /. i
by A15, A3, A4, FINSEQ_4:15
.=
f /. 1
by A2, A3, A4, A16, A25, A27, FINSEQ_7:31
;
hence
A * (
i,
j)
= 0. K
by A7, A28, MATRIX_0:def 5;
verum
end;
assume A29:
( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) )
; ( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) )
per cases
( ( i <> 1 & i <> i0 ) or ( j <> 1 & j <> i0 ) )
by A29;
suppose A30:
(
i <> 1 &
i <> i0 )
;
( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) )thus
(
i = j implies
A * (
i,
j)
= 1. K )
( i <> j implies A * (i,j) = 0. K )proof
reconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
assume A31:
i = j
;
A * (i,j) = 1. K
reconsider qq =
f /. i as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
j <= len f
by A6, MATRIX_0:def 2;
then f /. i =
f . i
by A5, A31, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,
i)
by A3, A4, Th26
;
then A32:
qq . j = 1. K
by A3, A4, A31, Th24;
A33:
len f = n
by MATRIX_0:def 2;
A . i =
A /. i
by A15, A3, A4, FINSEQ_4:15
.=
f /. i
by A2, A3, A4, A30, A33, FINSEQ_7:30
;
hence
A * (
i,
j)
= 1. K
by A7, A32, MATRIX_0:def 5;
verum
end; thus
(
i <> j implies
A * (
i,
j)
= 0. K )
verumproof
reconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
assume A34:
i <> j
;
A * (i,j) = 0. K
reconsider qq =
f /. i as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
A35:
len f = n
by MATRIX_0:def 2;
then f /. i =
f . i
by A3, A4, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,
i)
by A3, A4, Th26
;
then A36:
qq . j = 0. K
by A5, A6, A34, Th25;
A . i =
A /. i
by A15, A3, A4, FINSEQ_4:15
.=
f /. i
by A2, A3, A4, A30, A35, FINSEQ_7:30
;
hence
A * (
i,
j)
= 0. K
by A7, A36, MATRIX_0:def 5;
verum
end; end; suppose A37:
(
j <> 1 &
j <> i0 )
;
( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) )thus
(
i = j implies
A * (
i,
j)
= 1. K )
( i <> j implies A * (i,j) = 0. K )proof
reconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
assume A38:
i = j
;
A * (i,j) = 1. K
reconsider qq =
f /. i as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
j <= len f
by A6, MATRIX_0:def 2;
then f /. i =
f . i
by A5, A38, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,
i)
by A3, A4, Th26
;
then A39:
qq . j = 1. K
by A3, A4, A38, Th24;
A40:
len f = n
by MATRIX_0:def 2;
A . i =
A /. i
by A15, A3, A4, FINSEQ_4:15
.=
f /. i
by A2, A3, A4, A37, A38, A40, FINSEQ_7:30
;
hence
A * (
i,
j)
= 1. K
by A7, A39, MATRIX_0:def 5;
verum
end; thus
(
i <> j implies
A * (
i,
j)
= 0. K )
verumproof
assume A41:
i <> j
;
A * (i,j) = 0. K
per cases
( ( not i = 1 & not i = i0 ) or i = 1 or i = i0 )
;
suppose A42:
( not
i = 1 & not
i = i0 )
;
A * (i,j) = 0. Kreconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
reconsider qq =
f /. i as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
A43:
len f = n
by MATRIX_0:def 2;
then f /. i =
f . i
by A3, A4, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,
i)
by A3, A4, Th26
;
then A44:
qq . j = 0. K
by A5, A6, A41, Th25;
A . i =
A /. i
by A15, A3, A4, FINSEQ_4:15
.=
f /. i
by A2, A3, A4, A42, A43, FINSEQ_7:30
;
hence
A * (
i,
j)
= 0. K
by A7, A44, MATRIX_0:def 5;
verum end; suppose A45:
(
i = 1 or
i = i0 )
;
A * (i,j) = 0. Kper cases
( i = 1 or i = i0 )
by A45;
suppose A46:
i = 1
;
A * (i,j) = 0. Kreconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
reconsider qq =
f /. i0 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
A47:
len f = n
by MATRIX_0:def 2;
then f /. i0 =
f . i0
by A1, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,
i0)
by A1, Th26
;
then A48:
qq . j = 0. K
by A5, A6, A37, Th25;
A . i =
A /. i
by A15, A3, A4, FINSEQ_4:15
.=
f /. i0
by A1, A2, A4, A46, A47, FINSEQ_7:31
;
hence
A * (
i,
j)
= 0. K
by A7, A48, MATRIX_0:def 5;
verum end; suppose A49:
i = i0
;
A * (i,j) = 0. Kreconsider f =
1. (
K,
n) as
FinSequence of the
carrier of
K * ;
reconsider qq =
f /. 1 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
A50:
len f = n
by MATRIX_0:def 2;
then f /. 1 =
f . 1
by A16, FINSEQ_4:15
.=
Base_FinSeq (
K,
n,1)
by A16, Th26
;
then A51:
qq . j = 0. K
by A5, A6, A37, Th25;
A . i =
A /. i
by A15, A3, A4, FINSEQ_4:15
.=
f /. 1
by A2, A3, A4, A16, A49, A50, FINSEQ_7:31
;
hence
A * (
i,
j)
= 0. K
by A7, A51, MATRIX_0:def 5;
verum end; end; end; end;
end; end; end;