let l, n, k be Nat; :: thesis: for K being Field
for A being Matrix of n,K st l in dom (1. K,n) & k in dom (1. K,n) holds
(ILine (1. K,n),l,k) * A = ILine A,l,k
let K be Field; :: thesis: for A being Matrix of n,K st l in dom (1. K,n) & k in dom (1. K,n) holds
(ILine (1. K,n),l,k) * A = ILine A,l,k
let A be Matrix of n,K; :: thesis: ( l in dom (1. K,n) & k in dom (1. K,n) implies (ILine (1. K,n),l,k) * A = ILine A,l,k )
assume that
A1: l in dom (1. K,n) and
A2: k in dom (1. K,n) ; :: thesis: (ILine (1. K,n),l,k) * A = ILine A,l,k
set B = ILine (1. K,n),l,k;
A3: ( len (ILine (1. K,n),l,k) = len (1. K,n) & len (ILine (1. K,n),l,k) = n ) by Def1, MATRIX_1:25;
then A4: l in Seg n by A1, FINSEQ_1:def 3;
A5: k in Seg n by A2, A3, FINSEQ_1:def 3;
A6: width (ILine (1. K,n),l,k) = n by MATRIX_1:25;
A7: Indices ((ILine (1. K,n),l,k) * A) = [:(Seg n),(Seg n):] by MATRIX_1:25;
A8: width A = n by MATRIX_1:25;
A9: len A = n by MATRIX_1:25;
A10: width (ILine (1. K,n),l,k) = width (1. K,n) by Th1;
A11: for i, j being Nat st j in Seg n & i in dom (1. K,n) & i <> l & i <> k holds
((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j

proof

let i, j be Nat; :: thesis: ( j in Seg n & i in dom (1. K,n) & i <> l & i <> k implies ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j )
assume that
A12: j in Seg n and
A13: i in dom (1. K,n) ; :: thesis: ( not i <> l or not i <> k or ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j )
A14: i in Seg n by A3, A13, FINSEQ_1:def 3;
then A15: [i,i] in Indices (1. K,n) by A10, A6, A13, ZFMISC_1:106;
thus ( i <> l & i <> k implies ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j ) :: thesis: verum

proof

A16: ( (Line (1. K,n),i) . i = 1_ K & ( for t being Nat st t in dom (Line (1. K,n),i) & t <> i holds
(Line (1. K,n),i) . t = 0. K ) )

proof

thus (Line (1. K,n),i) . i = 1_ K by A15, MATRIX_3:17; :: thesis: for t being Nat st t in dom (Line (1. K,n),i) & t <> i holds
(Line (1. K,n),i) . t = 0. K
let t be Nat; :: thesis: ( t in dom (Line (1. K,n),i) & t <> i implies (Line (1. K,n),i) . t = 0. K )
assume that
A17: t in dom (Line (1. K,n),i) and
A18: t <> i ; :: thesis: (Line (1. K,n),i) . t = 0. K
t in Seg (len (Line (1. K,n),i)) by A17, FINSEQ_1:def 3;
then t in Seg (width (1. K,n)) by MATRIX_1:def 8;
then [i,t] in Indices (1. K,n) by A13, ZFMISC_1:106;
hence (Line (1. K,n),i) . t = 0. K by A18, MATRIX_3:17; :: thesis: verum

end;

len (Col A,j) = len A by MATRIX_1:def 9;
then A19: i in dom (Col A,j) by A9, A14, FINSEQ_1:def 3;
A20: dom (1. K,n) = Seg (len (1. K,n)) by FINSEQ_1:def 3
.= Seg (len A) by A9, MATRIX_1:25
.= dom A by FINSEQ_1:def 3 ;
len (Line (1. K,n),i) = width (1. K,n) by MATRIX_1:def 8;
then A21: i in dom (Line (1. K,n),i) by A10, A6, A14, FINSEQ_1:def 3;
assume A22: ( i <> l & i <> k ) ; :: thesis: ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j
[i,j] in Indices ((ILine (1. K,n),l,k) * A) by A7, A12, A14, ZFMISC_1:106;
then ((ILine (1. K,n),l,k) * A) * i,j = (Line (ILine (1. K,n),l,k),i) "*" (Col A,j) by A6, A9, MATRIX_3:def 4
.= Sum (mlt (Line (1. K,n),i),(Col A,j)) by A1, A2, A13, A22, Th2
.= (Col A,j) . i by A21, A19, A16, MATRIX_3:19
.= A * i,j by A13, A20, MATRIX_1:def 9
.= (ILine A,l,k) * i,j by A8, A12, A13, A22, A20, Def1 ;
hence ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j ; :: thesis: verum

end;

end;

A23: l in Seg (width (1. K,n)) by A1, A10, A3, A6, FINSEQ_1:def 3;
then A24: [l,l] in Indices (1. K,n) by A1, ZFMISC_1:106;
A25: for i, j being Nat st j in Seg n & i in dom (1. K,n) & i = k holds
((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j

proof

let i, j be Nat; :: thesis: ( j in Seg n & i in dom (1. K,n) & i = k implies ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j )
assume that
A26: j in Seg n and
A27: i in dom (1. K,n) ; :: thesis: ( not i = k or ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j )
thus ( i = k implies ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j ) :: thesis: verum

proof

A28: ( (Line (1. K,n),l) . l = 1_ K & ( for t being Nat st t in dom (Line (1. K,n),l) & t <> l holds
(Line (1. K,n),l) . t = 0. K ) )

proof

thus (Line (1. K,n),l) . l = 1_ K by A24, MATRIX_3:17; :: thesis: for t being Nat st t in dom (Line (1. K,n),l) & t <> l holds
(Line (1. K,n),l) . t = 0. K
let t be Nat; :: thesis: ( t in dom (Line (1. K,n),l) & t <> l implies (Line (1. K,n),l) . t = 0. K )
assume that
A29: t in dom (Line (1. K,n),l) and
A30: t <> l ; :: thesis: (Line (1. K,n),l) . t = 0. K
t in Seg (len (Line (1. K,n),l)) by A29, FINSEQ_1:def 3;
then t in Seg (width (1. K,n)) by MATRIX_1:def 8;
then [l,t] in Indices (1. K,n) by A1, ZFMISC_1:106;
hence (Line (1. K,n),l) . t = 0. K by A30, MATRIX_3:17; :: thesis: verum

end;

len (Line (1. K,n),l) = width (1. K,n) by MATRIX_1:def 8;
then A31: l in dom (Line (1. K,n),l) by A23, FINSEQ_1:def 3;
( len (Col A,j) = len A & l in Seg n ) by A1, A3, FINSEQ_1:def 3, MATRIX_1:def 9;
then A32: l in dom (Col A,j) by A9, FINSEQ_1:def 3;
A33: dom (1. K,n) = Seg (len (1. K,n)) by FINSEQ_1:def 3
.= Seg (len A) by A9, MATRIX_1:25
.= dom A by FINSEQ_1:def 3 ;
assume A34: i = k ; :: thesis: ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j
then [i,j] in Indices ((ILine (1. K,n),l,k) * A) by A5, A7, A26, ZFMISC_1:106;
then ((ILine (1. K,n),l,k) * A) * i,j = (Line (ILine (1. K,n),l,k),i) "*" (Col A,j) by A6, A9, MATRIX_3:def 4
.= Sum (mlt (Line (1. K,n),l),(Col A,j)) by A1, A2, A34, Th2
.= (Col A,j) . l by A31, A32, A28, MATRIX_3:19
.= A * l,j by A1, A33, MATRIX_1:def 9
.= (ILine A,l,k) * i,j by A8, A26, A27, A34, A33, Def1 ;
hence ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j ; :: thesis: verum

end;

end;

A35: k in Seg (width (1. K,n)) by A2, A10, A3, A6, FINSEQ_1:def 3;
then A36: [k,k] in Indices (1. K,n) by A2, ZFMISC_1:106;
A37: for i, j being Nat st j in Seg n & i in dom (1. K,n) & i = l holds
((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j

proof

let i, j be Nat; :: thesis: ( j in Seg n & i in dom (1. K,n) & i = l implies ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j )
assume that
A38: j in Seg n and
A39: i in dom (1. K,n) ; :: thesis: ( not i = l or ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j )
thus ( i = l implies ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j ) :: thesis: verum

proof

A40: ( (Line (1. K,n),k) . k = 1_ K & ( for t being Nat st t in dom (Line (1. K,n),k) & t <> k holds
(Line (1. K,n),k) . t = 0. K ) )

proof

thus (Line (1. K,n),k) . k = 1_ K by A36, MATRIX_3:17; :: thesis: for t being Nat st t in dom (Line (1. K,n),k) & t <> k holds
(Line (1. K,n),k) . t = 0. K
let t be Nat; :: thesis: ( t in dom (Line (1. K,n),k) & t <> k implies (Line (1. K,n),k) . t = 0. K )
assume that
A41: t in dom (Line (1. K,n),k) and
A42: t <> k ; :: thesis: (Line (1. K,n),k) . t = 0. K
t in Seg (len (Line (1. K,n),k)) by A41, FINSEQ_1:def 3;
then t in Seg (width (1. K,n)) by MATRIX_1:def 8;
then [k,t] in Indices (1. K,n) by A2, ZFMISC_1:106;
hence (Line (1. K,n),k) . t = 0. K by A42, MATRIX_3:17; :: thesis: verum

end;

len (Line (1. K,n),k) = width (1. K,n) by MATRIX_1:def 8;
then A43: k in dom (Line (1. K,n),k) by A35, FINSEQ_1:def 3;
( len (Col A,j) = len A & k in Seg n ) by A2, A3, FINSEQ_1:def 3, MATRIX_1:def 9;
then A44: k in dom (Col A,j) by A9, FINSEQ_1:def 3;
A45: dom (1. K,n) = Seg (len (1. K,n)) by FINSEQ_1:def 3
.= Seg (len A) by A9, MATRIX_1:25
.= dom A by FINSEQ_1:def 3 ;
assume A46: i = l ; :: thesis: ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j
then [i,j] in Indices ((ILine (1. K,n),l,k) * A) by A4, A7, A38, ZFMISC_1:106;
then ((ILine (1. K,n),l,k) * A) * i,j = (Line (ILine (1. K,n),l,k),i) "*" (Col A,j) by A6, A9, MATRIX_3:def 4
.= Sum (mlt (Line (1. K,n),k),(Col A,j)) by A1, A2, A46, Th2
.= (Col A,j) . k by A43, A44, A40, MATRIX_3:19
.= A * k,j by A2, A45, MATRIX_1:def 9
.= (ILine A,l,k) * i,j by A8, A38, A39, A46, A45, Def1 ;
hence ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j ; :: thesis: verum

end;

end;

A47: for i, j being Nat st [i,j] in Indices ((ILine (1. K,n),l,k) * A) holds
((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((ILine (1. K,n),l,k) * A) implies ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j )
assume A48: [i,j] in Indices ((ILine (1. K,n),l,k) * A) ; :: thesis: ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j
dom (1. K,n) = Seg (len (1. K,n)) by FINSEQ_1:def 3
.= Seg n by MATRIX_1:25 ;
then A49: i in dom (1. K,n) by A7, A48, ZFMISC_1:106;
A50: j in Seg n by A7, A48, ZFMISC_1:106;
then ( i = l implies ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j ) by A37, A49;
hence ((ILine (1. K,n),l,k) * A) * i,j = (ILine A,l,k) * i,j by A25, A11, A49, A50; :: thesis: verum

end;

A51: ( len ((ILine (1. K,n),l,k) * A) = n & width ((ILine (1. K,n),l,k) * A) = n ) by MATRIX_1:25;
( len (ILine A,l,k) = len A & width (ILine A,l,k) = width A ) by Def1, Th1;
hence (ILine (1. K,n),l,k) * A = ILine A,l,k by A9, A8, A51, A47, MATRIX_1:21; :: thesis: verum