let K be Field; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A0:
( 1 <= i0 & i0 <= n )
; :: thesis: ( 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 A1:
A = SwapDiagonal K,n,i0
; :: thesis: 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 ) ) ) )
B44:
( len A = n & width A = n & Indices A = [:(Seg n),(Seg n):] )
by MATRIX_1:25;
let i, j be Nat; :: thesis: ( 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 B1:
( 1 <= i & i <= n & 1 <= j & j <= n )
; :: thesis: ( 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 ) ) ) ) )
B2:
[i,j] in Indices A
by B1, MATRIX_1:38;
B77:
1 <= n
by B1, XXREAL_0:2;
assume C1:
i0 <> 1
; :: thesis: ( ( 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 )
:: thesis: ( ( 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
assume D0:
(
i = 1 &
j = i0 )
;
:: thesis: A * i,j = 1. K
then D1:
1
< i0
by B1, C1, XXREAL_0:1;
reconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
len (<*(f /. i0)*> ^ h) =
(len <*(f /. i0)*>) + (len h)
by FINSEQ_1:35
.=
1
+ (len h)
by FINSEQ_1:56
;
then D7:
1
<= len (<*(f /. i0)*> ^ h)
by NAT_1:11;
D8:
1
= len <*(f /. i0)*>
by FINSEQ_1:56;
D28:
A . i =
(((<*(f /. i0)*> ^ h) ^ <*(f /. 1)*>) ^ (f /^ i0)) . i
by D0, D1, B1, D20, A1, FINSEQ_7:30
.=
((<*(f /. i0)*> ^ h) ^ (<*(f /. 1)*> ^ (f /^ i0))) . i
by FINSEQ_1:45
.=
(<*(f /. i0)*> ^ h) . 1
by D0, D7, FINSEQ_1:85
.=
<*(f /. i0)*> . 1
by D8, FINSEQ_1:85
.=
f /. i0
by FINSEQ_1:def 8
;
reconsider qq =
f /. i0 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
( 1
<= i0 &
i0 <= len f )
by D0, B1, MATRIX_1:def 3;
then f /. i0 =
f . i0
by FINSEQ_4:24
.=
Base_FinSeq K,
n,
i0
by AA1200, D0, B1
;
then
qq . j = 1. K
by D0, B1, AA1110;
hence
A * i,
j = 1. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum
end;
thus
( i = i0 & j = 1 implies A * i,j = 1. K )
:: thesis: ( ( 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
assume D0:
(
i = i0 &
j = 1 )
;
:: thesis: A * i,j = 1. K
reconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
D28:
A . i =
A /. i
by B44, B1, FINSEQ_4:24
.=
f /. 1
by B1, D20, A1, D0, FINSEQ_7:33
;
reconsider qq =
f /. 1 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
f /. 1 =
f . 1
by B77, D20, FINSEQ_4:24
.=
Base_FinSeq K,
n,1
by B77, AA1200
;
then
qq . j = 1. K
by D0, B1, AA1110;
hence
A * i,
j = 1. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum
end;
thus
( i = 1 & j = 1 implies A * i,j = 0. K )
:: thesis: ( ( 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
assume D0:
(
i = 1 &
j = 1 )
;
:: thesis: A * i,j = 0. K
reconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
D28:
A . i =
A /. i
by B44, B1, FINSEQ_4:24
.=
f /. i0
by A0, D20, B1, A1, D0, FINSEQ_7:33
;
reconsider qq =
f /. i0 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
f /. i0 =
f . i0
by A0, D20, FINSEQ_4:24
.=
Base_FinSeq K,
n,
i0
by AA1200, A0
;
then
qq . j = 0. K
by D0, B1, C1, AA1120, A0;
hence
A * i,
j = 0. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum
end;
thus
( i = i0 & j = i0 implies A * i,j = 0. K )
:: thesis: ( ( ( 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
assume D0:
(
i = i0 &
j = i0 )
;
:: thesis: A * i,j = 0. K
reconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
D28:
A . i =
A /. i
by B44, B1, FINSEQ_4:24
.=
f /. 1
by B1, D20, B77, A1, D0, FINSEQ_7:33
;
reconsider qq =
f /. 1 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
f /. 1 =
f . 1
by B77, D20, FINSEQ_4:24
.=
Base_FinSeq K,
n,1
by B77, AA1200
;
then
qq . j = 0. K
by D0, C1, AA1120, A0, B77;
hence
A * i,
j = 0. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum
end;
assume E0:
( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) )
; :: thesis: ( ( 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 E0;
suppose E1:
(
i <> 1 &
i <> i0 )
;
:: thesis: ( ( 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 )
:: thesis: ( i <> j implies A * i,j = 0. K )proof
assume D0:
i = j
;
:: thesis: A * i,j = 1. K
reconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
D28:
A . i =
A /. i
by B44, B1, FINSEQ_4:24
.=
f /. i
by B1, D20, A1, E1, FINSEQ_7:32
;
reconsider qq =
f /. i as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
( 1
<= j &
j <= len f )
by B1, MATRIX_1:def 3;
then f /. i =
f . i
by D0, FINSEQ_4:24
.=
Base_FinSeq K,
n,
i
by AA1200, B1
;
then
qq . j = 1. K
by D0, B1, AA1110;
hence
A * i,
j = 1. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum
end; thus
(
i <> j implies
A * i,
j = 0. K )
:: thesis: verumproof
assume D0:
i <> j
;
:: thesis: A * i,j = 0. K
reconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
D28:
A . i =
A /. i
by B44, B1, FINSEQ_4:24
.=
f /. i
by B1, D20, A1, E1, FINSEQ_7:32
;
reconsider qq =
f /. i as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
f /. i =
f . i
by B1, D20, FINSEQ_4:24
.=
Base_FinSeq K,
n,
i
by AA1200, B1
;
then
qq . j = 0. K
by D0, AA1120, B1;
hence
A * i,
j = 0. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum
end; end; suppose F0:
(
j <> 1 &
j <> i0 )
;
:: thesis: ( ( 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 )
:: thesis: ( i <> j implies A * i,j = 0. K )proof
assume D0:
i = j
;
:: thesis: A * i,j = 1. K
reconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
D28:
A . i =
A /. i
by B44, B1, FINSEQ_4:24
.=
f /. i
by B1, D20, A1, D0, F0, FINSEQ_7:32
;
reconsider qq =
f /. i as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
( 1
<= j &
j <= len f )
by B1, MATRIX_1:def 3;
then f /. i =
f . i
by D0, FINSEQ_4:24
.=
Base_FinSeq K,
n,
i
by AA1200, B1
;
then
qq . j = 1. K
by D0, B1, AA1110;
hence
A * i,
j = 1. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum
end; thus
(
i <> j implies
A * i,
j = 0. K )
:: thesis: verumproof
assume D0:
i <> j
;
:: thesis: A * i,j = 0. K
per cases
( ( not i = 1 & not i = i0 ) or i = 1 or i = i0 )
;
suppose G0:
( not
i = 1 & not
i = i0 )
;
:: thesis: A * i,j = 0. Kreconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
D28:
A . i =
A /. i
by B44, B1, FINSEQ_4:24
.=
f /. i
by B1, D20, A1, G0, FINSEQ_7:32
;
reconsider qq =
f /. i as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
f /. i =
f . i
by B1, D20, FINSEQ_4:24
.=
Base_FinSeq K,
n,
i
by AA1200, B1
;
then
qq . j = 0. K
by D0, AA1120, B1;
hence
A * i,
j = 0. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum end; suppose G0:
(
i = 1 or
i = i0 )
;
:: thesis: A * i,j = 0. Kper cases
( i = 1 or i = i0 )
by G0;
suppose H0:
i = 1
;
:: thesis: A * i,j = 0. Kreconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
D28:
A . i =
A /. i
by B44, B1, FINSEQ_4:24
.=
f /. i0
by A0, D20, B1, A1, H0, FINSEQ_7:33
;
reconsider qq =
f /. i0 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
f /. i0 =
f . i0
by A0, D20, FINSEQ_4:24
.=
Base_FinSeq K,
n,
i0
by AA1200, A0
;
then
qq . j = 0. K
by AA1120, A0, B1, F0;
hence
A * i,
j = 0. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum end; suppose H0:
i = i0
;
:: thesis: A * i,j = 0. Kreconsider f =
1. K,
n as
FinSequence of the
carrier of
K * ;
D20:
len f = n
by MATRIX_1:def 3;
reconsider g =
f /^ 1 as
FinSequence of the
carrier of
K * ;
reconsider j0 =
i0 -' 2 as
Element of
NAT ;
reconsider h =
g | j0 as
FinSequence of the
carrier of
K * ;
D28:
A . i =
A /. i
by B44, B1, FINSEQ_4:24
.=
f /. 1
by B1, D20, B77, A1, H0, FINSEQ_7:33
;
reconsider qq =
f /. 1 as
FinSequence of the
carrier of
K by FINSEQ_1:def 11;
f /. 1 =
f . 1
by B77, D20, FINSEQ_4:24
.=
Base_FinSeq K,
n,1
by B77, AA1200
;
then
qq . j = 0. K
by AA1120, B77, B1, F0;
hence
A * i,
j = 0. K
by D28, B2, MATRIX_1:def 6;
:: thesis: verum end;
end; end;