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 that
A1: 1 <= i0 and
A2: 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

set Q = SwapDiagonal (K,n,i0);
set P = A;
let j be Element of NAT ; :: thesis:
A3: width (SwapDiagonal (K,n,i0)) = n by MATRIX_0:24;
A4: 1 <= n by A1, A2, XXREAL_0:2;
A5: 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:
reconsider j3 = j2 as Element of NAT by ORDINAL1:def 12;
assume A6: j2 in Seg (width (SwapDiagonal (K,n,i0))) ; :: thesis:
then A7: 1 <= j2 by FINSEQ_1:1;
A8: j2 <= n by A3, A6, FINSEQ_1:1;

now :: thesis:

per cases ;

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

now :: thesis:

per cases ;

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

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

end;

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

then (SwapDiagonal (K,n,i0)) * (1,j3) = 0. K by A1, A2, A8, A9, Th43;
hence (Base_FinSeq (K,n,i0)) . j2 = (SwapDiagonal (K,n,i0)) * (1,j2) by A4, A9, A10, Th25; :: thesis:

end;

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

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

end;

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

then (SwapDiagonal (K,n,i0)) * (1,j3) = 1. K by A1, A2, A4, A9, Th43;
hence (Base_FinSeq (K,n,i0)) . j2 = (SwapDiagonal (K,n,i0)) * (1,j2) by A7, A8, A11, Th24; :: thesis:

end;

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

now :: thesis:

per cases ;

suppose i0 = j2 ; :: thesis:

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

end;

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

(SwapDiagonal (K,n,i0)) * (1,j3) = 0. K by A1, A2, A4, A7, A8, A9, A12, Th43;
hence (Base_FinSeq (K,n,i0)) . j2 = (SwapDiagonal (K,n,i0)) * (1,j2) by A7, A8, A13, Th25; :: thesis:

end;

end;

end;

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

end;

end;

end;

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

end;

suppose A14: i0 = 1 ; :: thesis:

now :: thesis:

per cases ;

suppose A15: i0 = j2 ; :: thesis:

then (SwapDiagonal (K,n,i0)) * (1,j3) = 1. K by A8, A14, Th44;
hence (Base_FinSeq (K,n,i0)) . j2 = (SwapDiagonal (K,n,i0)) * (1,j2) by A7, A8, A15, Th24; :: thesis:

end;

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

then (SwapDiagonal (K,n,i0)) * (1,j3) = 0. K by A2, A7, A8, A14, Th45;
hence (Base_FinSeq (K,n,i0)) . j2 = (SwapDiagonal (K,n,i0)) * (1,j2) by A7, A8, A16, Th25; :: thesis:

end;

end;

end;

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

end;

end;

end;

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

end;

assume A17: ( 1 <= j & j <= n ) ; :: thesis:
then 1 <= n by XXREAL_0:2;
then A18: ( Indices ((SwapDiagonal (K,n,i0)) * A) = [:(Seg n),(Seg n):] & 1 in Seg n ) by FINSEQ_1:1, MATRIX_0:24;
A19: 1 <= n by A1, A2, XXREAL_0:2;
A20: 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

let j2 be Nat; :: thesis:
reconsider j3 = j2 as Element of NAT by ORDINAL1:def 12;
assume A21: j2 in Seg (width (SwapDiagonal (K,n,i0))) ; :: thesis:
then A22: 1 <= j2 by FINSEQ_1:1;
A23: j2 <= n by A3, A21, FINSEQ_1:1;

now :: thesis:

per cases ;

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

now :: thesis:

per cases ;

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

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

end;

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

then (SwapDiagonal (K,n,i0)) * (i0,j3) = 1. K by A1, A2, A19, A24, Th43;
hence (Base_FinSeq (K,n,1)) . j2 = (SwapDiagonal (K,n,i0)) * (i0,j2) by A23, A25, Th24; :: thesis:

end;

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

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

end;

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

then (SwapDiagonal (K,n,i0)) * (i0,j3) = 0. K by A22, A23, A24, Th43;
hence (Base_FinSeq (K,n,1)) . j2 = (SwapDiagonal (K,n,i0)) * (i0,j2) by A1, A2, A24, A26, Th25; :: thesis:

end;

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

now :: thesis:

(SwapDiagonal (K,n,i0)) * (i0,j3) = 0. K by A1, A2, A22, A23, A24, A27, Th43;
hence (Base_FinSeq (K,n,1)) . j2 = (SwapDiagonal (K,n,i0)) * (i0,j2) by A22, A23, A27, Th25; :: thesis:

end;

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

end;

end;

end;

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

end;

suppose A28: i0 = 1 ; :: thesis:

now :: thesis:

per cases ;

suppose A29: i0 = j2 ; :: thesis:

then (SwapDiagonal (K,n,i0)) * (i0,j3) = 1. K by A23, A28, Th44;
hence (Base_FinSeq (K,n,1)) . j2 = (SwapDiagonal (K,n,i0)) * (i0,j2) by A23, A28, A29, Th24; :: thesis:

end;

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

then (SwapDiagonal (K,n,1)) * (i0,j3) = 0. K by A1, A2, A22, A23, Th45;
hence (Base_FinSeq (K,n,1)) . j2 = (SwapDiagonal (K,n,i0)) * (i0,j2) by A22, A23, A28, A30, Th25; :: thesis:

end;

end;

end;

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

end;

end;

end;

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

end;

len (Base_FinSeq (K,n,1)) = n by Th23
.= width (SwapDiagonal (K,n,i0)) by MATRIX_0:24 ;
then A31: Line ((SwapDiagonal (K,n,i0)),i0) = Base_FinSeq (K,n,1) by A20, MATRIX_0:def 7;
A32: len A = n by MATRIX_0:24;
then A33: len (Col (A,j)) = n by MATRIX_0:def 8;
A34: 1 <= n by A17, XXREAL_0:2;
then 1 in Seg n by FINSEQ_1:1;
then A35: 1 in dom A by A32, FINSEQ_1:def 3;
j in Seg n by A17, FINSEQ_1:1;
then A36: [1,j] in Indices ((SwapDiagonal (K,n,i0)) * A) by A18, ZFMISC_1:87;
[i0,j] in Indices ((SwapDiagonal (K,n,i0)) * A) by A1, A2, A17, MATRIX_0:31;
hence ((SwapDiagonal (K,n,i0)) * A) * (i0,j) = |((Base_FinSeq (K,n,1)),(Col (A,j)))| by A3, A32, A31, MATRIX_3:def 4
.= |((Col (A,j)),(Base_FinSeq (K,n,1)))| by FVSUM_1:90
.= (Col (A,j)) . 1 by A34, A33, Th35
.= A * (1,j) by A35, MATRIX_0:def 8 ;
:: thesis:
i0 in Seg n by A1, A2, FINSEQ_1:1;
then A37: i0 in dom A by A32, FINSEQ_1:def 3;
len (Base_FinSeq (K,n,i0)) = n by Th23
.= width (SwapDiagonal (K,n,i0)) by MATRIX_0:24 ;
then Line ((SwapDiagonal (K,n,i0)),1) = Base_FinSeq (K,n,i0) by A5, MATRIX_0:def 7;
hence ((SwapDiagonal (K,n,i0)) * A) * (1,j) = |((Base_FinSeq (K,n,i0)),(Col (A,j)))| by A3, A32, A36, MATRIX_3:def 4
.= |((Col (A,j)),(Base_FinSeq (K,n,i0)))| by FVSUM_1:90
.= (Col (A,j)) . i0 by A1, A2, A33, Th35
.= A * (i0,j) by A37, MATRIX_0:def 8 ;
:: 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

set Q = SwapDiagonal (K,n,i0);
set P = A;
let i, j be Element of NAT ; :: thesis:
assume that
A38: i <> 1 and
A39: i <> i0 and
A40: ( 1 <= i & i <= n ) and
A41: ( 1 <= j & j <= n ) ; :: thesis:
A42: len A = n by MATRIX_0:24;
then A43: len (Col (A,j)) = n by MATRIX_0:def 8;
A44: width (SwapDiagonal (K,n,i0)) = n by MATRIX_0:24;
A45: 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

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

now :: thesis:

per cases ;

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

now :: thesis:

per cases ;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

now :: thesis:

per cases ;

suppose A49: i = j2 ; :: thesis:

then (SwapDiagonal (K,n,i0)) * (i,j3) = 1. K by A1, A2, A46, A47, A48, Th43;
hence (Base_FinSeq (K,n,i)) . j2 = (SwapDiagonal (K,n,i0)) * (i,j2) by A40, A49, Th24; :: thesis:

end;

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

then (SwapDiagonal (K,n,i0)) * (i,j3) = 0. K by A1, A2, A38, A39, A40, A46, A47, Th43;
hence (Base_FinSeq (K,n,i)) . j2 = (SwapDiagonal (K,n,i0)) * (i,j2) by A46, A50, Th25; :: thesis:

end;

end;

end;

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

end;

end;

end;

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

end;

suppose A51: i0 = 1 ; :: thesis:

now :: thesis:

per cases ;

suppose A52: i = j2 ; :: thesis:

then (SwapDiagonal (K,n,i0)) * (i,j3) = 1. K by A46, A51, Th44;
hence (Base_FinSeq (K,n,i)) . j2 = (SwapDiagonal (K,n,i0)) * (i,j2) by A46, A52, Th24; :: thesis:

end;

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

then (SwapDiagonal (K,n,i0)) * (i,j3) = 0. K by A40, A46, A51, Th45;
hence (Base_FinSeq (K,n,i)) . j2 = (SwapDiagonal (K,n,i0)) * (i,j2) by A46, A53, Th25; :: thesis:

end;

end;

end;

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

end;

end;

end;

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

end;

i in Seg n by A40, FINSEQ_1:1;
then A54: i in dom A by A42, FINSEQ_1:def 3;
len (Base_FinSeq (K,n,i)) = n by Th23
.= width (SwapDiagonal (K,n,i0)) by MATRIX_0:24 ;
then A55: Line ((SwapDiagonal (K,n,i0)),i) = Base_FinSeq (K,n,i) by A45, MATRIX_0:def 7;
[i,j] in Indices ((SwapDiagonal (K,n,i0)) * A) by A40, A41, MATRIX_0:31;
hence ((SwapDiagonal (K,n,i0)) * A) * (i,j) = |((Base_FinSeq (K,n,i)),(Col (A,j)))| by A44, A42, A55, MATRIX_3:def 4
.= |((Col (A,j)),(Base_FinSeq (K,n,i)))| by FVSUM_1:90
.= (Col (A,j)) . i by A40, A43, Th35
.= A * (i,j) by A54, MATRIX_0:def 8 ;
:: thesis:

end;