let n be Element of NAT ; :: thesis:
let K be Field; :: thesis:
let A be Matrix of n,K; :: thesis:
let i0 be Element of NAT ; :: thesis:
assume A1: ( 1 <= i0 & i0 <= n ) ; :: thesis:
thus for j being Element of NAT st 1 <= j & j <= n holds
( ((SwapDiagonal K,n,i0) * A) * i0,j = A * 1,j & ((SwapDiagonal K,n,i0) * A) * 1,j = A * i0,j ) :: thesis:

proof

let j be Element of NAT ; :: thesis:
assume B1: ( 1 <= j & j <= n ) ; :: thesis:
B12: 1 <= n by B1, XXREAL_0:2;
B3: 1 in Seg n by B12, FINSEQ_1:3;
B2: j in Seg n by B1, FINSEQ_1:3;
set Q = SwapDiagonal K,n,i0;
set P = A;
B9: ( len ((SwapDiagonal K,n,i0) * A) = n & width ((SwapDiagonal K,n,i0) * A) = n & Indices ((SwapDiagonal K,n,i0) * A) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
A2a: ( len (SwapDiagonal K,n,i0) = n & width (SwapDiagonal K,n,i0) = n & Indices (SwapDiagonal K,n,i0) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
A2d: ( len A = n & width A = n & Indices A = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
A9: 1 in dom A by B3, A2d, FINSEQ_1:def 3;
C1: ( 1 <= n & 1 <= i0 & i0 <= n ) by A1, XXREAL_0:2;
C1a: i0 in Seg n by A1, FINSEQ_1:3;
A9b: i0 in dom A by A2d, C1a, FINSEQ_1:def 3;
A6: Line (SwapDiagonal K,n,i0),1 = Base_FinSeq K,n,i0

proof

C2: len (Base_FinSeq K,n,i0) = n by AA1100
.= width (SwapDiagonal K,n,i0) by MATRIX_1:25 ;
for j2 being Nat st j2 in Seg (width (SwapDiagonal K,n,i0)) holds
(Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2

proof

let j2 be Nat; :: thesis:
assume j2 in Seg (width (SwapDiagonal K,n,i0)) ; :: thesis:
then D2: ( 1 <= j2 & j2 <= n ) by A2a, FINSEQ_1:3;
reconsider j3 = j2 as Element of NAT by ORDINAL1:def 13;

now

per cases ;

suppose D0: i0 <> 1 ; :: thesis:

now

per cases ;

suppose ( i0 = 1 & j2 = i0 ) ; :: thesis:

hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 by D0; :: thesis:

end;

suppose E0: ( i0 = i0 & j2 = 1 ) ; :: thesis:

(SwapDiagonal K,n,i0) * 1,j3 = 0. K by XA, D2, D0, E0, A1;
hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 by C1, E0, AA1120, D0; :: thesis:

end;

suppose ( i0 = 1 & j2 = 1 ) ; :: thesis:

hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 by D0; :: thesis:

end;

suppose E0: ( i0 = i0 & j2 = i0 ) ; :: thesis:

(SwapDiagonal K,n,i0) * 1,j3 = 1. K by C1, XA, D0, E0;
hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 by D2, E0, AA1110; :: thesis:

end;

suppose E0: ( ( not i0 = 1 & not i0 = i0 ) or ( not j2 = 1 & not j2 = i0 ) ) ; :: thesis:

now

per cases ;

suppose F0: i0 = j2 ; :: thesis:

thus (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 by E0, F0; :: thesis:

end;

suppose F0: i0 <> j2 ; :: thesis:

(SwapDiagonal K,n,i0) * 1,j3 = 0. K by C1, XA, E0, D2, D0;
hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 by A1, D2, F0, AA1120; :: thesis:

end;

hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 ; :: thesis:

end;

hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 ; :: thesis:

end;

suppose D0: i0 = 1 ; :: thesis:

now

per cases ;

suppose E0: i0 = j2 ; :: thesis:

(SwapDiagonal K,n,i0) * 1,j3 = 1. K by XB, D2, D0, E0;
hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 by AA1110, D2, E0; :: thesis:

end;

suppose E0: i0 <> j2 ; :: thesis:

(SwapDiagonal K,n,i0) * 1,j3 = 0. K by A1, D2, XC, D0, E0;
hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 by A1, D2, E0, AA1120; :: thesis:

end;

hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 ; :: thesis:

end;

hence (Base_FinSeq K,n,i0) . j2 = (SwapDiagonal K,n,i0) * 1,j2 ; :: thesis:

end;

hence Line (SwapDiagonal K,n,i0),1 = Base_FinSeq K,n,i0 by C2, MATRIX_1:def 8; :: thesis:

end;

A6b: Line (SwapDiagonal K,n,i0),i0 = Base_FinSeq K,n,1

proof

C1: ( 1 <= n & 1 <= i0 & i0 <= n ) by A1, XXREAL_0:2;
C2: len (Base_FinSeq K,n,1) = n by AA1100
.= width (SwapDiagonal K,n,i0) by MATRIX_1:25 ;
for j2 being Nat st j2 in Seg (width (SwapDiagonal K,n,i0)) holds
(Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2

proof

now

per cases ;

suppose D0: i0 <> 1 ; :: thesis:

now

per cases ;

suppose ( i0 = 1 & j2 = i0 ) ; :: thesis:

hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 by D0; :: thesis:

end;

suppose E0: ( i0 = i0 & j2 = 1 ) ; :: thesis:

(SwapDiagonal K,n,i0) * i0,j3 = 1. K by C1, XA, D0, E0;
hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 by D2, E0, AA1110; :: thesis:

end;

suppose ( i0 = 1 & j2 = 1 ) ; :: thesis:

hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 by D0; :: thesis:

end;

suppose E0: ( i0 = i0 & j2 = i0 ) ; :: thesis:

then (SwapDiagonal K,n,i0) * i0,j3 = 0. K by XA, D2, D0;
hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 by C1, E0, AA1120, D0; :: thesis:

end;

suppose E0: ( ( not i0 = 1 & not i0 = i0 ) or ( not j2 = 1 & not j2 = i0 ) ) ; :: thesis:

now

per cases ;

suppose F0: i0 = j2 ; :: thesis:

thus (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 by E0, F0; :: thesis:

end;

suppose i0 <> j2 ; :: thesis:

(SwapDiagonal K,n,i0) * i0,j3 = 0. K by A1, XA, E0, D2, D0;
hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 by C1, D2, E0, AA1120; :: thesis:

end;

hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 ; :: thesis:

end;

hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 ; :: thesis:

end;

suppose D0: i0 = 1 ; :: thesis:

now

per cases ;

suppose E0: i0 = j2 ; :: thesis:

(SwapDiagonal K,n,i0) * i0,j3 = 1. K by XB, D2, D0, E0;
hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 by AA1110, D2, D0, E0; :: thesis:

end;

suppose E0: i0 <> j2 ; :: thesis:

(SwapDiagonal K,n,1) * i0,j3 = 0. K by D2, XC, E0, A1;
hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 by A1, D2, E0, AA1120, D0; :: thesis:

end;

hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 ; :: thesis:

end;

hence (Base_FinSeq K,n,1) . j2 = (SwapDiagonal K,n,i0) * i0,j2 ; :: thesis:

end;

hence Line (SwapDiagonal K,n,i0),i0 = Base_FinSeq K,n,1 by C2, MATRIX_1:def 8; :: thesis:

end;

A10: len (Col A,j) = n by A2d, MATRIX_1:def 9;
B18: 1 <= n by B1, XXREAL_0:2;
B8b: 1 in Seg n by B18, FINSEQ_1:3;
A22: [i0,j] in Indices ((SwapDiagonal K,n,i0) * A) by B1, A1, MATRIX_1:38;
A22b: [1,j] in Indices ((SwapDiagonal K,n,i0) * A) by B8b, B2, B9, ZFMISC_1:106;
thus ((SwapDiagonal K,n,i0) * A) * i0,j = |((Base_FinSeq K,n,1),(Col A,j))| by A6b, A2a, A2d, A22, MATRIX_3:def 4
.= |((Col A,j),(Base_FinSeq K,n,1))| by FVSUM_1:115
.= (Col A,j) . 1 by AA2627, A10, B12
.= A * 1,j by A9, MATRIX_1:def 9 ; :: thesis:
thus ((SwapDiagonal K,n,i0) * A) * 1,j = |((Base_FinSeq K,n,i0),(Col A,j))| by A6, A2a, A2d, A22b, MATRIX_3:def 4
.= |((Col A,j),(Base_FinSeq K,n,i0))| by FVSUM_1:115
.= (Col A,j) . i0 by A1, AA2627, A10
.= A * i0,j by A9b, MATRIX_1:def 9 ; :: thesis:

end;

thus for i, j being Element of NAT st i <> 1 & i <> i0 & 1 <= i & i <= n & 1 <= j & j <= n holds
((SwapDiagonal K,n,i0) * A) * i,j = A * i,j :: thesis:

proof

let i, j be Element of NAT ; :: thesis:
assume B1: ( i <> 1 & i <> i0 & 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis:
B3b: i in Seg n by B1, FINSEQ_1:3;
set Q = SwapDiagonal K,n,i0;
set P = A;
A2a: ( len (SwapDiagonal K,n,i0) = n & width (SwapDiagonal K,n,i0) = n & Indices (SwapDiagonal K,n,i0) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
A2d: ( len A = n & width A = n & Indices A = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
A9c: i in dom A by B3b, A2d, FINSEQ_1:def 3;
A6d: Line (SwapDiagonal K,n,i0),i = Base_FinSeq K,n,i

proof

C2: len (Base_FinSeq K,n,i) = n by AA1100
.= width (SwapDiagonal K,n,i0) by MATRIX_1:25 ;
for j2 being Nat st j2 in Seg (width (SwapDiagonal K,n,i0)) holds
(Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2

proof

now

per cases ;

suppose D0: i0 <> 1 ; :: thesis:

now

per cases ;

suppose ( i = 1 & j2 = i0 ) ; :: thesis:

hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 by B1; :: thesis:

end;

suppose ( i = i0 & j2 = 1 ) ; :: thesis:

hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 by B1; :: thesis:

end;

suppose ( i = 1 & j2 = 1 ) ; :: thesis:

hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 by B1; :: thesis:

end;

suppose E0: ( i = i0 & j2 = i0 ) ; :: thesis:

thus (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 by B1, E0; :: thesis:

end;

suppose E0: ( ( not i = 1 & not i = i0 ) or ( not j2 = 1 & not j2 = i0 ) ) ; :: thesis:

now

per cases ;

suppose F0: i = j2 ; :: thesis:

then (SwapDiagonal K,n,i0) * i,j3 = 1. K by XA, A1, E0, D2, D0;
hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 by B1, F0, AA1110; :: thesis:

end;

suppose F0: i <> j2 ; :: thesis:

(SwapDiagonal K,n,i0) * i,j3 = 0. K by B1, XA, A1, D2, D0, F0;
hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 by B1, D2, F0, AA1120; :: thesis:

end;

hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 ; :: thesis:

end;

hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 ; :: thesis:

end;

suppose D0: i0 = 1 ; :: thesis:

now

per cases ;

suppose E0: i = j2 ; :: thesis:

(SwapDiagonal K,n,i0) * i,j3 = 1. K by XB, D2, D0, E0;
hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 by AA1110, D2, E0; :: thesis:

end;

suppose E0: i <> j2 ; :: thesis:

(SwapDiagonal K,n,i0) * i,j3 = 0. K by B1, D2, XC, D0, E0;
hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 by AA1120, B1, D2, E0; :: thesis:

end;

hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 ; :: thesis:

end;

hence (Base_FinSeq K,n,i) . j2 = (SwapDiagonal K,n,i0) * i,j2 ; :: thesis:

end;

hence Line (SwapDiagonal K,n,i0),i = Base_FinSeq K,n,i by C2, MATRIX_1:def 8; :: thesis:

end;

A10: len (Col A,j) = n by A2d, MATRIX_1:def 9;
A22: [i,j] in Indices ((SwapDiagonal K,n,i0) * A) by B1, MATRIX_1:38;
thus ((SwapDiagonal K,n,i0) * A) * i,j = |((Base_FinSeq K,n,i),(Col A,j))| by A6d, A2a, A2d, A22, MATRIX_3:def 4
.= |((Col A,j),(Base_FinSeq K,n,i))| by FVSUM_1:115
.= (Col A,j) . i by AA2627, A10, B1
.= A * i,j by A9c, MATRIX_1:def 9 ; :: thesis:

end;