:: Some Properties of Line and Column Operations on Matrices
:: by Xiquan Liang , Tao Sun and Dahai Hu
::
:: Received August 13, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, XCMPLX_0, NUMBERS, NAT_1, VECTSP_1, VECTSP_2,
SUBSET_1, MATRIX_1, FINSEQ_1, TREES_1, INCSP_1, MATRIX11,
RELAT_1, FUNCT_1, FUNCSDOM, XXREAL_0, CARD_1, ARYTM_3, FINSEQ_2,
STRUCT_0, ALGSTR_0, MESFUNC1, ZFMISC_1, GROUP_1, SUPINF_2,
FVSUM_1, CARD_3, RVSUM_1, MATRIX_6, ARYTM_1, QC_LANG1, MATRIX12;
notations XBOOLE_0, MATRIX_0, XXREAL_0, MATRIX11, TARSKI, ORDINAL1,
NUMBERS, FUNCT_1, FINSEQ_1, ZFMISC_1, BINOP_1, STRUCT_0,
ALGSTR_0, GROUP_1, VECTSP_2, VECTSP_1, FVSUM_1, FINSEQ_2, MATRIX_1,
MATRIX_3, MATRIX_6;
constructors STRUCT_0, ALGSTR_0, VECTSP_2, VECTSP_1, XBOOLE_0,
MATRIX_0, FINSEQ_4, MATRIX_6, MATRIX11, CAT_2, ALGSTR_1,
FVSUM_1, RELSET_1, MATRIX_1, MATRIX_3, XXREAL_0;
registrations XBOOLE_0, RELSET_1, STRUCT_0, ALGSTR_0, FVSUM_1,
VECTSP_1, VECTSP_2, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_2,
MATRIX_6, MATRIX_0;
requirements NUMERALS, REAL, SUBSET;
equalities FINSEQ_1, MATRIX_0, FVSUM_1, ALGSTR_0;
expansions FINSEQ_1;
theorems STRUCT_0, ALGSTR_0, MATRIX_6, MATRIX11, FINSEQ_1, FINSEQ_2,
FVSUM_1, MATRIX_0, FINSEQOP, ZFMISC_1, FUNCOP_1, RLVECT_1,
GROUP_1, MATRIX_3, MATRIX_4, MATRIXR1, VECTSP_1, VECTSP_2,
CARD_1;
begin
reserve
j, k, l, n, m, t,i for Nat,
K for comRing, ::Field,
a for Element of K,
M,M1,M2 for Matrix of n,m,K,
pK,qK for FinSequence of K,
A for Matrix of n,K;
Lm1: for K being non empty set,M,M1,M2 being Matrix
of n,m,K,pK,qK being FinSequence of K,i,j st i in Seg n & j in Seg
width M & pK=Line(M,l) & qK=Line(M,k) & M1=RLine(M,k,pK) &
M2=RLine(M1,l,qK) holds (i = l implies M2*( i,j) = M*(k,j)) & (i = k
implies M2*(i,j) = M*(l,j)) & (i <> l & i <> k implies M2*(i,j) =
M*(i,j))
proof
let K be non empty set;
let M,M1,M2 be Matrix of n,m,K;
let pK,qK be FinSequence of K;
let i,j;
assume that
A1: i in Seg n and
A2: j in Seg width M and
A3: pK=Line(M,l) and
A4: qK=Line(M,k) and
A5: M1=RLine(M,k,pK) and
A6: M2=RLine(M1,l,qK);
thus i = l implies M2*(i,j) = M*(k,j)
proof
assume
A7: i = l;
len pK = width M by A3,MATRIX_0:def 7;
then
A8: width M1 = width M by A5,MATRIX11:def 3;
A9: len qK = width M by A4,MATRIX_0:def 7;
then width M1 = width M2 by A6,A8,MATRIX11:def 3;
hence M2*(i,j) = Line(M2,i).j by A2,A8,MATRIX_0:def 7
.= qK.j by A1,A6,A7,A9,A8,MATRIX11:28
.= M*(k,j) by A2,A4,MATRIX_0:def 7;
end;
thus i = k implies M2*(i,j) = M*(l,j)
proof
assume
A10: i = k;
A11: len pK = width M by A3,MATRIX_0:def 7;
then
A12: width M1 = width M by A5,MATRIX11:def 3;
A13: i=k implies Line(M2,i) = Line(M1,i)
proof
assume
A14: i=k;
per cases;
suppose
l<>k;
hence thesis by A1,A6,A14,MATRIX11:28;
end;
suppose
l=k;
then Line(M2,i) = pK by A1,A3,A4,A6,A10,A11,A12,MATRIX11:28;
hence thesis by A1,A5,A10,A11,MATRIX11:28;
end;
end;
len qK = width M by A4,MATRIX_0:def 7;
then width M1 = width M2 by A6,A12,MATRIX11:def 3;
hence M2*(i,j) = Line(M2,i).j by A2,A12,MATRIX_0:def 7
.= pK.j by A1,A5,A10,A11,A13,MATRIX11:28
.= M*(l,j) by A2,A3,MATRIX_0:def 7;
end;
thus i <> l & i <> k implies M2*(i,j) = M*(i,j)
proof
assume that
A15: i <> l and
A16: i <> k;
A17: Line(M1,i) = Line(M,i) by A1,A5,A16,MATRIX11:28;
len pK = width M by A3,MATRIX_0:def 7;
then
A18: width M1 = width M by A5,MATRIX11:def 3;
len qK = len Line(M,k) by A4
.= width M by MATRIX_0:def 7;
then width M1 = width M2 by A6,A18,MATRIX11:def 3;
hence M2*(i,j) = Line(M2,i).j by A2,A18,MATRIX_0:def 7
.= Line(M,i).j by A1,A6,A15,A17,MATRIX11:28
.= M*(i,j) by A2,MATRIX_0:def 7;
end;
end;
definition
let n,m;
let K be non empty 1-sorted;
let M be Matrix of n,m,K;
let l,k be Nat;
func InterchangeLine(M,l,k) -> Matrix of n,m,K means
:Def1:
len it = len M &
for i,j st i in dom M & j in Seg width M holds (i = l implies it*(i,j) = M*(k,j
)) & (i = k implies it*(i,j) = M*(l,j)) & (i <> l & i <> k implies it*(i,j) = M
*(i,j));
existence
proof
set M1=RLine(M,k,Line(M,l));
set M2=RLine(M1,l,Line(M,k));
take M2;
len M = n by MATRIX_0:25;
then
A1: len Line(M,k) = width M & dom M = Seg n by FINSEQ_1:def 3,MATRIX_0:def 7;
len Line(M,l) = width M by MATRIX_0:def 7;
then len M1 = len M & width M1 = width M by MATRIX11:def 3;
hence thesis by A1,Lm1,MATRIX11:def 3;
end;
uniqueness
proof
let M1,M2 be Matrix of n,m,K;
assume that
len M1 = len M and
A2: for i,j st i in dom M & j in Seg width M holds (i = l implies M1*(
i,j) = M*(k,j)) & (i = k implies M1*(i,j) = M*(l,j)) & (i <> l & i <> k implies
M1*(i,j) = M*(i,j)) and
len M2 = len M and
A3: for i,j st i in dom M & j in Seg width M holds (i = l implies M2*(
i,j) = M*(k,j)) & (i = k implies M2*(i,j) = M*(l,j)) & (i <> l & i <> k implies
M2*(i,j) = M*(i,j));
for i,j st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
A4: Indices M = Indices M1 by MATRIX_0:26;
let i,j;
assume [i,j] in Indices M1;
then
A5: i in dom M & j in Seg width M by A4,ZFMISC_1:87;
then
A6: i = k implies M1*(i,j) = M*(l,j) by A2;
A7: i = l implies M2*(i,j) = M*(k,j) by A3,A5;
A8: i <> l & i <> k implies M1*(i,j) = M*(i,j) by A2,A5;
A9: i = k implies M2*(i,j) = M*(l,j) by A3,A5;
i = l implies M1*(i,j) = M*(k,j) by A2,A5;
hence thesis by A3,A5,A6,A8,A7,A9;
end;
hence thesis by MATRIX_0:27;
end;
end;
theorem Th1:
for K being non empty set
for M1,M2 being Matrix of n,m,K holds width M1 = width M2
proof
let K be non empty set;
let M1,M2 be Matrix of n,m,K;
per cases;
suppose
A1: n > 0;
then width M1 = m by MATRIX_0:23;
hence thesis by A1,MATRIX_0:23;
end;
suppose
A2: n=0;
then width M1 = 0 by MATRIX_0:22;
hence thesis by A2,MATRIX_0:22;
end;
end;
theorem Th2:
for M,M1,i st l in dom M & k in dom M & i in dom M & M1 =
InterchangeLine(M,l,k) holds (i = l implies Line(M1,i) = Line(M,k)) & (i = k
implies Line(M1,i) = Line(M,l)) & (i <> l & i <> k implies Line(M1,i) = Line(M,
i))
proof
let M,M1,i;
assume that
A1: l in dom M and
A2: k in dom M and
A3: i in dom M and
A4: M1 = InterchangeLine(M,l,k);
thus i = l implies Line(M1,i) = Line(M,k)
proof
A5: width M1 = width M by Th1;
A6: len Line(M1,i) = width M1 by MATRIX_0:def 7;
assume
A7: i=l;
A8: now
let j be Nat such that
A9: 1 <=j & j <= len Line(M1,i);
A10: j in Seg width M1 by A6,A9;
hence Line(M1,i).j = M1*(i,j) by MATRIX_0:def 7
.= M*(k,j) by A1,A4,A7,A5,A10,Def1
.= Line(M,k).j by A5,A10,MATRIX_0:def 7;
end;
len Line(M,k) = width M by MATRIX_0:def 7;
hence thesis by A6,A8,Th1;
end;
thus i = k implies Line(M1,i) = Line(M,l)
proof
A11: width M1 = width M by Th1;
A12: len Line(M1,i) = width M1 by MATRIX_0:def 7;
assume
A13: i = k;
A14: now
let j be Nat such that
A15: 1 <=j & j <= len Line(M1,i);
A16: j in Seg width M1 by A12,A15;
hence Line(M1,i).j = M1*(i,j) by MATRIX_0:def 7
.= M*(l,j) by A2,A4,A13,A11,A16,Def1
.= Line(M,l).j by A11,A16,MATRIX_0:def 7;
end;
len Line(M,l) = width M by MATRIX_0:def 7
.= width M1 by A11
.= len Line(M1,i) by A12;
hence thesis by A14;
end;
thus i <> l & i <> k implies Line(M1,i) = Line(M,i)
proof
A17: width M1 = width M by Th1;
A18: len Line(M1,i) = width M1 by MATRIX_0:def 7;
assume
A19: i <> l & i <> k;
A20: now
let j be Nat such that
A21: 1 <=j & j <= len Line(M1,i);
A22: j in Seg width M1 by A18,A21;
hence Line(M1,i).j = M1*(i,j) by MATRIX_0:def 7
.= M*(i,j) by A3,A4,A19,A17,A22,Def1
.= Line(M,i).j by A17,A22,MATRIX_0:def 7;
end;
len Line(M,i) = width M by MATRIX_0:def 7;
hence thesis by A18,A20,Th1;
end;
end;
theorem Th3:
for K being non empty multMagma, a being Element of K, M being
Matrix of n,m,K
for i,j st i in dom M & j in Seg width M holds (a*Line(M,i)).
j = a*(M*(i,j))
proof
let K be non empty multMagma;
let a be Element of K;
let M be Matrix of n,m,K;
let i,j;
assume that
A1: i in dom M and
A2: j in Seg width M;
A3: [i,j] in Indices M by A1,A2,ZFMISC_1:87;
A4: j in Seg width (a * M) by A2,MATRIX_3:def 5;
dom M = Seg len M by FINSEQ_1:def 3;
then 1<=i & i<=len M by A1,FINSEQ_1:1;
then (a*Line(M,i)).j = (Line(a*M,i)).j by MATRIXR1:20
.= (a*M)*(i,j) by A4,MATRIX_0:def 7
.= a*(M*(i,j)) by A3,MATRIX_3:def 5;
hence thesis;
end;
Lm2: for l,i,j for K being non empty multMagma,a being Element of
K,M,M1 being Matrix of n,m,K,pK being FinSequence of K st i in Seg n &
j in Seg width M & pK= Line(M,l) & M1 =RLine(M,l,a*pK) holds (i = l
implies M1*(i,j) = a*(M*(l,j))) & (i <> l implies M1*(i,j) = M*(i,j))
proof
let l,i,j;
let K be non empty multMagma;
let a be Element of K;
let M,M1 be Matrix of n,m,K;
let pK be FinSequence of K;
assume that
A1: i in Seg n and
A2: j in Seg width M and
A3: pK= Line(M,l) and
A4: M1=RLine(M,l,a*pK);
thus i = l implies M1*(i,j) = a*(M*(l,j))
proof
assume
A5: i = l;
len M = n by MATRIX_0:def 2;
then
A6: l in dom M by A1,A5,FINSEQ_1:def 3;
A7: len (a*Line(M,l)) = width M by CARD_1:def 7;
then width M1 = width M by A3,A4,MATRIX11:def 3;
then M1*(i,j) = (Line(M1,i)).j by A2,MATRIX_0:def 7
.= (a*Line(M,l)).j by A1,A3,A4,A5,A7,MATRIX11:28
.= a*(M*(l,j)) by A2,A6,Th3;
hence thesis;
end;
assume
A8: i <> l;
len (a*Line(M,l)) = width M by CARD_1:def 7;
then width M1 = width M by A3,A4,MATRIX11:def 3;
hence M1*(i,j) = Line(M1,i).j by A2,MATRIX_0:def 7
.= Line(M,i).j by A1,A4,A8,MATRIX11:28
.= M*(i,j) by A2,MATRIX_0:def 7;
end;
definition
let n,m;
let K be non empty multMagma;
let M be Matrix of n,m,K;
let l be Nat;
let a be Element of K;
func ScalarXLine(M,l,a) -> Matrix of n,m,K means
:Def2:
len it = len M & for
i,j st i in dom M & j in Seg width M holds (i = l implies it*(i,j) = a*(M*(l,j)
)) & (i <> l implies it*(i,j) = M*(i,j));
existence
proof
set pK= Line(M,l);
set M1=RLine(M,l,a*pK);
take M1;
len M = n by MATRIX_0:25;
then
A1: dom M = Seg n by FINSEQ_1:def 3;
len pK = width M & len (a*pK) = len pK by MATRIXR1:16,MATRIX_0:def 7;
hence thesis by A1,Lm2,MATRIX11:def 3;
end;
uniqueness
proof
let M1,M2 be Matrix of n,m,K;
assume that
len M1 = len M and
A2: for i,j st i in dom M & j in Seg width M holds (i = l implies M1*(
i,j) = a*(M*(l,j))) & (i <> l implies M1*(i,j) = M*(i,j)) and
len M2 = len M and
A3: for i,j st i in dom M & j in Seg width M holds (i = l implies M2*(
i,j) = a*(M*(l,j))) & (i <> l implies M2*(i,j) = M*(i,j));
for i,j st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
A4: Indices M = Indices M1 by MATRIX_0:26;
let i,j;
assume [i,j] in Indices M1;
then
A5: i in dom M & j in Seg width M by A4,ZFMISC_1:87;
then
A6: i <> l implies M1*(i,j) = M*(i,j) by A2;
i = l implies M1*(i,j) = a*(M*(l,j)) by A2,A5;
hence thesis by A3,A5,A6;
end;
hence thesis by MATRIX_0:27;
end;
end;
theorem Th4:
l in dom M & i in dom M & M1 = ScalarXLine(M,l,a) implies (i = l
implies Line(M1,i) = a*Line(M,l)) & (i <> l implies Line(M1,i) = Line(M,i))
proof
assume that
A1: l in dom M and
A2: i in dom M and
A3: M1 = ScalarXLine(M,l,a);
thus i = l implies Line(M1,i) = a*Line(M,l)
proof
A4: width M1 = width M by Th1;
A5: len Line(M1,i) = width M1 by MATRIX_0:def 7;
assume
A6: i=l;
A7: now
let j be Nat such that
A8: 1 <=j & j <= len Line(M1,i);
A9: j in Seg width M1 by A5,A8;
hence Line(M1,i).j = M1*(i,j) by MATRIX_0:def 7
.= a*(M*(l,j)) by A1,A3,A6,A4,A9,Def2
.= (a*Line(M,l)).j by A1,A4,A9,Th3;
end;
len (a*Line(M,l)) = len Line(M,l) & len Line(M,l) = width M by MATRIXR1:16
,MATRIX_0:def 7;
hence thesis by A5,A7,Th1;
end;
A10: len Line(M1,i) = width M1 by MATRIX_0:def 7;
A11: width M1 = width M by Th1;
assume
A12: i <> l;
A13: now
let j be Nat such that
A14: 1 <=j & j <= len Line(M1,i);
A15: j in Seg width M1 by A10,A14;
hence Line(M1,i).j = M1*(i,j) by MATRIX_0:def 7
.= M*(i,j) by A2,A3,A12,A11,A15,Def2
.= Line(M,i).j by A11,A15,MATRIX_0:def 7;
end;
len Line(M,i) = width M by MATRIX_0:def 7;
hence thesis by A10,A13,Th1;
end;
Lm3: for K being non empty doubleLoopStr,a being Element of K,M,M1
being Matrix of n,m,K,pK,qK being FinSequence of K holds i in Seg n &
j in Seg width M & k in dom M & pK= Line(M,l) & qK=Line(M,k) &
M1=RLine(M,l,a*qK+pK) implies (i = l implies M1*(i,j) =
a*(M*(k,j))+(M*(l,j)) ) & (i <> l implies M1*(i,j) = M*(i,j))
proof
let K be non empty doubleLoopStr;
let a be Element of K;
let M,M1 be Matrix of n,m,K;
let pK,qK be FinSequence of K;
assume that
A1: i in Seg n and
A2: j in Seg width M and
A3: k in dom M and
A4: pK= Line(M,l) and
A5: qK=Line(M,k) and
A6: M1=RLine(M,l,a*qK+pK);
thus i = l implies M1*(i,j) = a*(M*(k,j))+(M*(l,j))
proof
(a*Line(M,k)).j = a*(M*(k,j)) by A2,A3,Th3;
then consider a1 being Element of K such that
A7: a1 = (a*Line(M,k)).j;
assume
A8: i = l;
A9: (Line(M,l)).j = M*(l,j) by A2,MATRIX_0:def 7;
then consider a2 being Element of K such that
A10: a2 = (Line(M,l)).j;
a*qK is Element of (width M)-tuples_on the carrier of K by A5,FINSEQ_2:113;
then a*qK+pK is Element of (width M)-tuples_on the carrier of K by A4,
FINSEQ_2:120;
then
A11: len (a*qK+pK) = width M by CARD_1:def 7;
then j in dom (a*qK + pK) by A2,FINSEQ_1:def 3;
then
A12: ((a*qK) + pK).j = (the addF of K).(a1,a2) by A4,A5,A7,A10,FUNCOP_1:22
.= a*(M*(k,j)) + M*(l,j) by A2,A3,A9,A7,A10,Th3;
width M1 = width M by A6,A11,MATRIX11:def 3;
then M1*(i,j) = (Line(M1,i)).j by A2,MATRIX_0:def 7
.= a*(M*(k,j)) + M*(l,j) by A1,A6,A8,A11,A12,MATRIX11:28;
hence thesis;
end;
assume
A13: i <> l;
a*qK is Element of (width M)-tuples_on the carrier of K by A5,FINSEQ_2:113;
then a*qK+pK is Element of (width M)-tuples_on the carrier of K by A4,
FINSEQ_2:120;
then len (a*qK+pK) = width M by CARD_1:def 7;
then width M1 = width M by A6,MATRIX11:def 3;
hence M1*(i,j) = Line(M1,i).j by A2,MATRIX_0:def 7
.= Line(M,i).j by A1,A6,A13,MATRIX11:28
.= M*(i,j) by A2,MATRIX_0:def 7;
end;
definition
let n,m;
let K be non empty doubleLoopStr;
let M be Matrix of n,m,K;
let l,k be Nat;
let a be Element of K;
assume
A1: k in dom M;
func RlineXScalar(M,l,k,a) -> Matrix of n,m,K means
:Def3:
len it = len M &
for i,j st i in dom M & j in Seg width M holds (i = l implies it*(i,j) = a*(M*(
k,j))+(M*(l,j))) & (i <> l implies it*(i,j) = M*(i,j));
existence
proof
set qK=Line(M,k);
set pK= Line(M,l);
set M1=RLine(M,l,a*qK+pK);
take M1;
len M = n by MATRIX_0:25;
then len (a*qK+pK) = width M & dom M = Seg n by CARD_1:def 7,FINSEQ_1:def 3
;
hence thesis by A1,Lm3,MATRIX11:def 3;
end;
uniqueness
proof
let M1,M2 be Matrix of n,m,K;
assume that
len M1 = len M and
A2: for i,j st i in dom M & j in Seg width M holds (i = l implies M1*(
i,j) = a*(M*(k,j))+(M*(l,j))) & (i <> l implies M1*(i,j) = M*(i,j)) and
len M2 = len M and
A3: for i,j st i in dom M & j in Seg width M holds (i = l implies M2*(
i,j) = a*(M*(k,j))+(M*(l,j))) & (i <> l implies M2*(i,j) = M*(i,j));
for i,j st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
A4: Indices M = Indices M1 by MATRIX_0:26;
let i,j;
assume [i,j] in Indices M1;
then
A5: i in dom M & j in Seg width M by A4,ZFMISC_1:87;
then
A6: i <> l implies M1*(i,j) = M*(i,j) by A2;
i = l implies M1*(i,j) = a*(M*(k,j))+(M*(l,j)) by A2,A5;
hence thesis by A3,A5,A6;
end;
hence thesis by MATRIX_0:27;
end;
end;
theorem Th5:
l in dom M & k in dom M & i in dom M & M1 = RlineXScalar(M,l,k,a)
implies (i = l implies Line(M1,i) = a*Line(M,k) + Line(M,l)) & (i <> l implies
Line(M1,i) = Line(M,i))
proof
assume that
A1: l in dom M and
A2: k in dom M and
A3: i in dom M and
A4: M1 = RlineXScalar(M,l,k,a);
thus i = l implies Line(M1,i) = a*Line(M,k) + Line(M,l)
proof
A5: len (a*Line(M,k)+Line(M,l)) = width M by CARD_1:def 7;
A6: len Line(M1,i) = width M1 by MATRIX_0:def 7;
A7: width M1 = width M by Th1;
assume
A8: i=l;
now
let j be Nat such that
A9: 1 <=j & j <= len Line(M1,i);
A10: j in Seg width M1 by A6,A9;
then
A11: (Line(M,l)).j = M*(l,j) by A7,MATRIX_0:def 7;
then consider a2 being Element of K such that
A12: a2 = (Line(M,l)).j;
(a*Line(M,k)).j = a*(M*(k,j)) by A2,A7,A10,Th3;
then consider a1 being Element of K such that
A13: a1 = (a*Line(M,k)).j;
j in dom (a*Line(M,k) + Line(M,l)) by A7,A5,A10,FINSEQ_1:def 3;
then
A14: ((a*Line(M,k)) + Line(M,l)).j = (the addF of K).(a1,a2) by A13,A12,
FUNCOP_1:22
.= a*(M*(k,j)) + M*(l,j) by A2,A7,A10,A11,A13,A12,Th3;
thus Line(M1,i).j = M1*(i,j) by A10,MATRIX_0:def 7
.= ((a*Line(M,k)) + Line(M,l)).j by A1,A2,A4,A8,A7,A10,A14,Def3;
end;
hence thesis by A6,A5,Th1;
end;
thus i <> l implies Line(M1,i) = Line(M,i)
proof
A15: width M1 = width M by Th1;
A16: len Line(M1,i) = width M1 by MATRIX_0:def 7;
assume
A17: i <> l;
A18: now
let j be Nat such that
A19: 1 <=j & j <= len Line(M1,i);
A20: j in Seg width M1 by A16,A19;
hence Line(M1,i).j = M1*(i,j) by MATRIX_0:def 7
.= M*(i,j) by A2,A3,A4,A17,A15,A20,Def3
.= Line(M,i).j by A15,A20,MATRIX_0:def 7;
end;
len Line(M,i) = width M by MATRIX_0:def 7;
hence thesis by A16,A18,Th1;
end;
end;
notation
let n,m;
let K be non empty 1-sorted;
let M be Matrix of n,m,K;
let l,k be Nat;
synonym ILine(M,l,k) for InterchangeLine(M,l,k);
end;
notation
let n,m;
let K be non empty multMagma;
let M be Matrix of n,m,K;
let l be Nat;
let a be Element of K;
synonym SXLine(M,l,a) for ScalarXLine(M,l,a);
end;
notation
let n,m;
let K be non empty doubleLoopStr;
let M be Matrix of n,m,K;
let l,k be Nat;
let a be Element of K;
synonym RLineXS(M,l,k,a) for RlineXScalar(M,l,k,a);
end;
theorem Th6:
l in dom (1.(K,n)) & k in dom (1.(K,n)) implies ILine((1.(K,n)),l
,k) * A = ILine(A,l,k)
proof
assume that
A1: l in dom (1.(K,n)) and
A2: k in dom (1.(K,n));
set B = ILine((1.(K,n)),l,k);
A3: len B = len (1.(K,n)) & len B=n by Def1,MATRIX_0:24;
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 B=n by MATRIX_0:24;
A7: Indices (B*A)=[:Seg n,Seg n:] by MATRIX_0:24;
A8: width A=n by MATRIX_0:24;
A9: len A=n by MATRIX_0:24;
A10: width B = width (1.(K,n)) by Th1;
A11: for j st j in Seg n & i in dom (1.(K,n)) holds (i <> l & i <> k implies
(B*A)*(i,j) = (ILine(A,l,k))*(i,j))
proof
let j;
assume that
A12: j in Seg n and
A13: i in dom (1.(K,n));
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:87;
thus i <> l & i <> k implies (B*A)*(i,j) = (ILine(A,l,k))*(i,j)
proof
A16: (Line((1.(K,n)),i)).i=1_K & for t 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:15;
let t;
assume that
A17: t in dom (Line ((1.(K,n)),i)) and
A18: t<>i;
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_0:def 7;
then [i,t] in Indices (1.(K,n)) by A13,ZFMISC_1:87;
hence thesis by A18,MATRIX_3:15;
end;
len Col(A,j) = len A by MATRIX_0:def 8;
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_0:24
.=dom A by FINSEQ_1:def 3;
len Line((1.(K,n)),i) = width (1.(K,n)) by MATRIX_0:def 7;
then
A21: i in dom (Line((1.(K,n)),i)) by A10,A6,A14,FINSEQ_1:def 3;
assume
A22: i <> l & i <> k;
[i,j] in Indices (B*A) by A7,A12,A14,ZFMISC_1:87;
then (B*A)*(i,j) = Line(B,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:17
.=A*(i,j) by A13,A20,MATRIX_0:def 8
.=(ILine(A,l,k))*(i,j) by A8,A12,A13,A22,A20,Def1;
hence thesis;
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:87;
A25: for j st j in Seg n & i in dom (1.(K,n)) holds (i = k implies (B*A)*(i,
j) = (ILine(A,l,k))*(i,j))
proof
let j;
assume that
A26: j in Seg n and
A27: i in dom (1.(K,n));
thus i = k implies (B*A)*(i,j) = (ILine(A,l,k))*(i,j)
proof
A28: (Line((1.(K,n)),l)).l=1_K & for t 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:15;
let t;
assume that
A29: t in dom (Line ((1.(K,n)),l)) and
A30: t<>l;
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_0:def 7;
then [l,t] in Indices (1.(K,n)) by A1,ZFMISC_1:87;
hence thesis by A30,MATRIX_3:15;
end;
len Line((1.(K,n)),l) = width (1.(K,n)) by MATRIX_0:def 7;
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_0:def 8;
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_0:24
.=dom A by FINSEQ_1:def 3;
assume
A34: i = k;
then [i,j] in Indices (B*A) by A5,A7,A26,ZFMISC_1:87;
then (B*A)*(i,j) = Line(B,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:17
.=A*(l,j) by A1,A33,MATRIX_0:def 8
.=(ILine(A,l,k))*(i,j) by A8,A26,A27,A34,A33,Def1;
hence thesis;
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:87;
A37: for j st j in Seg n & i in dom (1.(K,n)) holds (i = l implies (B*A)*(i,
j) = (ILine(A,l,k))*(i,j))
proof
let j;
assume that
A38: j in Seg n and
A39: i in dom (1.(K,n));
thus i = l implies (B*A)*(i,j) = (ILine(A,l,k))*(i,j)
proof
A40: (Line((1.(K,n)),k)).k=1_K & for t 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:15;
let t;
assume that
A41: t in dom (Line ((1.(K,n)),k)) and
A42: t<>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_0:def 7;
then [k,t] in Indices (1.(K,n)) by A2,ZFMISC_1:87;
hence thesis by A42,MATRIX_3:15;
end;
len Line((1.(K,n)),k) = width (1.(K,n)) by MATRIX_0:def 7;
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_0:def 8;
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_0:24
.=dom A by FINSEQ_1:def 3;
assume
A46: i = l;
then [i,j] in Indices (B*A) by A4,A7,A38,ZFMISC_1:87;
then (B*A)*(i,j) = Line(B,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:17
.=A*(k,j) by A2,A45,MATRIX_0:def 8
.=(ILine(A,l,k))*(i,j) by A8,A38,A39,A46,A45,Def1;
hence thesis;
end;
end;
A47: for i,j st [i,j] in Indices (B*A) holds (B*A)*(i,j) = (ILine(A,l,k))*(i
,j)
proof
let i,j;
assume
A48: [i,j] in Indices (B*A);
dom (1.(K,n)) = Seg len (1.(K,n)) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24;
then
A49: i in dom (1.(K,n)) by A7,A48,ZFMISC_1:87;
A50: j in Seg n by A7,A48,ZFMISC_1:87;
then i = l implies (B*A)*(i,j) = (ILine(A,l,k))*(i,j) by A37,A49;
hence thesis by A25,A11,A49,A50;
end;
A51: len (B*A) = n & width(B*A) = n by MATRIX_0:24;
len ILine(A,l,k) = len A & width ILine(A,l,k)= width A by Def1,Th1;
hence thesis by A9,A8,A51,A47,MATRIX_0:21;
end;
theorem Th7:
for l,a,A st l in dom (1.(K,n)) holds SXLine((1.(K,n)),l,a) * A =
SXLine(A,l,a)
proof
let l,a,A;
assume
A1: l in dom (1.(K,n));
set B = SXLine((1.(K,n)),l,a);
A2: len B = len (1.(K,n)) & len B=n by Def2,MATRIX_0:24;
then
A3: l in Seg n by A1,FINSEQ_1:def 3;
A4: width B=n by MATRIX_0:24;
A5: width A=n by MATRIX_0:24;
A6: len A=n by MATRIX_0:24;
A7: Indices (B*A)=[:Seg n,Seg n:] by MATRIX_0:24;
A8: width B = width (1.(K,n)) by Th1;
then
A9: l in Seg width (1.(K,n)) by A1,A2,A4,FINSEQ_1:def 3;
then
A10: [l,l] in Indices (1.(K,n)) by A1,ZFMISC_1:87;
A11: for j st j in Seg n & i in dom (1.(K,n)) holds (i = l implies (B*A)*(i,
j) = (SXLine(A,l,a))*(i,j))
proof
let j;
assume that
A12: j in Seg n and
A13: i in dom (1.(K,n));
thus i = l implies (B*A)*(i,j) = (SXLine(A,l,a))*(i,j)
proof
reconsider p=Line((1.(K,n)),l) as Element of (width A)-tuples_on the
carrier of K by Th1;
reconsider q=Col(A,j) as Element of (width A)-tuples_on the carrier of K
by A6,MATRIX_0:24;
len Line((1.(K,n)),l) = width (1.(K,n)) by MATRIX_0:def 7;
then
A14: l in dom (Line((1.(K,n)),l)) by A9,FINSEQ_1:def 3;
len Col(A,j) = len A & l in Seg n by A1,A2,FINSEQ_1:def 3,MATRIX_0:def 8;
then
A15: l in dom (Col(A,j)) by A6,FINSEQ_1:def 3;
A16: (Line((1.(K,n)),l)).l=1_K & for t 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 A10,MATRIX_3:15;
let t;
assume that
A17: t in dom (Line ((1.(K,n)),l)) and
A18: t<>l;
t in Seg len (Line ((1.(K,n)),l)) by A17,FINSEQ_1:def 3;
then t in Seg width (1.(K,n)) by MATRIX_0:def 7;
then [l,t] in Indices (1.(K,n)) by A1,ZFMISC_1:87;
hence thesis by A18,MATRIX_3:15;
end;
A19: dom (1.(K,n)) = Seg len (1.(K,n)) by FINSEQ_1:def 3
.=Seg len A by A6,MATRIX_0:24
.=dom A by FINSEQ_1:def 3;
then Col(A,j).l = A*(l,j) by A1,MATRIX_0:def 8;
then consider a1 being Element of K such that
A20: a1 = Col(A,j).l;
assume
A21: i = l;
then [i,j] in Indices (B*A) by A3,A7,A12,ZFMISC_1:87;
then (B*A)*(i,j) = Line(B,i) "*" Col(A,j) by A4,A6,MATRIX_3:def 4
.=Sum(mlt(a*p,q)) by A1,A21,Th4
.=Sum(a*mlt(p,q)) by FVSUM_1:69
.=a*Sum(mlt(Line((1.(K,n)),l),Col(A,j))) by FVSUM_1:73
.=a*a1 by A14,A15,A16,A20,MATRIX_3:17
.=a*(A*(l,j)) by A1,A19,A20,MATRIX_0:def 8
.=(SXLine(A,l,a))*(i,j) by A5,A12,A13,A21,A19,Def2;
hence thesis;
end;
end;
A22: for j st j in Seg n & i in dom (1.(K,n)) holds (i <> l implies (B*A)*(i
,j) = (SXLine(A,l,a))*(i,j))
proof
let j;
assume that
A23: j in Seg n and
A24: i in dom (1.(K,n));
A25: i in Seg n by A2,A24,FINSEQ_1:def 3;
then
A26: [i,i] in Indices (1.(K,n)) by A8,A4,A24,ZFMISC_1:87;
thus i <> l implies (B*A)*(i,j) = (SXLine(A,l,a))*(i,j)
proof
A27: (Line((1.(K,n)),i)).i=1_K & for t 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 A26,MATRIX_3:15;
let t;
assume that
A28: t in dom (Line ((1.(K,n)),i)) and
A29: t<>i;
t in Seg len (Line ((1.(K,n)),i)) by A28,FINSEQ_1:def 3;
then t in Seg width (1.(K,n)) by MATRIX_0:def 7;
then [i,t] in Indices (1.(K,n)) by A24,ZFMISC_1:87;
hence thesis by A29,MATRIX_3:15;
end;
len Col(A,j) = len A by MATRIX_0:def 8;
then
A30: i in dom Col(A,j) by A6,A25,FINSEQ_1:def 3;
A31: dom (1.(K,n)) = Seg len (1.(K,n)) by FINSEQ_1:def 3
.=Seg len A by A6,MATRIX_0:24
.=dom A by FINSEQ_1:def 3;
len Line((1.(K,n)),i) = width (1.(K,n)) by MATRIX_0:def 7;
then
A32: i in dom Line((1.(K,n)),i) by A8,A4,A25,FINSEQ_1:def 3;
assume
A33: i <> l;
[i,j] in Indices (B*A) by A7,A23,A25,ZFMISC_1:87;
then (B*A)*(i,j) = Line(B,i) "*" Col(A,j) by A4,A6,MATRIX_3:def 4
.=Sum(mlt(Line((1.(K,n)),i),Col(A,j))) by A1,A24,A33,Th4
.=Col(A,j).i by A32,A30,A27,MATRIX_3:17
.=A*(i,j) by A24,A31,MATRIX_0:def 8
.=(SXLine(A,l,a))*(i,j) by A5,A23,A24,A33,A31,Def2;
hence thesis;
end;
end;
A34: for i,j st [i,j] in Indices (B*A) holds (B*A)*(i,j) = (SXLine(A,l,a))*(
i,j)
proof
let i,j;
assume [i,j] in Indices (B*A);
then
A35: i in Seg n & j in Seg n by A7,ZFMISC_1:87;
dom (1.(K,n)) = Seg len (1.(K,n)) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24;
hence thesis by A11,A22,A35;
end;
A36: len (B*A) = n & width(B*A) = n by MATRIX_0:24;
len SXLine(A,l,a) = len A & width SXLine(A,l,a) = width A by Def2,Th1;
hence thesis by A6,A5,A36,A34,MATRIX_0:21;
end;
theorem Th8:
l in dom (1.(K,n)) & k in dom (1.(K,n)) implies RLineXS((1.(K,n))
,l,k,a) * A = RLineXS(A,l,k,a)
proof
assume that
A1: l in dom (1.(K,n)) and
A2: k in dom (1.(K,n));
set B = RLineXS((1.(K,n)),l,k,a);
A3: len B=n by MATRIX_0:24;
A4: len A=n by MATRIX_0:24;
dom (1.(K,n)) = Seg len (1.(K,n)) by FINSEQ_1:def 3
.=Seg len A by A4,MATRIX_0:24
.=dom A by FINSEQ_1:def 3;
then
A5: len RLineXS(A,l,k,a) = len A by A2,Def3;
A6: len (B*A) = n & width(B*A) = n by MATRIX_0:24;
A7: width A=n by MATRIX_0:24;
A8: len B = len (1.(K,n)) by A2,Def3;
then
A9: l in Seg n by A1,A3,FINSEQ_1:def 3;
A10: width B=n by MATRIX_0:24;
A11: width B = width (1.(K,n)) by Th1;
then
A12: l in Seg width (1.(K,n)) by A1,A8,A3,A10,FINSEQ_1:def 3;
then
A13: [l,l] in Indices (1.(K,n)) by A1,ZFMISC_1:87;
A14: Indices (B*A)=[:Seg n,Seg n:] by MATRIX_0:24;
A15: k in Seg width (1.(K,n)) by A2,A8,A11,A3,A10,FINSEQ_1:def 3;
then
A16: [k,k] in Indices (1.(K,n)) by A2,ZFMISC_1:87;
A17: for j st j in Seg n & i in dom (1.(K,n)) holds (i = l implies (B*A)*(i,
j) = (RLineXS(A,l,k,a))*(i,j))
proof
let j;
assume that
A18: j in Seg n and
i in dom (1.(K,n));
thus i = l implies (B*A)*(i,j) = (RLineXS(A,l,k,a))*(i,j)
proof
A19: (Line((1.(K,n)),l)).l=1_K & for t 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 A13,MATRIX_3:15;
let t;
assume that
A20: t in dom (Line ((1.(K,n)),l)) and
A21: t<>l;
t in Seg len (Line ((1.(K,n)),l)) by A20,FINSEQ_1:def 3;
then t in Seg width (1.(K,n)) by MATRIX_0:def 7;
then [l,t] in Indices (1.(K,n)) by A1,ZFMISC_1:87;
hence thesis by A21,MATRIX_3:15;
end;
reconsider q=Col(A,j) as Element of (width A)-tuples_on the carrier of K
by A4,MATRIX_0:24;
A22: len Col(A,j) = len A by MATRIX_0:def 8;
k in Seg n by A2,A8,A3,FINSEQ_1:def 3;
then
A23: k in dom Col(A,j) by A4,A22,FINSEQ_1:def 3;
len Line((1.(K,n)),k) = width (1.(K,n)) by MATRIX_0:def 7;
then
A24: k in dom Line((1.(K,n)),k) by A15,FINSEQ_1:def 3;
l in Seg n by A1,A8,A3,FINSEQ_1:def 3;
then
A25: l in dom (Col(A,j)) by A4,A22,FINSEQ_1:def 3;
len Line((1.(K,n)),l) = width (1.(K,n)) by MATRIX_0:def 7;
then
A26: l in dom Line((1.(K,n)),l) by A12,FINSEQ_1:def 3;
reconsider p2=Line((1.(K,n)),l) as Element of (width A)-tuples_on the
carrier of K by Th1;
A27: len q = (width A) by CARD_1:def 7;
reconsider p1=Line((1.(K,n)),k) as Element of (width A)-tuples_on the
carrier of K by Th1;
A28: len (a*p1) = width A & len p2 = (width A) by CARD_1:def 7;
A29: (Line((1.(K,n)),k)).k=1_K & for t 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 A16,MATRIX_3:15;
let t;
assume that
A30: t in dom Line ((1.(K,n)),k) and
A31: t<>k;
t in Seg len Line ((1.(K,n)),k) by A30,FINSEQ_1:def 3;
then t in Seg width (1.(K,n)) by MATRIX_0:def 7;
then [k,t] in Indices (1.(K,n)) by A2,ZFMISC_1:87;
hence thesis by A31,MATRIX_3:15;
end;
A32: dom (1.(K,n)) = Seg len (1.(K,n)) by FINSEQ_1:def 3
.=Seg len A by A4,MATRIX_0:24
.=dom A by FINSEQ_1:def 3;
then Col(A,j).k = A*(k,j) by A2,MATRIX_0:def 8;
then consider a1 being Element of K such that
A33: a1 = Col(A,j).k;
A34: Col(A,j).l = A*(l,j) by A1,A32,MATRIX_0:def 8;
then consider a2 being Element of K such that
A35: a2 = Col(A,j).l;
assume
A36: i = l;
then [i,j] in Indices (B*A) by A9,A14,A18,ZFMISC_1:87;
then (B*A)*(i,j) = Line(B,i) "*" Col(A,j) by A10,A4,MATRIX_3:def 4
.=Sum(mlt(a*p1+p2,q)) by A1,A2,A36,Th5
.=Sum(mlt(a*p1,q)+mlt(p2,q)) by A28,A27,MATRIX_4:56
.=Sum(a*mlt(p1,q)+mlt(p2,q)) by FVSUM_1:69
.=Sum(a*mlt(p1,q))+Sum(mlt(p2,q)) by FVSUM_1:76
.=a*Sum(mlt(Line((1.(K,n)),k),Col(A,j))) + Sum(mlt(Line((1.(K,n)),l)
,Col(A,j))) by FVSUM_1:73
.=a*a1 + Sum(mlt(Line((1.(K,n)),l),Col(A,j))) by A24,A23,A29,A33,
MATRIX_3:17
.=a*a1 + a2 by A26,A25,A19,A35,MATRIX_3:17
.=a*(A*(k,j))+A*(l,j) by A2,A32,A33,A34,A35,MATRIX_0:def 8
.=(RLineXS(A,l,k,a))*(i,j) by A1,A2,A7,A18,A36,A32,Def3;
hence thesis;
end;
end;
A37: for j st j in Seg n & i in dom (1.(K,n)) holds (i <> l implies (B*A)*(i
,j) = (RLineXS(A,l,k,a))*(i,j))
proof
let j;
assume that
A38: j in Seg n and
A39: i in dom (1.(K,n));
A40: i in Seg n by A8,A3,A39,FINSEQ_1:def 3;
then
A41: [i,i] in Indices (1.(K,n)) by A11,A10,A39,ZFMISC_1:87;
thus i <> l implies (B*A)*(i,j) = (RLineXS(A,l,k,a))*(i,j)
proof
A42: (Line((1.(K,n)),i)).i=1_K & for t 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 A41,MATRIX_3:15;
let t;
assume that
A43: t in dom (Line ((1.(K,n)),i)) and
A44: t<>i;
t in Seg len (Line ((1.(K,n)),i)) by A43,FINSEQ_1:def 3;
then t in Seg width (1.(K,n)) by MATRIX_0:def 7;
then [i,t] in Indices (1.(K,n)) by A39,ZFMISC_1:87;
hence thesis by A44,MATRIX_3:15;
end;
len Col(A,j) = len A by MATRIX_0:def 8;
then
A45: i in dom (Col(A,j)) by A4,A40,FINSEQ_1:def 3;
A46: dom (1.(K,n)) = Seg len (1.(K,n)) by FINSEQ_1:def 3
.=Seg len A by A4,MATRIX_0:24
.=dom A by FINSEQ_1:def 3;
len Line((1.(K,n)),i) = width (1.(K,n)) by MATRIX_0:def 7;
then
A47: i in dom Line((1.(K,n)),i) by A11,A10,A40,FINSEQ_1:def 3;
assume
A48: i <> l;
[i,j] in Indices (B*A) by A14,A38,A40,ZFMISC_1:87;
then (B*A)*(i,j) = Line(B,i) "*" Col(A,j) by A10,A4,MATRIX_3:def 4
.=Sum(mlt(Line((1.(K,n)),i),Col(A,j))) by A1,A2,A39,A48,Th5
.=Col(A,j).i by A47,A45,A42,MATRIX_3:17
.=A*(i,j) by A39,A46,MATRIX_0:def 8
.=(RLineXS(A,l,k,a))*(i,j) by A2,A7,A38,A39,A48,A46,Def3;
hence thesis;
end;
end;
A49: for i,j st [i,j] in Indices (B*A) holds (B*A)*(i,j) = (RLineXS(A,l,k,a)
)*(i,j)
proof
let i,j;
assume [i,j] in Indices (B*A);
then
A50: i in Seg n & j in Seg n by A14,ZFMISC_1:87;
dom (1.(K,n)) = Seg len (1.(K,n)) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24;
hence thesis by A17,A37,A50;
end;
width RLineXS(A,l,k,a) = width A by Th1;
hence thesis by A4,A7,A6,A5,A49,MATRIX_0:21;
end;
theorem
ILine(M,k,k) = M
proof
A1: for i,j st [i,j] in Indices M holds ILine(M,k,k)*(i,j) = M*(i,j)
proof
let i,j;
assume [i,j] in Indices M;
then
A2: i in dom M & j in Seg width M by ZFMISC_1:87;
then i = k implies ILine(M,k,k)*(i,j) = M*(k,j) by Def1;
hence thesis by A2,Def1;
end;
len ILine(M,k,k) = len M & width ILine(M,k,k) = width M by Def1,Th1;
hence thesis by A1,MATRIX_0:21;
end;
theorem
ILine(M,l,k) = ILine(M,k,l)
proof
A1: width ILine(M,k,l) = width M by Th1;
A2: for i,j st [i,j] in Indices (ILine(M,l,k)) holds ILine(M,l,k)*(i,j) =
ILine(M,k,l)*(i,j)
proof
let i,j;
A3: Indices (ILine(M,l,k)) = Indices M by MATRIX_0:26;
assume [i,j] in Indices (ILine(M,l,k));
then
A4: i in dom M & j in Seg width M by A3,ZFMISC_1:87;
then
A5: i = k implies ILine(M,l,k)*(i,j) = M*(l,j) by Def1;
A6: i = l implies ILine(M,k,l)*(i,j) = M*(k,j) by A4,Def1;
A7: i <> l & i <> k implies ILine(M,l,k)*(i,j) = M*(i,j) by A4,Def1;
A8: i = k implies ILine(M,k,l)*(i,j) = M*(l,j) by A4,Def1;
i = l implies ILine(M,l,k)*(i,j) = M*(k,j) by A4,Def1;
hence thesis by A4,A5,A7,A6,A8,Def1;
end;
len ILine(M,l,k) = len M & len ILine(M,k,l) = len M by Def1;
hence thesis by A1,A2,Th1,MATRIX_0:21;
end;
theorem Th11:
l in dom M & k in dom M implies ILine(ILine(M,l,k),l,k) = M
proof
assume
A1: l in dom M & k in dom M;
set M1 = ILine(M,l,k);
A2: dom M1 = Seg len ILine(M,l,k) by FINSEQ_1:def 3
.= Seg len M by Def1
.= dom M by FINSEQ_1:def 3;
A3: width M1 = width M by Th1;
A4: for i,j st [i,j] in Indices M holds ILine(M1,l,k)*(i,j) = M*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices M;
then
A6: j in Seg width M by ZFMISC_1:87;
A7: i in dom M by A5,ZFMISC_1:87;
then i <> l & i <> k implies ILine(M1,l,k)*(i,j) = M1*(i,j) by A3,A2,A6
,Def1;
then
A8: i <> l & i <> k implies ILine(M1,l,k)*(i,j) = M*(i,j) by A7,A6,Def1;
ILine(M1,l,k)*(l,j) = M1*(k,j) & ILine(M1,l,k)*(k,j) = M1*(l,j) by A1,A3,A2
,A6,Def1;
hence thesis by A1,A6,A8,Def1;
end;
A9: width ILine(M1,l,k) =width M1 by Th1;
len M1 =len M & len ILine(M1,l,k) =len M1 by Def1;
hence thesis by A9,A4,Th1,MATRIX_0:21;
end;
theorem Th12:
l in dom (1.(K,n)) & k in dom (1.(K,n)) implies ILine((1.(K,n)),
l,k) is invertible & (ILine((1.(K,n)),l,k))~ = ILine((1.(K,n)),l,k)
proof
assume l in dom (1.(K,n)) & k in dom (1.(K,n));
then
ILine((1.(K,n)),l,k) * ILine((1.(K,n)),l,k) = ILine(ILine((1.(K,n)),l,k)
,l,k ) & ILine(ILine((1.(K,n)),l,k),l,k) = 1.(K,n) by Th6,Th11;
then
A1: ILine((1.(K,n)),l,k) is_reverse_of ILine((1.(K,n)),l,k) by MATRIX_6:def 2;
then ILine((1.(K,n)),l,k) is invertible by MATRIX_6:def 3;
hence thesis by A1,MATRIX_6:def 4;
end;
Lm4: for i,j,l,k,a st [i,j] in Indices (1.(K,n)) & l in dom (1.(K,n)) & k in
dom (1.(K,n)) & k<>l holds (1.(K,n))*(i,j) = (RLineXS(RLineXS((1.(K,n)),l,k,-a)
,l,k,a))*(i,j)
proof
let i,j,l,k,a;
assume that
A1: [i,j] in Indices (1.(K,n)) and
A2: l in dom (1.(K,n)) and
A3: k in dom (1.(K,n)) and
A4: k<>l;
A5: i in dom (1.(K,n)) by A1,ZFMISC_1:87;
A6: j in Seg width (1.(K,n)) by A1,ZFMISC_1:87;
set B= RLineXS((1.(K,n)),l,k,-a);
A7: width B = width (1.(K,n)) & width RLineXS(B,l,k,a) = width B by Th1;
A8: dom B = Seg len B by FINSEQ_1:def 3
.= Seg len (1.(K,n)) by A3,Def3
.= dom (1.(K,n)) by FINSEQ_1:def 3;
then
A9: i in dom B by A1,ZFMISC_1:87;
now
per cases;
case
A10: i = l;
reconsider p2=Line((1.(K,n)),i) as Element of (width B)-tuples_on the
carrier of K by Th1;
reconsider p1=Line((1.(K,n)),k) as Element of (width B)-tuples_on the
carrier of K by Th1;
A11: Line(B,k) = Line((1.(K,n)),k) by A2,A3,A4,Th5;
Line(RLineXS(B,l,k,a),i) = a*Line(B,k) + Line(B,i) by A2,A3,A8,A10,Th5;
then Line(RLineXS(B,l,k,a),i) = a*p1 + ((-a)*p1 + p2) by A2,A3,A10,A11
,Th5
.= a*p1 + (-a)*p1 + p2 by FINSEQOP:28
.= (a+(-a))*p1 + p2 by FVSUM_1:55
.= (0.K)*p1 + p2 by RLVECT_1:5
.= (width B) |-> 0.K + p2 by FVSUM_1:58
.= Line((1.(K,n)),i) by FVSUM_1:21;
hence (RLineXS(B,l,k,a))*(i,j) = Line((1.(K,n)),i).j by A6,A7,
MATRIX_0:def 7
.= (1.(K,n))*(i,j) by A6,MATRIX_0:def 7;
end;
case
A12: i <> l;
then
A13: Line(RLineXS(B,l,k,a),i) = Line(B,i) by A2,A3,A8,A9,Th5;
thus (RLineXS(B,l,k,a))*(i,j) = Line(RLineXS(B,l,k,a),i).j by A6,A7,
MATRIX_0:def 7
.= Line((1.(K,n)),i).j by A2,A3,A5,A12,A13,Th5
.= (1.(K,n))*(i,j) by A6,MATRIX_0:def 7;
end;
end;
hence thesis;
end;
theorem Th13:
l in dom (1.(K,n)) & k in dom (1.(K,n)) & k<>l implies RLineXS((
1.(K,n)),l,k,a) is invertible & (RLineXS((1.(K,n)),l,k,a))~ = RLineXS((1.(K,n))
,l,k,-a)
proof
assume that
A1: l in dom (1.(K,n)) & k in dom (1.(K,n)) and
A2: k<>l;
set B = RLineXS((1.(K,n)),l,k,-a);
for i,j st [i,j] in Indices (1.(K,n)) holds (1.(K,n))*(i,j) = RLineXS(B,
l,k,a)*(i,j) by A1,A2,Lm4;
then
A3: 1.(K,n) = RLineXS(B,l,k,a) by MATRIX_0:27;
set b = -a;
set A = RLineXS((1.(K,n)),l,k,a);
a+b = 0.K by RLVECT_1:def 10;
then a = -b by RLVECT_1:6;
then
for i,j st [i,j] in Indices (1.(K,n)) holds (1.(K,n))*(i,j) = RLineXS(A,
l,k,-a)*(i,j) by A1,A2,Lm4;
then
A4: 1.(K,n) = RLineXS(A,l,k,-a) by MATRIX_0:27;
A * B = RLineXS(B,l,k,a) & B * A = RLineXS(A,l,k,-a) by A1,Th8;
then
A5: B is_reverse_of A by A3,A4,MATRIX_6:def 2;
then A is invertible by MATRIX_6:def 3;
hence thesis by A5,MATRIX_6:def 4;
end;
registration
let K be Field;
cluster non zero -> left_invertible for Element of K;
coherence
proof
let x be Element of K;
assume x is non zero;
then x <> 0.K;
hence x is left_invertible by ALGSTR_0:def 39;
end;
end;
registration
let K be Field;
cluster non zero -> right_mult-cancelable for Element of K;
coherence
proof
let x be Element of K;
assume x is non zero;
then x is left_invertible;
then consider x1 being Element of K such that
A3: x1 * x = 1.K by ALGSTR_0:def 27;
now
let y, z be Element of K;
assume A4: y * x = z * x ;
thus y = y * (1. K)
.= (z * x) * x1 by A3, A4, GROUP_1:def 3
.= z * (1. K) by A3, GROUP_1:def 3
.= z;
end;
hence thesis by ALGSTR_0:def 21;
end;
end;
theorem Th14:
a is left_invertible & a is right_mult-cancelable &
l in dom (1.(K,n)) implies SXLine((1.(K,n)),l,a) is
invertible & (SXLine((1.(K,n)),l,a))~ = SXLine((1.(K,n)),l, / a)
proof
assume that
A0: a is left_invertible & a is right_mult-cancelable and
A1: l in dom (1.(K,n));
set A = SXLine((1.(K,n)),l,a);
A3: dom A = Seg len A by FINSEQ_1:def 3
.= Seg len (1.(K,n)) by Def2
.= dom (1.(K,n)) by FINSEQ_1:def 3;
set B = SXLine((1.(K,n)),l,/ a);
A4: dom B = Seg len B by FINSEQ_1:def 3
.= Seg len (1.(K,n)) by Def2
.= dom (1.(K,n)) by FINSEQ_1:def 3;
A5: width B = width (1.(K,n)) by Th1;
for i,j st [i,j] in Indices (1.(K,n)) holds (1.(K,n))*(i,j) = SXLine(B,l
,a)*(i,j)
proof
let i,j;
assume
A6: [i,j] in Indices (1.(K,n));
then
A7: i in dom (1.(K,n)) by ZFMISC_1:87;
A8: j in Seg width (1.(K,n)) by A6,ZFMISC_1:87;
then
A9: i <> l implies B*(i,j) = (1.(K,n))*(i,j) by A7,Def2;
B*(l,j) = (/ a)*((1.(K,n))*(l,j)) by A1,A8,Def2;
then
A10: SXLine(B,l,a)*(l,j) = a*((/ a)*((1.(K,n))*(l,j))) by A1,A5,A4,A8,Def2
.= (a*(/ a))*((1.(K,n))*(l,j)) by GROUP_1:def 3
.= ((/ a)*a)*((1.(K,n))*(l,j))
.= (1_K)*((1.(K,n))*(l,j)) by A0, ALGSTR_0:def 30
.= (1.(K,n))*(l,j);
i <> l implies SXLine(B,l,a)*(i,j) = B*(i,j) by A5,A4,A7,A8,Def2;
hence thesis by A9,A10;
end;
then
A11: 1.(K,n) = SXLine(B,l,a) by MATRIX_0:27;
A12: width A = width (1.(K,n)) by Th1;
for i,j st [i,j] in Indices (1.(K,n)) holds (1.(K,n))*(i,j) = SXLine(A,
l,/ a)*(i,j)
proof
let i,j;
assume
A13: [i,j] in Indices (1.(K,n));
then
A14: i in dom (1.(K,n)) by ZFMISC_1:87;
A15: j in Seg width (1.(K,n)) by A13,ZFMISC_1:87;
then
A16: i <> l implies A*(i,j) = (1.(K,n))*(i,j) by A14,Def2;
A*(l,j) = a*((1.(K,n))*(l,j)) by A1,A15,Def2;
then
A17: SXLine(A,l,/a)*(l,j) = (/a)*(a*((1.(K,n))*(l,j))) by A1,A12,A3,A15,Def2
.= ((/a)*a)*((1.(K,n))*(l,j)) by GROUP_1:def 3
.= (1_K)*((1.(K,n))*(l,j)) by A0,ALGSTR_0:def 30
.= (1.(K,n))*(l,j);
i <> l implies SXLine(A,l,/a)*(i,j) = A*(i,j) by A12,A3,A14,A15,Def2;
hence thesis by A16,A17;
end;
then
A18: 1.(K,n) = SXLine(A,l,/a) by MATRIX_0:27;
A * B = SXLine(B,l,a) & B * A = SXLine(A,l,/a) by A1,Th7;
then
A19: B is_reverse_of A by A11,A18,MATRIX_6:def 2;
then A is invertible by MATRIX_6:def 3;
hence thesis by A19,MATRIX_6:def 4;
end;
definition
let n,m;
let K be non empty 1-sorted;
let M be Matrix of n,m,K;
let l,k be Nat;
assume that
A1: l in Seg width M and
A2: k in Seg width M and
A3: n>0 and
A4: m>0;
func InterchangeCol(M,l,k) -> Matrix of n,m,K means
:Def4:
len it = len M &
for i,j st i in dom M & j in Seg width M holds (j = l implies it*(i,j) = M*(i,k
)) & (j = k implies it*(i,j) = M*(i,l)) & (j <> l & j <> k implies it*(i,j) = M
*(i,j));
existence
proof
A5: width M = m by A3,MATRIX_0:23;
then
A6: len (M@) = m by A4,MATRIX_0:54;
A7: len M = n by A3,MATRIX_0:23;
then width (M@) = n by A4,A5,MATRIX_0:54;
then (M@) is Matrix of m,n,K by A4,A6,MATRIX_0:20;
then consider M1 being Matrix of m,n,K such that
A8: M1 = M@;
A9: width ILine(M1,l,k) = n by A4,MATRIX_0:23;
then
A10: len (ILine(M1,l,k)@) = n by A3,MATRIX_0:54;
len ILine(M1,l,k) = m by A4,MATRIX_0:23;
then width (ILine(M1,l,k)@) = m by A3,A9,MATRIX_0:54;
then (ILine(M1,l,k)@) is Matrix of n,m,K by A3,A10,MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A11: M2 = (ILine(M1,l,k))@;
take M2;
for i,j st i in dom M & j in Seg width M holds (j = l implies M2*(i,j
) = M*(i,k)) & (j = k implies M2*(i,j) = M*(i,l)) & (j <> l & j <> k implies M2
*(i,j) = M*(i,j))
proof
let i,j;
assume that
A12: i in dom M and
A13: j in Seg width M;
A14: [i,j] in Indices M by A12,A13,ZFMISC_1:87;
then
A15: [j,i] in Indices M1 by A8,MATRIX_0:def 6;
then
A16: j in dom M1 & i in Seg width M1 by ZFMISC_1:87;
dom (ILine(M1,l,k)) = Seg len ILine(M1,l,k) by FINSEQ_1:def 3
.= Seg len M1 by Def1
.= dom M1 by FINSEQ_1:def 3;
then
A17: [j,i] in Indices (ILine(M1,l,k)) by A15,Th1;
thus j = l implies M2*(i,j) = M*(i,k)
proof
A18: [i,k] in Indices M by A2,A12,ZFMISC_1:87;
assume
A19: j = l;
M2*(i,j) = (ILine(M1,l,k))*(j,i) by A11,A17,MATRIX_0:def 6
.= M1*(k,i) by A16,A19,Def1
.= M*(i,k) by A8,A18,MATRIX_0:def 6;
hence thesis;
end;
thus j = k implies M2*(i,j) = M*(i,l)
proof
A20: [i,l] in Indices M by A1,A12,ZFMISC_1:87;
assume
A21: j = k;
M2*(i,j) = (ILine(M1,l,k))*(j,i) by A11,A17,MATRIX_0:def 6
.= M1*(l,i) by A16,A21,Def1
.= M*(i,l) by A8,A20,MATRIX_0:def 6;
hence thesis;
end;
thus j <> l & j <> k implies M2*(i,j) = M*(i,j)
proof
assume
A22: j <> l & j <> k;
M2*(i,j) = (ILine(M1,l,k))*(j,i) by A11,A17,MATRIX_0:def 6
.= M1*(j,i) by A16,A22,Def1
.= M*(i,j) by A8,A14,MATRIX_0:def 6;
hence thesis;
end;
end;
hence thesis by A3,A7,MATRIX_0:23;
end;
uniqueness
proof
let M1,M2 be Matrix of n,m,K;
assume that
len M1 = len M and
A23: for i,j st i in dom M & j in Seg width M holds (j = l implies M1*
(i,j) = M*(i,k)) & (j = k implies M1*(i,j) = M*(i,l)) & (j <> l & j <> k
implies M1*(i,j) = M*(i,j)) and
len M2 = len M and
A24: for i,j st i in dom M & j in Seg width M holds (j = l implies M2*
(i,j) = M*(i,k)) & (j = k implies M2*(i,j) = M*(i,l)) & (j <> l & j <> k
implies M2*(i,j) = M*(i,j));
for i,j st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
A25: Indices M = Indices M1 by MATRIX_0:26;
let i,j;
assume [i,j] in Indices M1;
then
A26: i in dom M & j in Seg width M by A25,ZFMISC_1:87;
then
A27: j = k implies M1*(i,j) = M*(i,l) by A23;
A28: j = l implies M2*(i,j) = M*(i,k) by A24,A26;
A29: j <> l & j <> k implies M1*(i,j) = M*(i,j) by A23,A26;
A30: j = k implies M2*(i,j) = M*(i,l) by A24,A26;
j = l implies M1*(i,j) = M*(i,k) by A23,A26;
hence thesis by A24,A26,A27,A29,A28,A30;
end;
hence thesis by MATRIX_0:27;
end;
end;
definition
let n,m;
let K be non empty multMagma;
let M be Matrix of n,m,K;
let l be Nat;
let a be Element of K;
assume that
A1: l in Seg width M and
A2: n>0 and
A3: m>0;
func ScalarXCol(M,l,a) -> Matrix of n,m,K means
:Def5:
len it = len M & for
i,j st i in dom M & j in Seg width M holds (j = l implies it*(i,j) = a*(M*(i,l)
)) & (j <> l implies it*(i,j) = M*(i,j));
existence
proof
A4: width M = m by A2,MATRIX_0:23;
then
A5: len (M@) = m by A3,MATRIX_0:54;
A6: len M = n by A2,MATRIX_0:23;
then width (M@) = n by A3,A4,MATRIX_0:54;
then (M@) is Matrix of m,n,K by A3,A5,MATRIX_0:20;
then consider M1 being Matrix of m,n,K such that
A7: M1 = M@;
A8: width ScalarXLine(M1,l,a) = n by A3,MATRIX_0:23;
then
A9: len ((ScalarXLine(M1,l,a))@) = n by A2,MATRIX_0:54;
len ScalarXLine(M1,l,a) = m by A3,MATRIX_0:23;
then width ((ScalarXLine(M1,l,a))@) = m by A2,A8,MATRIX_0:54;
then ((ScalarXLine(M1,l,a))@) is Matrix of n,m,K by A2,A9,MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A10: M2 = (ScalarXLine(M1,l,a))@;
take M2;
for i,j st i in dom M & j in Seg width M holds (j = l implies M2*(i,j
) = a*(M*(i,l))) & (j <> l implies M2*(i,j) = M*(i,j))
proof
let i,j;
assume that
A11: i in dom M and
A12: j in Seg width M;
A13: [i,j] in Indices M by A11,A12,ZFMISC_1:87;
then
A14: [j,i] in Indices M1 by A7,MATRIX_0:def 6;
dom (ScalarXLine(M1,l,a)) = Seg len (ScalarXLine(M1,l,a)) by
FINSEQ_1:def 3
.= Seg len M1 by Def2
.= dom M1 by FINSEQ_1:def 3;
then
A15: [j,i] in Indices (ScalarXLine(M1,l,a)) by A14,Th1;
A16: j in dom M1 & i in Seg width M1 by A14,ZFMISC_1:87;
thus j = l implies M2*(i,j) = a*(M*(i,l))
proof
A17: [i,l] in Indices M by A1,A11,ZFMISC_1:87;
assume
A18: j = l;
M2*(i,j) = (ScalarXLine(M1,l,a))*(j,i) by A10,A15,MATRIX_0:def 6
.= a*(M1*(l,i)) by A16,A18,Def2
.= a*(M*(i,l)) by A7,A17,MATRIX_0:def 6;
hence thesis;
end;
thus j <> l implies M2*(i,j) = M*(i,j)
proof
assume
A19: j <> l;
M2*(i,j) = (ScalarXLine(M1,l,a))*(j,i) by A10,A15,MATRIX_0:def 6
.= M1*(j,i) by A16,A19,Def2
.= M*(i,j) by A7,A13,MATRIX_0:def 6;
hence thesis;
end;
end;
hence thesis by A2,A6,MATRIX_0:23;
end;
uniqueness
proof
let M1,M2 be Matrix of n,m,K;
assume that
len M1 = len M and
A20: for i,j st i in dom M & j in Seg width M holds (j = l implies M1*
(i,j) = a*(M*(i,l))) & (j <> l implies M1*(i,j) = M*(i,j)) and
len M2 = len M and
A21: for i,j st i in dom M & j in Seg width M holds (j = l implies M2*
(i,j) = a*(M*(i,l))) & (j <> l implies M2*(i,j) = M*(i,j));
for i,j st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
A22: Indices M = Indices M1 by MATRIX_0:26;
let i,j;
assume [i,j] in Indices M1;
then
A23: i in dom M & j in Seg width M by A22,ZFMISC_1:87;
then
A24: j <> l implies M1*(i,j) = M*(i,j) by A20;
j = l implies M1*(i,j) = a*(M*(i,l)) by A20,A23;
hence thesis by A21,A23,A24;
end;
hence thesis by MATRIX_0:27;
end;
end;
definition
let n,m;
let K be non empty doubleLoopStr;
let M be Matrix of n,m,K;
let l,k be Nat;
let a be Element of K;
assume that
A1: l in Seg width M and
A2: k in Seg width M and
A3: n>0 and
A4: m>0;
func RcolXScalar(M,l,k,a) -> Matrix of n,m,K means
:Def6:
len it = len M &
for i,j st i in dom M & j in Seg width M holds (j = l implies it*(i,j) = a*(M*(
i,k))+(M*(i,l))) & (j <> l implies it*(i,j) = M*(i,j));
existence
proof
A5: width M = m by A3,MATRIX_0:23;
then
A6: len (M@) = m by A4,MATRIX_0:54;
A7: len M = n by A3,MATRIX_0:23;
then width (M@) = n by A4,A5,MATRIX_0:54;
then (M@) is Matrix of m,n,K by A4,A6,MATRIX_0:20;
then consider M1 being Matrix of m,n,K such that
A8: M1 = M@;
A9: width RlineXScalar(M1,l,k,a) = n by A4,MATRIX_0:23;
then
A10: len ((RlineXScalar(M1,l,k,a))@) = n by A3,MATRIX_0:54;
len RlineXScalar(M1,l,k,a) = m by A4,MATRIX_0:23;
then width ((RlineXScalar(M1,l,k,a))@) = m by A3,A9,MATRIX_0:54;
then ((RlineXScalar(M1,l,k,a))@) is Matrix of n,m,K by A3,A10,MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A11: M2 = (RlineXScalar(M1,l,k,a))@;
take M2;
for i,j st i in dom M & j in Seg width M holds (j = l implies M2*(i,j
) = a*(M*(i,k))+(M*(i,l))) & (j <> l implies M2*(i,j) = M*(i,j))
proof
let i,j;
assume that
A12: i in dom M and
A13: j in Seg width M;
A14: [i,j] in Indices M by A12,A13,ZFMISC_1:87;
then
A15: [j,i] in Indices M1 by A8,MATRIX_0:def 6;
then
A16: i in Seg width M1 by ZFMISC_1:87;
A17: len M1 = width M by A8,MATRIX_0:def 6;
then
A18: k in dom M1 by A2,FINSEQ_1:def 3;
dom (RlineXScalar(M1,l,k,a)) = Seg len (RlineXScalar(M1,l,k,a)) by
FINSEQ_1:def 3
.= Seg len M1 by A18,Def3
.= dom M1 by FINSEQ_1:def 3;
then
A19: [j,i] in Indices (RlineXScalar(M1,l,k,a)) by A15,Th1;
A20: l in dom M1 by A1,A17,FINSEQ_1:def 3;
thus j = l implies M2*(i,j) = a*(M*(i,k))+(M*(i,l))
proof
A21: [i,k] in Indices M by A2,A12,ZFMISC_1:87;
A22: [i,l] in Indices M by A1,A12,ZFMISC_1:87;
assume
A23: j = l;
M2*(i,j) = (RlineXScalar(M1,l,k,a))*(j,i) by A11,A19,MATRIX_0:def 6
.= a*(M1*(k,i))+(M1*(l,i)) by A20,A18,A16,A23,Def3
.= a*(M*(i,k))+(M1*(l,i)) by A8,A21,MATRIX_0:def 6
.= a*(M*(i,k))+(M*(i,l)) by A8,A22,MATRIX_0:def 6;
hence thesis;
end;
A24: j in dom M1 by A15,ZFMISC_1:87;
thus j <> l implies M2*(i,j) = M*(i,j)
proof
assume
A25: j <> l;
M2*(i,j) = (RlineXScalar(M1,l,k,a))*(j,i) by A11,A19,MATRIX_0:def 6
.= M1*(j,i) by A18,A24,A16,A25,Def3
.= M*(i,j) by A8,A14,MATRIX_0:def 6;
hence thesis;
end;
end;
hence thesis by A3,A7,MATRIX_0:23;
end;
uniqueness
proof
let M1,M2 be Matrix of n,m,K;
assume that
len M1 = len M and
A26: for i,j st i in dom M & j in Seg width M holds (j = l implies M1*
(i,j) = a*(M*(i,k))+(M*(i,l))) & (j <> l implies M1*(i,j) = M*(i,j)) and
len M2 = len M and
A27: for i,j st i in dom M & j in Seg width M holds (j = l implies M2*
(i,j) = a*(M*(i,k))+(M*(i,l))) & (j <> l implies M2*(i,j) = M*(i,j));
for i,j st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
A28: Indices M = Indices M1 by MATRIX_0:26;
let i,j;
assume [i,j] in Indices M1;
then
A29: i in dom M & j in Seg width M by A28,ZFMISC_1:87;
then
A30: j <> l implies M1*(i,j) = M*(i,j) by A26;
j = l implies M1*(i,j) = a*(M*(i,k))+(M*(i,l)) by A26,A29;
hence thesis by A27,A29,A30;
end;
hence thesis by MATRIX_0:27;
end;
end;
notation
let n,m;
let K;
let M be Matrix of n,m,K;
let l,k be Nat;
synonym ICol(M,l,k) for InterchangeCol(M,l,k);
end;
notation
let n,m;
let K;
let M be Matrix of n,m,K;
let l be Nat;
let a be Element of K;
synonym SXCol(M,l,a) for ScalarXCol(M,l,a);
end;
notation
let n,m;
let K;
let M be Matrix of n,m,K;
let l,k be Nat;
let a be Element of K;
synonym RColXS(M,l,k,a) for RcolXScalar(M,l,k,a);
end;
theorem Th15:
l in Seg width M & k in Seg width M & n>0 & m>0 & M1 = M@
implies (ILine(M1,l,k))@ = ICol(M,l,k)
proof
assume that
A1: l in Seg width M and
A2: k in Seg width M and
A3: n>0 and
A4: m>0 and
A5: M1 = M@;
A6: width M = m by A3,MATRIX_0:23;
A7: width ILine(M1,l,k) = width M1 by Th1;
len M = n by A3,MATRIX_0:23;
then
A8: width (M1) = n by A4,A5,A6,MATRIX_0:54;
then
A9: len (ILine(M1,l,k)@) = n by A3,A7,MATRIX_0:54;
A10: len ILine(M1,l,k) = len M1 by Def1;
len (M1) = m by A4,A5,A6,MATRIX_0:54;
then width (ILine(M1,l,k)@) = m by A3,A8,A10,A7,MATRIX_0:54;
then
A11: (ILine(M1,l,k)@) is Matrix of n,m,K by A3,A9,MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A12: M2 = (ILine(M1,l,k))@;
A13: for i,j st i in dom M & j in Seg width M holds (j = l implies M2*(i,j)
= M*(i,k)) & (j = k implies M2*(i,j) = M*(i,l)) & (j <> l & j <> k implies M2*(
i,j) = M*(i,j))
proof
let i,j;
assume that
A14: i in dom M and
A15: j in Seg width M;
A16: [i,j] in Indices M by A14,A15,ZFMISC_1:87;
then
A17: [j,i] in Indices M1 by A5,MATRIX_0:def 6;
then
A18: j in dom M1 & i in Seg width M1 by ZFMISC_1:87;
dom (ILine(M1,l,k)) = Seg len (ILine(M1,l,k)) by FINSEQ_1:def 3
.= Seg len M1 by Def1
.= dom M1 by FINSEQ_1:def 3;
then
A19: [j,i] in Indices (ILine(M1,l,k)) by A17,Th1;
thus j = l implies M2*(i,j) = M*(i,k)
proof
A20: [i,k] in Indices M by A2,A14,ZFMISC_1:87;
assume
A21: j = l;
M2*(i,j) = (ILine(M1,l,k))*(j,i) by A12,A19,MATRIX_0:def 6
.= M1*(k,i) by A18,A21,Def1
.= M*(i,k) by A5,A20,MATRIX_0:def 6;
hence thesis;
end;
thus j = k implies M2*(i,j) = M*(i,l)
proof
A22: [i,l] in Indices M by A1,A14,ZFMISC_1:87;
assume
A23: j = k;
M2*(i,j) = (ILine(M1,l,k))*(j,i) by A12,A19,MATRIX_0:def 6
.= M1*(l,i) by A18,A23,Def1
.= M*(i,l) by A5,A22,MATRIX_0:def 6;
hence thesis;
end;
assume
A24: j <> l & j <> k;
M2*(i,j) = (ILine(M1,l,k))*(j,i) by A12,A19,MATRIX_0:def 6
.= M1*(j,i) by A18,A24,Def1
.= M*(i,j) by A5,A16,MATRIX_0:def 6;
hence thesis;
end;
for i,j st [i,j] in Indices ICol(M,l,k) holds ICol(M,l,k)*(i,j) = ((
ILine(M1,l,k))@)*(i,j)
proof
A25: Indices M = Indices ICol(M,l,k) by MATRIX_0:26;
let i,j;
assume [i,j] in Indices ICol(M,l,k);
then
A26: i in dom M & j in Seg width M by A25,ZFMISC_1:87;
then
A27: j = l implies ((ILine(M1,l,k))@)*(i,j) = M*(i,k) by A12,A13;
A28: j = k implies ICol(M,l,k)*(i,j) = M*(i,l) by A1,A3,A4,A26,Def4;
A29: j = k implies ((ILine(M1,l,k))@)*(i,j) = M*(i,l) by A12,A13,A26;
A30: j <> l & j <> k implies ((ILine(M1,l,k))@)*(i,j) = M*(i,j) by A12,A13,A26;
j = l implies ICol(M,l,k)*(i,j) = M*(i,k) by A2,A3,A4,A26,Def4;
hence thesis by A1,A2,A3,A4,A26,A27,A29,A30,A28,Def4;
end;
hence thesis by A11,MATRIX_0:27;
end;
theorem Th16:
l in Seg width M & n>0 & m>0 & M1 = M@ implies (SXLine(M1,l,a))@
= SXCol(M,l,a)
proof
assume that
A1: l in Seg width M and
A2: n>0 and
A3: m>0 and
A4: M1 = M@;
A5: width M = m by A2,MATRIX_0:23;
A6: width SXLine(M1,l,a) = width M1 by Th1;
len M = n by A2,MATRIX_0:23;
then
A7: width (M1) = n by A3,A4,A5,MATRIX_0:54;
then
A8: len (SXLine(M1,l,a)@) = n by A2,A6,MATRIX_0:54;
A9: len SXLine(M1,l,a) = len M1 by Def2;
len (M1) = m by A3,A4,A5,MATRIX_0:54;
then width (SXLine(M1,l,a)@) = m by A2,A7,A9,A6,MATRIX_0:54;
then
A10: (SXLine(M1,l,a)@) is Matrix of n,m,K by A2,A8,MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A11: M2 = (SXLine(M1,l,a))@;
A12: for i,j st i in dom M & j in Seg width M holds (j = l implies M2*(i,j)
= a*(M*(i,l))) & (j <> l implies M2*(i,j) = M*(i,j))
proof
let i,j;
assume i in dom M & j in Seg width M;
then
A13: [i,j] in Indices M by ZFMISC_1:87;
then
A14: [j,i] in Indices M1 by A4,MATRIX_0:def 6;
then
A15: j in dom M1 & i in Seg width M1 by ZFMISC_1:87;
dom (SXLine(M1,l,a)) = Seg len SXLine(M1,l,a) by FINSEQ_1:def 3
.= Seg len M1 by Def2
.= dom M1 by FINSEQ_1:def 3;
then
A16: [j,i] in Indices (SXLine(M1,l,a)) by A14,Th1;
thus j = l implies M2*(i,j) = a*(M*(i,l))
proof
assume
A17: j = l;
M2*(i,j) = (SXLine(M1,l,a))*(j,i) by A11,A16,MATRIX_0:def 6
.= a*(M1*(l,i)) by A15,A17,Def2
.= a*(M*(i,l)) by A4,A13,A17,MATRIX_0:def 6;
hence thesis;
end;
assume
A18: j <> l;
M2*(i,j) = (SXLine(M1,l,a))*(j,i) by A11,A16,MATRIX_0:def 6
.= M1*(j,i) by A15,A18,Def2
.= M*(i,j) by A4,A13,MATRIX_0:def 6;
hence thesis;
end;
for i,j st [i,j] in Indices SXCol(M,l,a) holds SXCol(M,l,a)*(i,j) = ((
SXLine(M1,l,a))@)*(i,j)
proof
A19: Indices M = Indices SXCol(M,l,a) by MATRIX_0:26;
let i,j;
assume [i,j] in Indices SXCol(M,l,a);
then
A20: i in dom M & j in Seg width M by A19,ZFMISC_1:87;
then
A21: j = l implies ((SXLine(M1,l,a))@)*(i,j) = a*(M*(i,l)) by A11,A12;
A22: j <> l implies ((SXLine(M1,l,a))@)*(i,j) = M*(i,j) by A11,A12,A20;
j = l implies SXCol(M,l,a)*(i,j) = a*(M*(i,l)) by A2,A3,A20,Def5;
hence thesis by A1,A2,A3,A20,A21,A22,Def5;
end;
hence thesis by A10,MATRIX_0:27;
end;
theorem Th17:
l in Seg width M & k in Seg width M & n>0 & m>0 & M1 = M@
implies (RLineXS(M1,l,k,a))@ = RColXS(M,l,k,a)
proof
assume that
A1: l in Seg width M and
A2: k in Seg width M and
A3: n>0 and
A4: m>0 and
A5: M1 = M@;
A6: width M = m by A3,MATRIX_0:23;
then
A7: len M1 = m by A4,A5,MATRIX_0:54;
A8: width RLineXS(M1,l,k,a) = width M1 by Th1;
len M = n by A3,MATRIX_0:23;
then
A9: width M1 = n by A4,A5,A6,MATRIX_0:54;
then
A10: len (RLineXS(M1,l,k,a)@) = n by A3,A8,MATRIX_0:54;
A11: dom M1 = Seg len M1 by FINSEQ_1:def 3
.= Seg width M by A4,A5,A6,MATRIX_0:54;
then len RLineXS(M1,l,k,a) = len M1 by A2,Def3;
then width (RLineXS(M1,l,k,a)@) = m by A3,A7,A9,A8,MATRIX_0:54;
then
A12: (RLineXS(M1,l,k,a)@) is Matrix of n,m,K by A3,A10,MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A13: M2 = (RLineXS(M1,l,k,a))@;
A14: for i,j st i in dom M & j in Seg width M holds (j = l implies M2*(i,j)
= a*(M*(i,k))+(M*(i,l))) & (j <> l implies M2*(i,j) = M*(i,j))
proof
let i,j;
assume that
A15: i in dom M and
A16: j in Seg width M;
A17: [i,j] in Indices M by A15,A16,ZFMISC_1:87;
then
A18: [j,i] in Indices M1 by A5,MATRIX_0:def 6;
then
A19: i in Seg width M1 by ZFMISC_1:87;
A20: len M1 = width M by A5,MATRIX_0:def 6;
then
A21: k in dom M1 by A2,FINSEQ_1:def 3;
dom (RLineXS(M1,l,k,a)) = Seg len (RLineXS(M1,l,k,a)) by FINSEQ_1:def 3
.= Seg len M1 by A2,A11,Def3
.= dom M1 by FINSEQ_1:def 3;
then
A22: [j,i] in Indices (RLineXS(M1,l,k,a)) by A18,Th1;
A23: l in dom M1 by A1,A20,FINSEQ_1:def 3;
thus j = l implies M2*(i,j) = a*(M*(i,k))+(M*(i,l))
proof
A24: [i,k] in Indices M by A2,A15,ZFMISC_1:87;
assume
A25: j = l;
M2*(i,j) = (RLineXS(M1,l,k,a))*(j,i) by A13,A22,MATRIX_0:def 6
.= a*(M1*(k,i))+(M1*(l,i)) by A23,A21,A19,A25,Def3
.= a*(M*(i,k))+(M1*(l,i)) by A5,A24,MATRIX_0:def 6
.= a*(M*(i,k))+(M*(i,l)) by A5,A17,A25,MATRIX_0:def 6;
hence thesis;
end;
A26: j in dom M1 by A18,ZFMISC_1:87;
thus j <> l implies M2*(i,j) = M*(i,j)
proof
assume
A27: j <> l;
M2*(i,j) = (RLineXS(M1,l,k,a))*(j,i) by A13,A22,MATRIX_0:def 6
.= M1*(j,i) by A21,A26,A19,A27,Def3
.= M*(i,j) by A5,A17,MATRIX_0:def 6;
hence thesis;
end;
end;
for i,j st [i,j] in Indices RColXS(M,l,k,a) holds RColXS(M,l,k,a)*(i,j)
= ((RLineXS(M1,l,k,a))@)*(i,j)
proof
A28: Indices M = Indices RColXS(M,l,k,a) by MATRIX_0:26;
let i,j;
assume [i,j] in Indices RColXS(M,l,k,a);
then
A29: i in dom M & j in Seg width M by A28,ZFMISC_1:87;
then
A30: j = l implies ((RLineXS(M1,l,k,a))@)*(i,j) = a*(M*(i,k))+(M*(i,l)) by A13
,A14;
A31: j <> l implies ((RLineXS(M1,l,k,a))@)*(i,j) = M*(i,j) by A13,A14,A29;
j = l implies RColXS(M,l,k,a)*(i,j) = a*(M*(i,k))+(M*(i,l)) by A2,A3,A4,A29
,Def6;
hence thesis by A1,A2,A3,A4,A29,A30,A31,Def6;
end;
hence thesis by A12,MATRIX_0:27;
end;
theorem
l in dom (1.(K,n)) & k in dom (1.(K,n)) & n>0 implies A * ICol((1.(K,n
)),l,k) = ICol(A,l,k)
proof
assume that
A1: l in dom (1.(K,n)) & k in dom (1.(K,n)) and
A2: n>0;
A3: len (1.(K,n)) = n by MATRIX_0:24;
A4: width (1.(K,n)) = n by MATRIX_0:24;
then
A5: dom (1.(K,n)) = Seg width (1.(K,n)) by A3,FINSEQ_1:def 3;
A6: width (A@)=n by MATRIX_0:24;
A7: width (ILine((1.(K,n)),l,k)) = width (1.(K,n)) & len (A@)=n by Th1,
MATRIX_0:24;
A8: len A=n by MATRIX_0:24;
A9: width A=n by MATRIX_0:24;
then
A10: Seg width A = dom (1.(K,n)) by A3,FINSEQ_1:def 3;
(ILine(A@,l,k))@ = (ILine((1.(K,n)),l,k) * (A@))@ by A1,Th6
.= (A@)@ * (ILine((1.(K,n)),l,k))@ by A2,A4,A7,A6,MATRIX_3:22
.= A* (ILine((1.(K,n)),l,k))@ by A2,A8,A9,MATRIX_0:57
.= A* (ILine((1.(K,n))@,l,k))@ by MATRIX_6:10
.= A* ICol((1.(K,n)),l,k) by A1,A2,A5,Th15;
hence thesis by A1,A2,A10,Th15;
end;
theorem
l in dom (1.(K,n)) & n>0 implies A * SXCol((1.(K,n)),l,a) = SXCol(A,l, a)
proof
assume that
A1: l in dom (1.(K,n)) and
A2: n>0;
A3: len (1.(K,n)) = n by MATRIX_0:24;
A4: width (1.(K,n)) = n by MATRIX_0:24;
then
A5: dom (1.(K,n)) = Seg width (1.(K,n)) by A3,FINSEQ_1:def 3;
A6: width (A@)=n by MATRIX_0:24;
A7: width (SXLine((1.(K,n)),l,a)) = width (1.(K,n)) & len (A@)=n by Th1,
MATRIX_0:24;
A8: len A=n by MATRIX_0:24;
A9: width A=n by MATRIX_0:24;
then
A10: Seg width A = dom (1.(K,n)) by A3,FINSEQ_1:def 3;
(SXLine(A@,l,a))@ = (SXLine((1.(K,n)),l,a) * (A@))@ by A1,Th7
.= (A@)@ * (SXLine((1.(K,n)),l,a))@ by A2,A4,A7,A6,MATRIX_3:22
.= A* (SXLine((1.(K,n)),l,a))@ by A2,A8,A9,MATRIX_0:57
.= A* (SXLine((1.(K,n))@,l,a))@ by MATRIX_6:10
.= A* SXCol((1.(K,n)),l,a) by A1,A2,A5,Th16;
hence thesis by A1,A2,A10,Th16;
end;
theorem
l in dom (1.(K,n)) & k in dom (1.(K,n)) & n>0 implies A * RColXS((1.(K
,n)),l,k,a) = RColXS(A,l,k,a)
proof
assume that
A1: l in dom (1.(K,n)) & k in dom (1.(K,n)) and
A2: n>0;
A3: len (1.(K,n)) = n by MATRIX_0:24;
A4: width (1.(K,n)) = n by MATRIX_0:24;
then
A5: dom (1.(K,n)) = Seg width (1.(K,n)) by A3,FINSEQ_1:def 3;
A6: width (A@)=n by MATRIX_0:24;
A7: width (RLineXS((1.(K,n)),l,k,a)) = width (1.(K,n)) & len (A@)=n by Th1,
MATRIX_0:24;
A8: len A=n by MATRIX_0:24;
A9: width A=n by MATRIX_0:24;
then
A10: Seg width A = dom (1.(K,n)) by A3,FINSEQ_1:def 3;
(RLineXS(A@,l,k,a))@ = (RLineXS((1.(K,n)),l,k,a) * (A@))@ by A1,Th8
.= (A@)@ * (RLineXS((1.(K,n)),l,k,a))@ by A2,A4,A7,A6,MATRIX_3:22
.= A* (RLineXS((1.(K,n)),l,k,a))@ by A2,A8,A9,MATRIX_0:57
.= A* (RLineXS((1.(K,n))@,l,k,a))@ by MATRIX_6:10
.= A* RColXS((1.(K,n)),l,k,a) by A1,A2,A5,Th17;
hence thesis by A1,A2,A10,Th17;
end;
theorem
l in dom (1.(K,n)) & k in dom (1.(K,n)) & n>0 implies (ICol((1.(K,n)),
l,k))~ = ICol((1.(K,n)),l,k)
proof
assume that
A1: l in dom (1.(K,n)) & k in dom (1.(K,n)) and
A2: n>0;
A3: (ILine((1.(K,n)),l,k))~ = ILine((1.(K,n)),l,k) by A1,Th12;
a2: ILine((1.(K,n)),l,k) is invertible by A1,Th12;
len (1.(K,n)) = n & width (1.(K,n)) = n by MATRIX_0:24;
then
A4: dom (1.(K,n)) = Seg width (1.(K,n)) by FINSEQ_1:def 3;
(1.(K,n))@ = 1.(K,n) by MATRIX_6:10;
then ICol((1.(K,n)),l,k) = (ILine((1.(K,n)),l,k))@ by A1,A2,A4,Th15
.= (ILine((1.(K,n)),l,k)@)~ by A3,MATRIX_6:13,a2
.= (ILine((1.(K,n))@,l,k)@)~ by MATRIX_6:10
.= (ICol((1.(K,n)),l,k))~ by A1,A2,A4,Th15;
hence thesis;
end;
theorem
l in dom (1.(K,n)) & k in dom (1.(K,n)) & k<>l & n>0 implies (RColXS((
1.(K,n)),l,k,a))~ = RColXS((1.(K,n)),l,k,-a)
proof
assume that
A1: l in dom (1.(K,n)) & k in dom (1.(K,n)) and
A2: k<>l and
A3: n>0;
A4: (RLineXS((1.(K,n)),l,k,a))~ = RLineXS((1.(K,n)),l,k,-a) by A1,A2,Th13;
a3: RLineXS((1.(K,n)),l,k,a) is invertible by A1,Th13,A2;
len (1.(K,n)) = n & width (1.(K,n)) = n by MATRIX_0:24;
then
A5: dom (1.(K,n)) = Seg width (1.(K,n)) by FINSEQ_1:def 3;
(1.(K,n))@ = (1.(K,n)) by MATRIX_6:10;
then RColXS((1.(K,n)),l,k,-a) = (RLineXS((1.(K,n)),l,k,-a))@ by A1,A3,A5,Th17
.= (RLineXS((1.(K,n)),l,k,a)@)~ by A4,MATRIX_6:13,a3
.= (RLineXS((1.(K,n))@,l,k,a)@)~ by MATRIX_6:10
.= (RColXS((1.(K,n)),l,k,a))~ by A1,A3,A5,Th17;
hence thesis;
end;
theorem
a is left_invertible & a is right_mult-cancelable &
l in dom (1.(K,n)) & n>0 implies (SXCol((1.(K,n)),l,a))~ =
SXCol((1.(K,n)),l,/a)
proof
assume that
A0: a is left_invertible & a is right_mult-cancelable and
A1: l in dom (1.(K,n)) and
A3: n>0;
A4: (SXLine((1.(K,n)),l,a))~ = SXLine((1.(K,n)),l,/a) by A0,A1,Th14;
a3: SXLine((1.(K,n)),l,a) is invertible by A0,A1,Th14;
len (1.(K,n)) = n & width (1.(K,n)) = n by MATRIX_0:24;
then
A5: dom (1.(K,n)) = Seg width (1.(K,n)) by FINSEQ_1:def 3;
(1.(K,n))@ = (1.(K,n)) by MATRIX_6:10;
then SXCol((1.(K,n)),l,/a) = (SXLine((1.(K,n)),l,/a))@ by A1,A3,A5,Th16
.= (SXLine((1.(K,n)),l,a)@)~ by A4,MATRIX_6:13,a3
.= (SXLine((1.(K,n))@,l,a)@)~ by MATRIX_6:10
.= (SXCol((1.(K,n)),l,a))~ by A1,A3,A5,Th16;
hence thesis;
end;