:: MATRIX12 semantic presentation begin Lm1: for m, n being Nat for K being Field for k, l being Nat for M, M1, M2 being Matrix of n,m,K for pK, qK being FinSequence of K for i, j being Nat 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 m, n be Nat; ::_thesis: for K being Field for k, l being Nat for M, M1, M2 being Matrix of n,m,K for pK, qK being FinSequence of K for i, j being Nat 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) ) ) let K be Field; ::_thesis: for k, l being Nat for M, M1, M2 being Matrix of n,m,K for pK, qK being FinSequence of K for i, j being Nat 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) ) ) let k, l be Nat; ::_thesis: for M, M1, M2 being Matrix of n,m,K for pK, qK being FinSequence of K for i, j being Nat 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) ) ) let M, M1, M2 be Matrix of n,m,K; ::_thesis: for pK, qK being FinSequence of K for i, j being Nat 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) ) ) let pK, qK be FinSequence of K; ::_thesis: for i, j being Nat 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) ) ) let i, j be Nat; ::_thesis: ( 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) implies ( ( 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) ) ) ) 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) ; ::_thesis: ( ( 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) ) ) thus ( i = l implies M2 * (i,j) = M * (k,j) ) ::_thesis: ( ( i = k implies M2 * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies M2 * (i,j) = M * (i,j) ) ) proof assume A7: i = l ; ::_thesis: M2 * (i,j) = M * (k,j) len pK = width M by A3, MATRIX_1:def_7; then A8: width M1 = width M by A5, MATRIX11:def_3; A9: len qK = width M by A4, MATRIX_1: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_1:def_7 .= qK . j by A1, A6, A7, A9, A8, MATRIX11:28 .= M * (k,j) by A2, A4, MATRIX_1:def_7 ; ::_thesis: verum end; thus ( i = k implies M2 * (i,j) = M * (l,j) ) ::_thesis: ( i <> l & i <> k implies M2 * (i,j) = M * (i,j) ) proof assume A10: i = k ; ::_thesis: M2 * (i,j) = M * (l,j) A11: len pK = width M by A3, MATRIX_1: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 ; ::_thesis: Line (M2,i) = Line (M1,i) percases ( l <> k or l = k ) ; suppose l <> k ; ::_thesis: Line (M2,i) = Line (M1,i) hence Line (M2,i) = Line (M1,i) by A1, A6, A14, MATRIX11:28; ::_thesis: verum end; suppose l = k ; ::_thesis: Line (M2,i) = Line (M1,i) then Line (M2,i) = pK by A1, A3, A4, A6, A10, A11, A12, MATRIX11:28; hence Line (M2,i) = Line (M1,i) by A1, A5, A10, A11, MATRIX11:28; ::_thesis: verum end; end; end; len qK = width M by A4, MATRIX_1: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_1:def_7 .= pK . j by A1, A5, A10, A11, A13, MATRIX11:28 .= M * (l,j) by A2, A3, MATRIX_1:def_7 ; ::_thesis: verum end; thus ( i <> l & i <> k implies M2 * (i,j) = M * (i,j) ) ::_thesis: verum proof assume that A15: i <> l and A16: i <> k ; ::_thesis: M2 * (i,j) = M * (i,j) A17: Line (M1,i) = Line (M,i) by A1, A5, A16, MATRIX11:28; len pK = width M by A3, MATRIX_1:def_7; then A18: width M1 = width M by A5, MATRIX11:def_3; len qK = width M by A4, MATRIX_1: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_1:def_7 .= (Line (M,i)) . j by A1, A6, A15, A17, MATRIX11:28 .= M * (i,j) by A2, MATRIX_1:def_7 ; ::_thesis: verum end; end; definition let n, m be Nat; let K be Field; 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: :: MATRIX12:def 1 ( len it = len M & ( for i, j being Nat 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 ex b1 being Matrix of n,m,K st ( len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b1 * (i,j) = M * (k,j) ) & ( i = k implies b1 * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b1 * (i,j) = M * (i,j) ) ) ) ) proof set M1 = RLine (M,k,(Line (M,l))); set M2 = RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k))); take RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k))) ; ::_thesis: ( len (RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k)))) = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies (RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k)))) * (i,j) = M * (k,j) ) & ( i = k implies (RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k)))) * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies (RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k)))) * (i,j) = M * (i,j) ) ) ) ) len M = n by MATRIX_1:25; then A1: ( len (Line (M,k)) = width M & dom M = Seg n ) by FINSEQ_1:def_3, MATRIX_1:def_7; len (Line (M,l)) = width M by MATRIX_1:def_7; then ( len (RLine (M,k,(Line (M,l)))) = len M & width (RLine (M,k,(Line (M,l)))) = width M ) by MATRIX11:def_3; hence ( len (RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k)))) = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies (RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k)))) * (i,j) = M * (k,j) ) & ( i = k implies (RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k)))) * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies (RLine ((RLine (M,k,(Line (M,l)))),l,(Line (M,k)))) * (i,j) = M * (i,j) ) ) ) ) by A1, Lm1, MATRIX11:def_3; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of n,m,K st len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b1 * (i,j) = M * (k,j) ) & ( i = k implies b1 * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b1 * (i,j) = M * (i,j) ) ) ) & len b2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b2 * (i,j) = M * (k,j) ) & ( i = k implies b2 * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b2 * (i,j) = M * (i,j) ) ) ) holds b1 = b2 proof let M1, M2 be Matrix of n,m,K; ::_thesis: ( len M1 = len M & ( for i, j being Nat 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) ) ) ) & len M2 = len M & ( for i, j being Nat 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) ) ) ) implies M1 = M2 ) assume that len M1 = len M and A2: for i, j being Nat 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 being Nat 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) ) ) ; ::_thesis: M1 = M2 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = M2 * (i,j) proof A4: Indices M = Indices M1 by MATRIX_1:26; let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) 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 M1 * (i,j) = M2 * (i,j) by A3, A5, A6, A8, A7, A9; ::_thesis: verum end; hence M1 = M2 by MATRIX_1:27; ::_thesis: verum end; end; :: deftheorem Def1 defines InterchangeLine MATRIX12:def_1_:_ for n, m being Nat for K being Field for M being Matrix of n,m,K for l, k being Nat for b7 being Matrix of n,m,K holds ( b7 = InterchangeLine (M,l,k) iff ( len b7 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b7 * (i,j) = M * (k,j) ) & ( i = k implies b7 * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b7 * (i,j) = M * (i,j) ) ) ) ) ); theorem Th1: :: MATRIX12:1 for n, m being Nat for K being Field for M1, M2 being Matrix of n,m,K holds width M1 = width M2 proof let n, m be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,m,K holds width M1 = width M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,m,K holds width M1 = width M2 let M1, M2 be Matrix of n,m,K; ::_thesis: width M1 = width M2 percases ( n > 0 or n = 0 ) ; supposeA1: n > 0 ; ::_thesis: width M1 = width M2 then width M1 = m by MATRIX_1:23; hence width M1 = width M2 by A1, MATRIX_1:23; ::_thesis: verum end; supposeA2: n = 0 ; ::_thesis: width M1 = width M2 then width M1 = 0 by MATRIX_1:22; hence width M1 = width M2 by A2, MATRIX_1:22; ::_thesis: verum end; end; end; theorem Th2: :: MATRIX12:2 for m, n, l, k being Nat for K being Field for M, M1 being Matrix of n,m,K for i being Nat 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, n, l, k be Nat; ::_thesis: for K being Field for M, M1 being Matrix of n,m,K for i being Nat 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) ) ) let K be Field; ::_thesis: for M, M1 being Matrix of n,m,K for i being Nat 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) ) ) let M, M1 be Matrix of n,m,K; ::_thesis: for i being Nat 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) ) ) let i be Nat; ::_thesis: ( l in dom M & k in dom M & i in dom M & M1 = InterchangeLine (M,l,k) implies ( ( 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) ) ) ) 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) ; ::_thesis: ( ( 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) ) ) thus ( i = l implies Line (M1,i) = Line (M,k) ) ::_thesis: ( ( i = k implies Line (M1,i) = Line (M,l) ) & ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) ) proof A5: width M1 = width M by Th1; A6: len (Line (M1,i)) = width M1 by MATRIX_1:def_7; assume A7: i = l ; ::_thesis: Line (M1,i) = Line (M,k) A8: now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Line_(M1,i))_holds_ (Line_(M1,i))_._j_=_(Line_(M,k))_._j let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,k)) . j ) assume A9: ( 1 <= j & j <= len (Line (M1,i)) ) ; ::_thesis: (Line (M1,i)) . j = (Line (M,k)) . j j in NAT by ORDINAL1:def_12; then A10: j in Seg (width M1) by A6, A9; hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_1:def_7 .= M * (k,j) by A1, A4, A7, A5, A10, Def1 .= (Line (M,k)) . j by A5, A10, MATRIX_1:def_7 ; ::_thesis: verum end; len (Line (M,k)) = width M by MATRIX_1:def_7; hence Line (M1,i) = Line (M,k) by A6, A8, Th1, FINSEQ_1:14; ::_thesis: verum end; thus ( i = k implies Line (M1,i) = Line (M,l) ) ::_thesis: ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) proof A11: width M1 = width M by Th1; A12: len (Line (M1,i)) = width M1 by MATRIX_1:def_7; assume A13: i = k ; ::_thesis: Line (M1,i) = Line (M,l) A14: now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Line_(M1,i))_holds_ (Line_(M1,i))_._j_=_(Line_(M,l))_._j let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,l)) . j ) assume A15: ( 1 <= j & j <= len (Line (M1,i)) ) ; ::_thesis: (Line (M1,i)) . j = (Line (M,l)) . j j in NAT by ORDINAL1:def_12; then A16: j in Seg (width M1) by A12, A15; hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_1:def_7 .= M * (l,j) by A2, A4, A13, A11, A16, Def1 .= (Line (M,l)) . j by A11, A16, MATRIX_1:def_7 ; ::_thesis: verum end; len (Line (M,l)) = width M by MATRIX_1:def_7; hence Line (M1,i) = Line (M,l) by A12, A14, Th1, FINSEQ_1:14; ::_thesis: verum end; thus ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) ::_thesis: verum proof A17: width M1 = width M by Th1; A18: len (Line (M1,i)) = width M1 by MATRIX_1:def_7; assume A19: ( i <> l & i <> k ) ; ::_thesis: Line (M1,i) = Line (M,i) A20: now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Line_(M1,i))_holds_ (Line_(M1,i))_._j_=_(Line_(M,i))_._j let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,i)) . j ) assume A21: ( 1 <= j & j <= len (Line (M1,i)) ) ; ::_thesis: (Line (M1,i)) . j = (Line (M,i)) . j j in NAT by ORDINAL1:def_12; then A22: j in Seg (width M1) by A18, A21; hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_1:def_7 .= M * (i,j) by A3, A4, A19, A17, A22, Def1 .= (Line (M,i)) . j by A17, A22, MATRIX_1:def_7 ; ::_thesis: verum end; len (Line (M,i)) = width M by MATRIX_1:def_7; hence Line (M1,i) = Line (M,i) by A18, A20, Th1, FINSEQ_1:14; ::_thesis: verum end; end; theorem Th3: :: MATRIX12:3 for m, n being Nat for K being Field for a being Element of K for i, j being Nat for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds (a * (Line (M,i))) . j = a * (M * (i,j)) proof let m, n be Nat; ::_thesis: for K being Field for a being Element of K for i, j being Nat for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds (a * (Line (M,i))) . j = a * (M * (i,j)) let K be Field; ::_thesis: for a being Element of K for i, j being Nat for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds (a * (Line (M,i))) . j = a * (M * (i,j)) let a be Element of K; ::_thesis: for i, j being Nat for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds (a * (Line (M,i))) . j = a * (M * (i,j)) let i, j be Nat; ::_thesis: for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds (a * (Line (M,i))) . j = a * (M * (i,j)) let M be Matrix of n,m,K; ::_thesis: ( i in dom M & j in Seg (width M) implies (a * (Line (M,i))) . j = a * (M * (i,j)) ) assume that A1: i in dom M and A2: j in Seg (width M) ; ::_thesis: (a * (Line (M,i))) . j = a * (M * (i,j)) 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_1:def_7 .= a * (M * (i,j)) by A3, MATRIX_3:def_5 ; hence (a * (Line (M,i))) . j = a * (M * (i,j)) ; ::_thesis: verum end; Lm2: for m, n being Nat for K being Field for a being Element of K for l being Nat for M, M1 being Matrix of n,m,K for pK being FinSequence of K for i, j being Nat 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 m, n be Nat; ::_thesis: for K being Field for a being Element of K for l being Nat for M, M1 being Matrix of n,m,K for pK being FinSequence of K for i, j being Nat 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) ) ) let K be Field; ::_thesis: for a being Element of K for l being Nat for M, M1 being Matrix of n,m,K for pK being FinSequence of K for i, j being Nat 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) ) ) let a be Element of K; ::_thesis: for l being Nat for M, M1 being Matrix of n,m,K for pK being FinSequence of K for i, j being Nat 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) ) ) let l be Nat; ::_thesis: for M, M1 being Matrix of n,m,K for pK being FinSequence of K for i, j being Nat 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) ) ) let M, M1 be Matrix of n,m,K; ::_thesis: for pK being FinSequence of K for i, j being Nat 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) ) ) let pK be FinSequence of K; ::_thesis: for i, j being Nat 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) ) ) let i, j be Nat; ::_thesis: ( i in Seg n & j in Seg (width M) & pK = Line (M,l) & M1 = RLine (M,l,(a * pK)) implies ( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) ) 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)) ; ::_thesis: ( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) thus ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) ::_thesis: ( i <> l implies M1 * (i,j) = M * (i,j) ) proof assume A5: i = l ; ::_thesis: M1 * (i,j) = a * (M * (l,j)) len M = n by MATRIX_1: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_1:def_7 .= (a * (Line (M,l))) . j by A1, A3, A4, A5, A7, MATRIX11:28 .= a * (M * (l,j)) by A2, A6, Th3 ; hence M1 * (i,j) = a * (M * (l,j)) ; ::_thesis: verum end; assume A8: i <> l ; ::_thesis: M1 * (i,j) = M * (i,j) 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_1:def_7 .= (Line (M,i)) . j by A1, A4, A8, MATRIX11:28 .= M * (i,j) by A2, MATRIX_1:def_7 ; ::_thesis: verum end; definition let n, m be Nat; let K be Field; 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: :: MATRIX12:def 2 ( len it = len M & ( for i, j being Nat 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 ex b1 being Matrix of n,m,K st ( len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) ) proof set pK = Line (M,l); set M1 = RLine (M,l,(a * (Line (M,l)))); take RLine (M,l,(a * (Line (M,l)))) ; ::_thesis: ( len (RLine (M,l,(a * (Line (M,l))))) = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies (RLine (M,l,(a * (Line (M,l))))) * (i,j) = a * (M * (l,j)) ) & ( i <> l implies (RLine (M,l,(a * (Line (M,l))))) * (i,j) = M * (i,j) ) ) ) ) len M = n by MATRIX_1:25; then A1: dom M = Seg n by FINSEQ_1:def_3; ( len (Line (M,l)) = width M & len (a * (Line (M,l))) = len (Line (M,l)) ) by MATRIXR1:16, MATRIX_1:def_7; hence ( len (RLine (M,l,(a * (Line (M,l))))) = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies (RLine (M,l,(a * (Line (M,l))))) * (i,j) = a * (M * (l,j)) ) & ( i <> l implies (RLine (M,l,(a * (Line (M,l))))) * (i,j) = M * (i,j) ) ) ) ) by A1, Lm2, MATRIX11:def_3; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of n,m,K st len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) & len b2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b2 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds b1 = b2 proof let M1, M2 be Matrix of n,m,K; ::_thesis: ( len M1 = len M & ( for i, j being Nat 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) ) ) ) & len M2 = len M & ( for i, j being Nat 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) ) ) ) implies M1 = M2 ) assume that len M1 = len M and A2: for i, j being Nat 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 being Nat 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) ) ) ; ::_thesis: M1 = M2 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = M2 * (i,j) proof A4: Indices M = Indices M1 by MATRIX_1:26; let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) 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 M1 * (i,j) = M2 * (i,j) by A3, A5, A6; ::_thesis: verum end; hence M1 = M2 by MATRIX_1:27; ::_thesis: verum end; end; :: deftheorem Def2 defines ScalarXLine MATRIX12:def_2_:_ for n, m being Nat for K being Field for M being Matrix of n,m,K for l being Nat for a being Element of K for b7 being Matrix of n,m,K holds ( b7 = ScalarXLine (M,l,a) iff ( len b7 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b7 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b7 * (i,j) = M * (i,j) ) ) ) ) ); theorem Th4: :: MATRIX12:4 for n, m, l, i being Nat for K being Field for a being Element of K for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds ( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) proof let n, m, l, i be Nat; ::_thesis: for K being Field for a being Element of K for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds ( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) let K be Field; ::_thesis: for a being Element of K for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds ( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) let a be Element of K; ::_thesis: for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds ( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) let M, M1 be Matrix of n,m,K; ::_thesis: ( 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) ) ) ) assume that A1: l in dom M and A2: i in dom M and A3: M1 = ScalarXLine (M,l,a) ; ::_thesis: ( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) thus ( i = l implies Line (M1,i) = a * (Line (M,l)) ) ::_thesis: ( i <> l implies Line (M1,i) = Line (M,i) ) proof A4: width M1 = width M by Th1; A5: len (Line (M1,i)) = width M1 by MATRIX_1:def_7; assume A6: i = l ; ::_thesis: Line (M1,i) = a * (Line (M,l)) A7: now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Line_(M1,i))_holds_ (Line_(M1,i))_._j_=_(a_*_(Line_(M,l)))_._j let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (a * (Line (M,l))) . j ) assume A8: ( 1 <= j & j <= len (Line (M1,i)) ) ; ::_thesis: (Line (M1,i)) . j = (a * (Line (M,l))) . j j in NAT by ORDINAL1:def_12; then A9: j in Seg (width M1) by A5, A8; hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_1:def_7 .= a * (M * (l,j)) by A1, A3, A6, A4, A9, Def2 .= (a * (Line (M,l))) . j by A1, A4, A9, Th3 ; ::_thesis: verum end; ( len (a * (Line (M,l))) = len (Line (M,l)) & len (Line (M,l)) = width M ) by MATRIXR1:16, MATRIX_1:def_7; hence Line (M1,i) = a * (Line (M,l)) by A5, A7, Th1, FINSEQ_1:14; ::_thesis: verum end; A10: len (Line (M1,i)) = width M1 by MATRIX_1:def_7; A11: width M1 = width M by Th1; assume A12: i <> l ; ::_thesis: Line (M1,i) = Line (M,i) A13: now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Line_(M1,i))_holds_ (Line_(M1,i))_._j_=_(Line_(M,i))_._j let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,i)) . j ) assume A14: ( 1 <= j & j <= len (Line (M1,i)) ) ; ::_thesis: (Line (M1,i)) . j = (Line (M,i)) . j j in NAT by ORDINAL1:def_12; then A15: j in Seg (width M1) by A10, A14; hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_1:def_7 .= M * (i,j) by A2, A3, A12, A11, A15, Def2 .= (Line (M,i)) . j by A11, A15, MATRIX_1:def_7 ; ::_thesis: verum end; len (Line (M,i)) = width M by MATRIX_1:def_7; hence Line (M1,i) = Line (M,i) by A10, A13, Th1, FINSEQ_1:14; ::_thesis: verum end; Lm3: for m, i, n, j, k, l being Nat for K being Field for a being Element of K for M, M1 being Matrix of n,m,K for pK, qK being FinSequence of K st 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)) holds ( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) proof let m, i, n, j, k, l be Nat; ::_thesis: for K being Field for a being Element of K for M, M1 being Matrix of n,m,K for pK, qK being FinSequence of K st 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)) holds ( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) let K be Field; ::_thesis: for a being Element of K for M, M1 being Matrix of n,m,K for pK, qK being FinSequence of K st 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)) holds ( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) let a be Element of K; ::_thesis: for M, M1 being Matrix of n,m,K for pK, qK being FinSequence of K st 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)) holds ( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) let M, M1 be Matrix of n,m,K; ::_thesis: for pK, qK being FinSequence of K st 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)) holds ( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) let pK, qK be FinSequence of K; ::_thesis: ( 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) ) ) ) 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)) ; ::_thesis: ( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) thus ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) ::_thesis: ( i <> l implies M1 * (i,j) = M * (i,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 ; ::_thesis: M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) A9: (Line (M,l)) . j = M * (l,j) by A2, MATRIX_1: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_1:def_7 .= (a * (M * (k,j))) + (M * (l,j)) by A1, A6, A8, A11, A12, MATRIX11:28 ; hence M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ; ::_thesis: verum end; assume A13: i <> l ; ::_thesis: M1 * (i,j) = M * (i,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 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_1:def_7 .= (Line (M,i)) . j by A1, A6, A13, MATRIX11:28 .= M * (i,j) by A2, MATRIX_1:def_7 ; ::_thesis: verum end; definition let n, m be Nat; let K be Field; 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: :: MATRIX12:def 3 ( len it = len M & ( for i, j being Nat 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 ex b1 being Matrix of n,m,K st ( len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) ) proof set qK = Line (M,k); set pK = Line (M,l); set M1 = RLine (M,l,((a * (Line (M,k))) + (Line (M,l)))); take RLine (M,l,((a * (Line (M,k))) + (Line (M,l)))) ; ::_thesis: ( len (RLine (M,l,((a * (Line (M,k))) + (Line (M,l))))) = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies (RLine (M,l,((a * (Line (M,k))) + (Line (M,l))))) * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies (RLine (M,l,((a * (Line (M,k))) + (Line (M,l))))) * (i,j) = M * (i,j) ) ) ) ) len M = n by MATRIX_1:25; then ( len ((a * (Line (M,k))) + (Line (M,l))) = width M & dom M = Seg n ) by CARD_1:def_7, FINSEQ_1:def_3; hence ( len (RLine (M,l,((a * (Line (M,k))) + (Line (M,l))))) = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies (RLine (M,l,((a * (Line (M,k))) + (Line (M,l))))) * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies (RLine (M,l,((a * (Line (M,k))) + (Line (M,l))))) * (i,j) = M * (i,j) ) ) ) ) by A1, Lm3, MATRIX11:def_3; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of n,m,K st len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) & len b2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b2 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds b1 = b2 proof let M1, M2 be Matrix of n,m,K; ::_thesis: ( len M1 = len M & ( for i, j being Nat 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) ) ) ) & len M2 = len M & ( for i, j being Nat 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) ) ) ) implies M1 = M2 ) assume that len M1 = len M and A2: for i, j being Nat 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 being Nat 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) ) ) ; ::_thesis: M1 = M2 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = M2 * (i,j) proof A4: Indices M = Indices M1 by MATRIX_1:26; let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) 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 M1 * (i,j) = M2 * (i,j) by A3, A5, A6; ::_thesis: verum end; hence M1 = M2 by MATRIX_1:27; ::_thesis: verum end; end; :: deftheorem Def3 defines RlineXScalar MATRIX12:def_3_:_ for n, m being Nat for K being Field for M being Matrix of n,m,K for l, k being Nat for a being Element of K st k in dom M holds for b8 being Matrix of n,m,K holds ( b8 = RlineXScalar (M,l,k,a) iff ( len b8 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( i = l implies b8 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b8 * (i,j) = M * (i,j) ) ) ) ) ); theorem Th5: :: MATRIX12:5 for n, m, l, k, i being Nat for K being Field for a being Element of K for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) holds ( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) proof let n, m, l, k, i be Nat; ::_thesis: for K being Field for a being Element of K for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) holds ( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) let K be Field; ::_thesis: for a being Element of K for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) holds ( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) let a be Element of K; ::_thesis: for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) holds ( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) let M, M1 be Matrix of n,m,K; ::_thesis: ( 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) ) ) ) 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) ; ::_thesis: ( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) thus ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) ::_thesis: ( i <> l implies Line (M1,i) = Line (M,i) ) 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_1:def_7; A7: width M1 = width M by Th1; assume A8: i = l ; ::_thesis: Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Line_(M1,i))_holds_ (Line_(M1,i))_._j_=_((a_*_(Line_(M,k)))_+_(Line_(M,l)))_._j let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = ((a * (Line (M,k))) + (Line (M,l))) . j ) assume A9: ( 1 <= j & j <= len (Line (M1,i)) ) ; ::_thesis: (Line (M1,i)) . j = ((a * (Line (M,k))) + (Line (M,l))) . j j in NAT by ORDINAL1:def_12; then A10: j in Seg (width M1) by A6, A9; then A11: (Line (M,l)) . j = M * (l,j) by A7, MATRIX_1: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_1:def_7 .= ((a * (Line (M,k))) + (Line (M,l))) . j by A1, A2, A4, A8, A7, A10, A14, Def3 ; ::_thesis: verum end; hence Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) by A6, A5, Th1, FINSEQ_1:14; ::_thesis: verum end; thus ( i <> l implies Line (M1,i) = Line (M,i) ) ::_thesis: verum proof A15: width M1 = width M by Th1; A16: len (Line (M1,i)) = width M1 by MATRIX_1:def_7; assume A17: i <> l ; ::_thesis: Line (M1,i) = Line (M,i) A18: now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Line_(M1,i))_holds_ (Line_(M1,i))_._j_=_(Line_(M,i))_._j let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,i)) . j ) assume A19: ( 1 <= j & j <= len (Line (M1,i)) ) ; ::_thesis: (Line (M1,i)) . j = (Line (M,i)) . j j in NAT by ORDINAL1:def_12; then A20: j in Seg (width M1) by A16, A19; hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_1:def_7 .= M * (i,j) by A2, A3, A4, A17, A15, A20, Def3 .= (Line (M,i)) . j by A15, A20, MATRIX_1:def_7 ; ::_thesis: verum end; len (Line (M,i)) = width M by MATRIX_1:def_7; hence Line (M1,i) = Line (M,i) by A16, A18, Th1, FINSEQ_1:14; ::_thesis: verum end; end; notation let n, m be Nat; let K be Field; 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 be Nat; let K be Field; 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 be Nat; let K be Field; 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: :: MATRIX12:6 for l, n, k being Nat 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) proof 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: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 (ILine ((1. (K,n)),l,k)) = n by MATRIX_1:24; A7: Indices ((ILine ((1. (K,n)),l,k)) * A) = [:(Seg n),(Seg n):] by MATRIX_1:24; A8: width A = n by MATRIX_1:24; A9: len A = n by MATRIX_1:24; 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:87; 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:15; ::_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_7; then [i,t] in Indices (1. (K,n)) by A13, ZFMISC_1:87; hence (Line ((1. (K,n)),i)) . t = 0. K by A18, MATRIX_3:15; ::_thesis: verum end; len (Col (A,j)) = len A by MATRIX_1: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_1:24 .= dom A by FINSEQ_1:def_3 ; len (Line ((1. (K,n)),i)) = width (1. (K,n)) by MATRIX_1: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 ) ; ::_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:87; 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:17 .= A * (i,j) by A13, A20, MATRIX_1:def_8 .= (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:87; 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:15; ::_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_7; then [l,t] in Indices (1. (K,n)) by A1, ZFMISC_1:87; hence (Line ((1. (K,n)),l)) . t = 0. K by A30, MATRIX_3:15; ::_thesis: verum end; len (Line ((1. (K,n)),l)) = width (1. (K,n)) by MATRIX_1: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_1: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_1:24 .= 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:87; 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:17 .= A * (l,j) by A1, A33, MATRIX_1:def_8 .= (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:87; 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:15; ::_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_7; then [k,t] in Indices (1. (K,n)) by A2, ZFMISC_1:87; hence (Line ((1. (K,n)),k)) . t = 0. K by A42, MATRIX_3:15; ::_thesis: verum end; len (Line ((1. (K,n)),k)) = width (1. (K,n)) by MATRIX_1: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_1: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_1:24 .= 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:87; 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:17 .= A * (k,j) by A2, A45, MATRIX_1:def_8 .= (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: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 ((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:24; ( 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 end; theorem Th7: :: MATRIX12:7 for n being Nat for K being Field for l being Nat for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) holds (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a) proof let n be Nat; ::_thesis: for K being Field for l being Nat for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) holds (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a) let K be Field; ::_thesis: for l being Nat for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) holds (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a) let l be Nat; ::_thesis: for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) holds (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a) let a be Element of K; ::_thesis: for A being Matrix of n,K st l in dom (1. (K,n)) holds (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a) let A be Matrix of n,K; ::_thesis: ( l in dom (1. (K,n)) implies (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a) ) assume A1: l in dom (1. (K,n)) ; ::_thesis: (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a) set B = SXLine ((1. (K,n)),l,a); A2: ( len (SXLine ((1. (K,n)),l,a)) = len (1. (K,n)) & len (SXLine ((1. (K,n)),l,a)) = n ) by Def2, MATRIX_1:24; then A3: l in Seg n by A1, FINSEQ_1:def_3; A4: width (SXLine ((1. (K,n)),l,a)) = n by MATRIX_1:24; A5: width A = n by MATRIX_1:24; A6: len A = n by MATRIX_1:24; A7: Indices ((SXLine ((1. (K,n)),l,a)) * A) = [:(Seg n),(Seg n):] by MATRIX_1:24; A8: width (SXLine ((1. (K,n)),l,a)) = 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 i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i = l holds ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) proof let i, j be Nat; ::_thesis: ( j in Seg n & i in dom (1. (K,n)) & i = l implies ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) ) assume that A12: j in Seg n and A13: i in dom (1. (K,n)) ; ::_thesis: ( not i = l or ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) ) thus ( i = l implies ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) ) ::_thesis: verum 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_1:24; len (Line ((1. (K,n)),l)) = width (1. (K,n)) by MATRIX_1: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_1: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 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 A10, MATRIX_3:15; ::_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 A17: t in dom (Line ((1. (K,n)),l)) and A18: t <> l ; ::_thesis: (Line ((1. (K,n)),l)) . t = 0. K 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_1:def_7; then [l,t] in Indices (1. (K,n)) by A1, ZFMISC_1:87; hence (Line ((1. (K,n)),l)) . t = 0. K by A18, MATRIX_3:15; ::_thesis: verum end; A19: dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def_3 .= Seg (len A) by A6, MATRIX_1:24 .= dom A by FINSEQ_1:def_3 ; then (Col (A,j)) . l = A * (l,j) by A1, MATRIX_1:def_8; then consider a1 being Element of K such that A20: a1 = (Col (A,j)) . l ; assume A21: i = l ; ::_thesis: ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) then [i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A) by A3, A7, A12, ZFMISC_1:87; then ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (Line ((SXLine ((1. (K,n)),l,a)),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_1:def_8 .= (SXLine (A,l,a)) * (i,j) by A5, A12, A13, A21, A19, Def2 ; hence ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) ; ::_thesis: verum end; end; A22: for i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i <> l holds ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) proof let i, j be Nat; ::_thesis: ( j in Seg n & i in dom (1. (K,n)) & i <> l implies ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) ) assume that A23: j in Seg n and A24: i in dom (1. (K,n)) ; ::_thesis: ( not i <> l or ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) ) 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 ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) ) ::_thesis: verum proof A27: ( (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 A26, MATRIX_3:15; ::_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 A28: t in dom (Line ((1. (K,n)),i)) and A29: t <> i ; ::_thesis: (Line ((1. (K,n)),i)) . t = 0. K 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_1:def_7; then [i,t] in Indices (1. (K,n)) by A24, ZFMISC_1:87; hence (Line ((1. (K,n)),i)) . t = 0. K by A29, MATRIX_3:15; ::_thesis: verum end; len (Col (A,j)) = len A by MATRIX_1: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_1:24 .= dom A by FINSEQ_1:def_3 ; len (Line ((1. (K,n)),i)) = width (1. (K,n)) by MATRIX_1:def_7; then A32: i in dom (Line ((1. (K,n)),i)) by A8, A4, A25, FINSEQ_1:def_3; assume A33: i <> l ; ::_thesis: ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) [i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A) by A7, A23, A25, ZFMISC_1:87; then ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (Line ((SXLine ((1. (K,n)),l,a)),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_1:def_8 .= (SXLine (A,l,a)) * (i,j) by A5, A23, A24, A33, A31, Def2 ; hence ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) ; ::_thesis: verum end; end; A34: for i, j being Nat st [i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A) holds ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A) implies ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) ) assume [i,j] in Indices ((SXLine ((1. (K,n)),l,a)) * A) ; ::_thesis: ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) 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_1:24 ; hence ((SXLine ((1. (K,n)),l,a)) * A) * (i,j) = (SXLine (A,l,a)) * (i,j) by A11, A22, A35; ::_thesis: verum end; A36: ( len ((SXLine ((1. (K,n)),l,a)) * A) = n & width ((SXLine ((1. (K,n)),l,a)) * A) = n ) by MATRIX_1:24; ( len (SXLine (A,l,a)) = len A & width (SXLine (A,l,a)) = width A ) by Def2, Th1; hence (SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a) by A6, A5, A36, A34, MATRIX_1:21; ::_thesis: verum end; theorem Th8: :: MATRIX12:8 for l, n, k being Nat for K being Field for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds (RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a) proof let l, n, k be Nat; ::_thesis: for K being Field for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds (RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a) let K be Field; ::_thesis: for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds (RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a) let a be Element of K; ::_thesis: for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds (RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a) let A be Matrix of n,K; ::_thesis: ( 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) ) assume that A1: l in dom (1. (K,n)) and A2: k in dom (1. (K,n)) ; ::_thesis: (RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a) set B = RLineXS ((1. (K,n)),l,k,a); A3: len (RLineXS ((1. (K,n)),l,k,a)) = n by MATRIX_1:24; A4: len A = n by MATRIX_1:24; dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def_3 .= Seg (len A) by A4, MATRIX_1:24 .= dom A by FINSEQ_1:def_3 ; then A5: len (RLineXS (A,l,k,a)) = len A by A2, Def3; A6: ( len ((RLineXS ((1. (K,n)),l,k,a)) * A) = n & width ((RLineXS ((1. (K,n)),l,k,a)) * A) = n ) by MATRIX_1:24; A7: width A = n by MATRIX_1:24; A8: len (RLineXS ((1. (K,n)),l,k,a)) = len (1. (K,n)) by A2, Def3; then A9: l in Seg n by A1, A3, FINSEQ_1:def_3; A10: width (RLineXS ((1. (K,n)),l,k,a)) = n by MATRIX_1:24; A11: width (RLineXS ((1. (K,n)),l,k,a)) = 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 ((RLineXS ((1. (K,n)),l,k,a)) * A) = [:(Seg n),(Seg n):] by MATRIX_1: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 i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i = l holds ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) proof let i, j be Nat; ::_thesis: ( j in Seg n & i in dom (1. (K,n)) & i = l implies ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) ) assume that A18: j in Seg n and i in dom (1. (K,n)) ; ::_thesis: ( not i = l or ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) ) thus ( i = l implies ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) ) ::_thesis: verum proof A19: ( (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 A13, MATRIX_3:15; ::_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 A20: t in dom (Line ((1. (K,n)),l)) and A21: t <> l ; ::_thesis: (Line ((1. (K,n)),l)) . t = 0. K 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_1:def_7; then [l,t] in Indices (1. (K,n)) by A1, ZFMISC_1:87; hence (Line ((1. (K,n)),l)) . t = 0. K by A21, MATRIX_3:15; ::_thesis: verum end; reconsider q = Col (A,j) as Element of (width A) -tuples_on the carrier of K by A4, MATRIX_1:24; A22: len (Col (A,j)) = len A by MATRIX_1: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_1: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_1: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 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 A16, MATRIX_3:15; ::_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 A30: t in dom (Line ((1. (K,n)),k)) and A31: t <> k ; ::_thesis: (Line ((1. (K,n)),k)) . t = 0. 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_1:def_7; then [k,t] in Indices (1. (K,n)) by A2, ZFMISC_1:87; hence (Line ((1. (K,n)),k)) . t = 0. K by A31, MATRIX_3:15; ::_thesis: verum end; A32: dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def_3 .= Seg (len A) by A4, MATRIX_1:24 .= dom A by FINSEQ_1:def_3 ; then (Col (A,j)) . k = A * (k,j) by A2, MATRIX_1: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_1:def_8; then consider a2 being Element of K such that A35: a2 = (Col (A,j)) . l ; assume A36: i = l ; ::_thesis: ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) then [i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A) by A9, A14, A18, ZFMISC_1:87; then ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (Line ((RLineXS ((1. (K,n)),l,k,a)),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_1:def_8 .= (RLineXS (A,l,k,a)) * (i,j) by A1, A2, A7, A18, A36, A32, Def3 ; hence ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) ; ::_thesis: verum end; end; A37: for i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i <> l holds ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) proof let i, j be Nat; ::_thesis: ( j in Seg n & i in dom (1. (K,n)) & i <> l implies ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) ) assume that A38: j in Seg n and A39: i in dom (1. (K,n)) ; ::_thesis: ( not i <> l or ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) ) 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 ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) ) ::_thesis: verum proof A42: ( (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 A41, MATRIX_3:15; ::_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 A43: t in dom (Line ((1. (K,n)),i)) and A44: t <> i ; ::_thesis: (Line ((1. (K,n)),i)) . t = 0. K 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_1:def_7; then [i,t] in Indices (1. (K,n)) by A39, ZFMISC_1:87; hence (Line ((1. (K,n)),i)) . t = 0. K by A44, MATRIX_3:15; ::_thesis: verum end; len (Col (A,j)) = len A by MATRIX_1: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_1:24 .= dom A by FINSEQ_1:def_3 ; len (Line ((1. (K,n)),i)) = width (1. (K,n)) by MATRIX_1:def_7; then A47: i in dom (Line ((1. (K,n)),i)) by A11, A10, A40, FINSEQ_1:def_3; assume A48: i <> l ; ::_thesis: ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) [i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A) by A14, A38, A40, ZFMISC_1:87; then ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (Line ((RLineXS ((1. (K,n)),l,k,a)),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_1:def_8 .= (RLineXS (A,l,k,a)) * (i,j) by A2, A7, A38, A39, A48, A46, Def3 ; hence ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) ; ::_thesis: verum end; end; A49: for i, j being Nat st [i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A) holds ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A) implies ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) ) assume [i,j] in Indices ((RLineXS ((1. (K,n)),l,k,a)) * A) ; ::_thesis: ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) 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_1:24 ; hence ((RLineXS ((1. (K,n)),l,k,a)) * A) * (i,j) = (RLineXS (A,l,k,a)) * (i,j) by A17, A37, A50; ::_thesis: verum end; width (RLineXS (A,l,k,a)) = width A by Th1; hence (RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a) by A4, A7, A6, A5, A49, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX12:9 for n, m, k being Nat for K being Field for M being Matrix of n,m,K holds ILine (M,k,k) = M proof let n, m, k be Nat; ::_thesis: for K being Field for M being Matrix of n,m,K holds ILine (M,k,k) = M let K be Field; ::_thesis: for M being Matrix of n,m,K holds ILine (M,k,k) = M let M be Matrix of n,m,K; ::_thesis: ILine (M,k,k) = M A1: for i, j being Nat st [i,j] in Indices M holds (ILine (M,k,k)) * (i,j) = M * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies (ILine (M,k,k)) * (i,j) = M * (i,j) ) assume [i,j] in Indices M ; ::_thesis: (ILine (M,k,k)) * (i,j) = M * (i,j) 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 (ILine (M,k,k)) * (i,j) = M * (i,j) by A2, Def1; ::_thesis: verum end; ( len (ILine (M,k,k)) = len M & width (ILine (M,k,k)) = width M ) by Def1, Th1; hence ILine (M,k,k) = M by A1, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX12:10 for n, m, l, k being Nat for K being Field for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l) proof let n, m, l, k be Nat; ::_thesis: for K being Field for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l) let K be Field; ::_thesis: for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l) let M be Matrix of n,m,K; ::_thesis: ILine (M,l,k) = ILine (M,k,l) A1: width (ILine (M,k,l)) = width M by Th1; A2: for i, j being Nat 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 be Nat; ::_thesis: ( [i,j] in Indices (ILine (M,l,k)) implies (ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j) ) A3: Indices (ILine (M,l,k)) = Indices M by MATRIX_1:26; assume [i,j] in Indices (ILine (M,l,k)) ; ::_thesis: (ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j) 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 (ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j) by A4, A5, A7, A6, A8, Def1; ::_thesis: verum end; ( len (ILine (M,l,k)) = len M & len (ILine (M,k,l)) = len M ) by Def1; hence ILine (M,l,k) = ILine (M,k,l) by A1, A2, Th1, MATRIX_1:21; ::_thesis: verum end; theorem Th11: :: MATRIX12:11 for n, m, l, k being Nat for K being Field for M being Matrix of n,m,K st l in dom M & k in dom M holds ILine ((ILine (M,l,k)),l,k) = M proof let n, m, l, k be Nat; ::_thesis: for K being Field for M being Matrix of n,m,K st l in dom M & k in dom M holds ILine ((ILine (M,l,k)),l,k) = M let K be Field; ::_thesis: for M being Matrix of n,m,K st l in dom M & k in dom M holds ILine ((ILine (M,l,k)),l,k) = M let M be Matrix of n,m,K; ::_thesis: ( l in dom M & k in dom M implies ILine ((ILine (M,l,k)),l,k) = M ) assume A1: ( l in dom M & k in dom M ) ; ::_thesis: ILine ((ILine (M,l,k)),l,k) = M set M1 = ILine (M,l,k); A2: dom (ILine (M,l,k)) = 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 (ILine (M,l,k)) = width M by Th1; A4: for i, j being Nat st [i,j] in Indices M holds (ILine ((ILine (M,l,k)),l,k)) * (i,j) = M * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies (ILine ((ILine (M,l,k)),l,k)) * (i,j) = M * (i,j) ) assume A5: [i,j] in Indices M ; ::_thesis: (ILine ((ILine (M,l,k)),l,k)) * (i,j) = M * (i,j) 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 ((ILine (M,l,k)),l,k)) * (i,j) = (ILine (M,l,k)) * (i,j) ) by A3, A2, A6, Def1; then A8: ( i <> l & i <> k implies (ILine ((ILine (M,l,k)),l,k)) * (i,j) = M * (i,j) ) by A7, A6, Def1; ( (ILine ((ILine (M,l,k)),l,k)) * (l,j) = (ILine (M,l,k)) * (k,j) & (ILine ((ILine (M,l,k)),l,k)) * (k,j) = (ILine (M,l,k)) * (l,j) ) by A1, A3, A2, A6, Def1; hence (ILine ((ILine (M,l,k)),l,k)) * (i,j) = M * (i,j) by A1, A6, A8, Def1; ::_thesis: verum end; A9: width (ILine ((ILine (M,l,k)),l,k)) = width (ILine (M,l,k)) by Th1; ( len (ILine (M,l,k)) = len M & len (ILine ((ILine (M,l,k)),l,k)) = len (ILine (M,l,k)) ) by Def1; hence ILine ((ILine (M,l,k)),l,k) = M by A9, A4, Th1, MATRIX_1:21; ::_thesis: verum end; theorem Th12: :: MATRIX12:12 for l, n, k being Nat for K being Field st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds ( ILine ((1. (K,n)),l,k) is invertible & (ILine ((1. (K,n)),l,k)) ~ = ILine ((1. (K,n)),l,k) ) proof let l, n, k be Nat; ::_thesis: for K being Field st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds ( ILine ((1. (K,n)),l,k) is invertible & (ILine ((1. (K,n)),l,k)) ~ = ILine ((1. (K,n)),l,k) ) let K be Field; ::_thesis: ( 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) ) ) assume ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) ; ::_thesis: ( ILine ((1. (K,n)),l,k) is invertible & (ILine ((1. (K,n)),l,k)) ~ = ILine ((1. (K,n)),l,k) ) 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 ( ILine ((1. (K,n)),l,k) is invertible & (ILine ((1. (K,n)),l,k)) ~ = ILine ((1. (K,n)),l,k) ) by A1, MATRIX_6:def_4; ::_thesis: verum end; Lm4: for n being Nat for K being Field for i, j, l, k being Nat for a being Element of K 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 n be Nat; ::_thesis: for K being Field for i, j, l, k being Nat for a being Element of K 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) let K be Field; ::_thesis: for i, j, l, k being Nat for a being Element of K 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) let i, j, l, k be Nat; ::_thesis: for a being Element of K 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) let a be Element of K; ::_thesis: ( [i,j] in Indices (1. (K,n)) & l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l implies (1. (K,n)) * (i,j) = (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) ) 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 ; ::_thesis: (1. (K,n)) * (i,j) = (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) 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 (RLineXS ((1. (K,n)),l,k,(- a))) = width (1. (K,n)) & width (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) = width (RLineXS ((1. (K,n)),l,k,(- a))) ) by Th1; A8: dom (RLineXS ((1. (K,n)),l,k,(- a))) = Seg (len (RLineXS ((1. (K,n)),l,k,(- a)))) 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 (RLineXS ((1. (K,n)),l,k,(- a))) by A1, ZFMISC_1:87; now__::_thesis:_(_(_i_=_l_&_(RLineXS_((RLineXS_((1._(K,n)),l,k,(-_a))),l,k,a))_*_(i,j)_=_(1._(K,n))_*_(i,j)_)_or_(_i_<>_l_&_(RLineXS_((RLineXS_((1._(K,n)),l,k,(-_a))),l,k,a))_*_(i,j)_=_(1._(K,n))_*_(i,j)_)_) percases ( i = l or i <> l ) ; caseA10: i = l ; ::_thesis: (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) = (1. (K,n)) * (i,j) reconsider p2 = Line ((1. (K,n)),i) as Element of (width (RLineXS ((1. (K,n)),l,k,(- a)))) -tuples_on the carrier of K by Th1; reconsider p1 = Line ((1. (K,n)),k) as Element of (width (RLineXS ((1. (K,n)),l,k,(- a)))) -tuples_on the carrier of K by Th1; A11: Line ((RLineXS ((1. (K,n)),l,k,(- a))),k) = Line ((1. (K,n)),k) by A2, A3, A4, Th5; Line ((RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)),i) = (a * (Line ((RLineXS ((1. (K,n)),l,k,(- a))),k))) + (Line ((RLineXS ((1. (K,n)),l,k,(- a))),i)) by A2, A3, A8, A10, Th5; then Line ((RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),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 (RLineXS ((1. (K,n)),l,k,(- a)))) |-> (0. K)) + p2 by FVSUM_1:58 .= Line ((1. (K,n)),i) by FVSUM_1:21 ; hence (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) = (Line ((1. (K,n)),i)) . j by A6, A7, MATRIX_1:def_7 .= (1. (K,n)) * (i,j) by A6, MATRIX_1:def_7 ; ::_thesis: verum end; caseA12: i <> l ; ::_thesis: (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) = (1. (K,n)) * (i,j) then A13: Line ((RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)),i) = Line ((RLineXS ((1. (K,n)),l,k,(- a))),i) by A2, A3, A8, A9, Th5; thus (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) = (Line ((RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)),i)) . j by A6, A7, MATRIX_1:def_7 .= (Line ((1. (K,n)),i)) . j by A2, A3, A5, A12, A13, Th5 .= (1. (K,n)) * (i,j) by A6, MATRIX_1:def_7 ; ::_thesis: verum end; end; end; hence (1. (K,n)) * (i,j) = (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) ; ::_thesis: verum end; theorem Th13: :: MATRIX12:13 for l, n, k being Nat for K being Field for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l holds ( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) ) proof let l, n, k be Nat; ::_thesis: for K being Field for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l holds ( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) ) let K be Field; ::_thesis: for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l holds ( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) ) let a be Element of K; ::_thesis: ( 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)) ) ) assume that A1: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) and A2: k <> l ; ::_thesis: ( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) ) set B = RLineXS ((1. (K,n)),l,k,(- a)); for i, j being Nat st [i,j] in Indices (1. (K,n)) holds (1. (K,n)) * (i,j) = (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) by A1, A2, Lm4; then A3: 1. (K,n) = RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a) by MATRIX_1:27; set b = - a; set A = RLineXS ((1. (K,n)),l,k,a); a + (- a) = 0. K by RLVECT_1:def_10; then a = - (- a) by RLVECT_1:6; then for i, j being Nat st [i,j] in Indices (1. (K,n)) holds (1. (K,n)) * (i,j) = (RLineXS ((RLineXS ((1. (K,n)),l,k,a)),l,k,(- a))) * (i,j) by A1, A2, Lm4; then A4: 1. (K,n) = RLineXS ((RLineXS ((1. (K,n)),l,k,a)),l,k,(- a)) by MATRIX_1:27; ( (RLineXS ((1. (K,n)),l,k,a)) * (RLineXS ((1. (K,n)),l,k,(- a))) = RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a) & (RLineXS ((1. (K,n)),l,k,(- a))) * (RLineXS ((1. (K,n)),l,k,a)) = RLineXS ((RLineXS ((1. (K,n)),l,k,a)),l,k,(- a)) ) by A1, Th8; then A5: RLineXS ((1. (K,n)),l,k,(- a)) is_reverse_of RLineXS ((1. (K,n)),l,k,a) by A3, A4, MATRIX_6:def_2; then RLineXS ((1. (K,n)),l,k,a) is invertible by MATRIX_6:def_3; hence ( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) ) by A5, MATRIX_6:def_4; ::_thesis: verum end; theorem Th14: :: MATRIX12:14 for l, n being Nat for K being Field for a being Element of K st l in dom (1. (K,n)) & a <> 0. K holds ( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) ) proof let l, n be Nat; ::_thesis: for K being Field for a being Element of K st l in dom (1. (K,n)) & a <> 0. K holds ( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) ) let K be Field; ::_thesis: for a being Element of K st l in dom (1. (K,n)) & a <> 0. K holds ( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) ) let a be Element of K; ::_thesis: ( l in dom (1. (K,n)) & a <> 0. K implies ( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) ) ) assume that A1: l in dom (1. (K,n)) and A2: a <> 0. K ; ::_thesis: ( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) ) set A = SXLine ((1. (K,n)),l,a); A3: dom (SXLine ((1. (K,n)),l,a)) = Seg (len (SXLine ((1. (K,n)),l,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 (SXLine ((1. (K,n)),l,(a "))) = Seg (len (SXLine ((1. (K,n)),l,(a ")))) by FINSEQ_1:def_3 .= Seg (len (1. (K,n))) by Def2 .= dom (1. (K,n)) by FINSEQ_1:def_3 ; A5: width (SXLine ((1. (K,n)),l,(a "))) = width (1. (K,n)) by Th1; for i, j being Nat st [i,j] in Indices (1. (K,n)) holds (1. (K,n)) * (i,j) = (SXLine ((SXLine ((1. (K,n)),l,(a "))),l,a)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = (SXLine ((SXLine ((1. (K,n)),l,(a "))),l,a)) * (i,j) ) assume A6: [i,j] in Indices (1. (K,n)) ; ::_thesis: (1. (K,n)) * (i,j) = (SXLine ((SXLine ((1. (K,n)),l,(a "))),l,a)) * (i,j) 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 (SXLine ((1. (K,n)),l,(a "))) * (i,j) = (1. (K,n)) * (i,j) ) by A7, Def2; (SXLine ((1. (K,n)),l,(a "))) * (l,j) = (a ") * ((1. (K,n)) * (l,j)) by A1, A8, Def2; then A10: (SXLine ((SXLine ((1. (K,n)),l,(a "))),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 .= (1_ K) * ((1. (K,n)) * (l,j)) by A2, VECTSP_2:def_2 .= (1. (K,n)) * (l,j) by GROUP_1:def_4 ; ( i <> l implies (SXLine ((SXLine ((1. (K,n)),l,(a "))),l,a)) * (i,j) = (SXLine ((1. (K,n)),l,(a "))) * (i,j) ) by A5, A4, A7, A8, Def2; hence (1. (K,n)) * (i,j) = (SXLine ((SXLine ((1. (K,n)),l,(a "))),l,a)) * (i,j) by A9, A10; ::_thesis: verum end; then A11: 1. (K,n) = SXLine ((SXLine ((1. (K,n)),l,(a "))),l,a) by MATRIX_1:27; A12: width (SXLine ((1. (K,n)),l,a)) = width (1. (K,n)) by Th1; for i, j being Nat st [i,j] in Indices (1. (K,n)) holds (1. (K,n)) * (i,j) = (SXLine ((SXLine ((1. (K,n)),l,a)),l,(a "))) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = (SXLine ((SXLine ((1. (K,n)),l,a)),l,(a "))) * (i,j) ) assume A13: [i,j] in Indices (1. (K,n)) ; ::_thesis: (1. (K,n)) * (i,j) = (SXLine ((SXLine ((1. (K,n)),l,a)),l,(a "))) * (i,j) 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 (SXLine ((1. (K,n)),l,a)) * (i,j) = (1. (K,n)) * (i,j) ) by A14, Def2; (SXLine ((1. (K,n)),l,a)) * (l,j) = a * ((1. (K,n)) * (l,j)) by A1, A15, Def2; then A17: (SXLine ((SXLine ((1. (K,n)),l,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 A2, VECTSP_2:def_2 .= (1. (K,n)) * (l,j) by GROUP_1:def_4 ; ( i <> l implies (SXLine ((SXLine ((1. (K,n)),l,a)),l,(a "))) * (i,j) = (SXLine ((1. (K,n)),l,a)) * (i,j) ) by A12, A3, A14, A15, Def2; hence (1. (K,n)) * (i,j) = (SXLine ((SXLine ((1. (K,n)),l,a)),l,(a "))) * (i,j) by A16, A17; ::_thesis: verum end; then A18: 1. (K,n) = SXLine ((SXLine ((1. (K,n)),l,a)),l,(a ")) by MATRIX_1:27; ( (SXLine ((1. (K,n)),l,a)) * (SXLine ((1. (K,n)),l,(a "))) = SXLine ((SXLine ((1. (K,n)),l,(a "))),l,a) & (SXLine ((1. (K,n)),l,(a "))) * (SXLine ((1. (K,n)),l,a)) = SXLine ((SXLine ((1. (K,n)),l,a)),l,(a ")) ) by A1, Th7; then A19: SXLine ((1. (K,n)),l,(a ")) is_reverse_of SXLine ((1. (K,n)),l,a) by A11, A18, MATRIX_6:def_2; then SXLine ((1. (K,n)),l,a) is invertible by MATRIX_6:def_3; hence ( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) ) by A19, MATRIX_6:def_4; ::_thesis: verum end; definition let n, m be Nat; let K be Field; 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: :: MATRIX12:def 4 ( len it = len M & ( for i, j being Nat 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 ex b1 being Matrix of n,m,K st ( len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b1 * (i,j) = M * (i,k) ) & ( j = k implies b1 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b1 * (i,j) = M * (i,j) ) ) ) ) proof A5: width M = m by A3, MATRIX_1:23; then A6: len (M @) = m by A4, MATRIX_2:10; A7: len M = n by A3, MATRIX_1:23; then width (M @) = n by A4, A5, MATRIX_2:10; then M @ is Matrix of m,n,K by A4, A6, MATRIX_1: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_1:23; then A10: len ((ILine (M1,l,k)) @) = n by A3, MATRIX_2:10; len (ILine (M1,l,k)) = m by A4, MATRIX_1:23; then width ((ILine (M1,l,k)) @) = m by A3, A9, MATRIX_2:10; then (ILine (M1,l,k)) @ is Matrix of n,m,K by A3, A10, MATRIX_1:20; then consider M2 being Matrix of n,m,K such that A11: M2 = (ILine (M1,l,k)) @ ; take M2 ; ::_thesis: ( len M2 = len M & ( for i, j being Nat 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 being Nat 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 be Nat; ::_thesis: ( i in dom M & j in Seg (width M) implies ( ( 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) ) ) ) assume that A12: i in dom M and A13: j in Seg (width M) ; ::_thesis: ( ( 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) ) ) A14: [i,j] in Indices M by A12, A13, ZFMISC_1:87; then A15: [j,i] in Indices M1 by A8, MATRIX_1: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) ) ::_thesis: ( ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) ) proof A18: [i,k] in Indices M by A2, A12, ZFMISC_1:87; assume A19: j = l ; ::_thesis: M2 * (i,j) = M * (i,k) M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A11, A17, MATRIX_1:def_6 .= M1 * (k,i) by A16, A19, Def1 .= M * (i,k) by A8, A18, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,k) ; ::_thesis: verum end; thus ( j = k implies M2 * (i,j) = M * (i,l) ) ::_thesis: ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) proof A20: [i,l] in Indices M by A1, A12, ZFMISC_1:87; assume A21: j = k ; ::_thesis: M2 * (i,j) = M * (i,l) M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A11, A17, MATRIX_1:def_6 .= M1 * (l,i) by A16, A21, Def1 .= M * (i,l) by A8, A20, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,l) ; ::_thesis: verum end; thus ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) ::_thesis: verum proof assume A22: ( j <> l & j <> k ) ; ::_thesis: M2 * (i,j) = M * (i,j) M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A11, A17, MATRIX_1:def_6 .= M1 * (j,i) by A16, A22, Def1 .= M * (i,j) by A8, A14, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,j) ; ::_thesis: verum end; end; hence ( len M2 = len M & ( for i, j being Nat 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) ) ) ) ) by A3, A7, MATRIX_1:23; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of n,m,K st len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b1 * (i,j) = M * (i,k) ) & ( j = k implies b1 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b1 * (i,j) = M * (i,j) ) ) ) & len b2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b2 * (i,j) = M * (i,k) ) & ( j = k implies b2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b2 * (i,j) = M * (i,j) ) ) ) holds b1 = b2 proof let M1, M2 be Matrix of n,m,K; ::_thesis: ( len M1 = len M & ( for i, j being Nat 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) ) ) ) & len M2 = len M & ( for i, j being Nat 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) ) ) ) implies M1 = M2 ) assume that len M1 = len M and A23: for i, j being Nat 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 being Nat 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) ) ) ; ::_thesis: M1 = M2 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = M2 * (i,j) proof A25: Indices M = Indices M1 by MATRIX_1:26; let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) 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 M1 * (i,j) = M2 * (i,j) by A24, A26, A27, A29, A28, A30; ::_thesis: verum end; hence M1 = M2 by MATRIX_1:27; ::_thesis: verum end; end; :: deftheorem Def4 defines InterchangeCol MATRIX12:def_4_:_ for n, m being Nat for K being Field for M being Matrix of n,m,K for l, k being Nat st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 holds for b7 being Matrix of n,m,K holds ( b7 = InterchangeCol (M,l,k) iff ( len b7 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b7 * (i,j) = M * (i,k) ) & ( j = k implies b7 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b7 * (i,j) = M * (i,j) ) ) ) ) ); definition let n, m be Nat; let K be Field; 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: :: MATRIX12:def 5 ( len it = len M & ( for i, j being Nat 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 ex b1 being Matrix of n,m,K st ( len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b1 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) ) proof A4: width M = m by A2, MATRIX_1:23; then A5: len (M @) = m by A3, MATRIX_2:10; A6: len M = n by A2, MATRIX_1:23; then width (M @) = n by A3, A4, MATRIX_2:10; then M @ is Matrix of m,n,K by A3, A5, MATRIX_1: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_1:23; then A9: len ((ScalarXLine (M1,l,a)) @) = n by A2, MATRIX_2:10; len (ScalarXLine (M1,l,a)) = m by A3, MATRIX_1:23; then width ((ScalarXLine (M1,l,a)) @) = m by A2, A8, MATRIX_2:10; then (ScalarXLine (M1,l,a)) @ is Matrix of n,m,K by A2, A9, MATRIX_1:20; then consider M2 being Matrix of n,m,K such that A10: M2 = (ScalarXLine (M1,l,a)) @ ; take M2 ; ::_thesis: ( len M2 = len M & ( for i, j being Nat 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 being Nat 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 be Nat; ::_thesis: ( i in dom M & j in Seg (width M) implies ( ( j = l implies M2 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) ) assume that A11: i in dom M and A12: j in Seg (width M) ; ::_thesis: ( ( j = l implies M2 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) A13: [i,j] in Indices M by A11, A12, ZFMISC_1:87; then A14: [j,i] in Indices M1 by A7, MATRIX_1: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)) ) ::_thesis: ( j <> l implies M2 * (i,j) = M * (i,j) ) proof A17: [i,l] in Indices M by A1, A11, ZFMISC_1:87; assume A18: j = l ; ::_thesis: M2 * (i,j) = a * (M * (i,l)) M2 * (i,j) = (ScalarXLine (M1,l,a)) * (j,i) by A10, A15, MATRIX_1:def_6 .= a * (M1 * (l,i)) by A16, A18, Def2 .= a * (M * (i,l)) by A7, A17, MATRIX_1:def_6 ; hence M2 * (i,j) = a * (M * (i,l)) ; ::_thesis: verum end; thus ( j <> l implies M2 * (i,j) = M * (i,j) ) ::_thesis: verum proof assume A19: j <> l ; ::_thesis: M2 * (i,j) = M * (i,j) M2 * (i,j) = (ScalarXLine (M1,l,a)) * (j,i) by A10, A15, MATRIX_1:def_6 .= M1 * (j,i) by A16, A19, Def2 .= M * (i,j) by A7, A13, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,j) ; ::_thesis: verum end; end; hence ( len M2 = len M & ( for i, j being Nat 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) ) ) ) ) by A2, A6, MATRIX_1:23; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of n,m,K st len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b1 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) & len b2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b2 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds b1 = b2 proof let M1, M2 be Matrix of n,m,K; ::_thesis: ( len M1 = len M & ( for i, j being Nat 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) ) ) ) & len M2 = len M & ( for i, j being Nat 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) ) ) ) implies M1 = M2 ) assume that len M1 = len M and A20: for i, j being Nat 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 being Nat 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) ) ) ; ::_thesis: M1 = M2 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = M2 * (i,j) proof A22: Indices M = Indices M1 by MATRIX_1:26; let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) 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 M1 * (i,j) = M2 * (i,j) by A21, A23, A24; ::_thesis: verum end; hence M1 = M2 by MATRIX_1:27; ::_thesis: verum end; end; :: deftheorem Def5 defines ScalarXCol MATRIX12:def_5_:_ for n, m being Nat for K being Field for M being Matrix of n,m,K for l being Nat for a being Element of K st l in Seg (width M) & n > 0 & m > 0 holds for b7 being Matrix of n,m,K holds ( b7 = ScalarXCol (M,l,a) iff ( len b7 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b7 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b7 * (i,j) = M * (i,j) ) ) ) ) ); definition let n, m be Nat; let K be Field; 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: :: MATRIX12:def 6 ( len it = len M & ( for i, j being Nat 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 ex b1 being Matrix of n,m,K st ( len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b1 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) ) proof A5: width M = m by A3, MATRIX_1:23; then A6: len (M @) = m by A4, MATRIX_2:10; A7: len M = n by A3, MATRIX_1:23; then width (M @) = n by A4, A5, MATRIX_2:10; then M @ is Matrix of m,n,K by A4, A6, MATRIX_1: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_1:23; then A10: len ((RlineXScalar (M1,l,k,a)) @) = n by A3, MATRIX_2:10; len (RlineXScalar (M1,l,k,a)) = m by A4, MATRIX_1:23; then width ((RlineXScalar (M1,l,k,a)) @) = m by A3, A9, MATRIX_2:10; then (RlineXScalar (M1,l,k,a)) @ is Matrix of n,m,K by A3, A10, MATRIX_1:20; then consider M2 being Matrix of n,m,K such that A11: M2 = (RlineXScalar (M1,l,k,a)) @ ; take M2 ; ::_thesis: ( len M2 = len M & ( for i, j being Nat 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 being Nat 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 be Nat; ::_thesis: ( i in dom M & j in Seg (width M) implies ( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) ) assume that A12: i in dom M and A13: j in Seg (width M) ; ::_thesis: ( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) A14: [i,j] in Indices M by A12, A13, ZFMISC_1:87; then A15: [j,i] in Indices M1 by A8, MATRIX_1:def_6; then A16: i in Seg (width M1) by ZFMISC_1:87; A17: len M1 = width M by A8, MATRIX_1: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)) ) ::_thesis: ( j <> l implies M2 * (i,j) = M * (i,j) ) 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 ; ::_thesis: M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) M2 * (i,j) = (RlineXScalar (M1,l,k,a)) * (j,i) by A11, A19, MATRIX_1: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_1:def_6 .= (a * (M * (i,k))) + (M * (i,l)) by A8, A22, MATRIX_1:def_6 ; hence M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ; ::_thesis: verum end; A24: j in dom M1 by A15, ZFMISC_1:87; thus ( j <> l implies M2 * (i,j) = M * (i,j) ) ::_thesis: verum proof assume A25: j <> l ; ::_thesis: M2 * (i,j) = M * (i,j) M2 * (i,j) = (RlineXScalar (M1,l,k,a)) * (j,i) by A11, A19, MATRIX_1:def_6 .= M1 * (j,i) by A18, A24, A16, A25, Def3 .= M * (i,j) by A8, A14, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,j) ; ::_thesis: verum end; end; hence ( len M2 = len M & ( for i, j being Nat 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) ) ) ) ) by A3, A7, MATRIX_1:23; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of n,m,K st len b1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b1 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) & len b2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds b1 = b2 proof let M1, M2 be Matrix of n,m,K; ::_thesis: ( len M1 = len M & ( for i, j being Nat 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) ) ) ) & len M2 = len M & ( for i, j being Nat 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) ) ) ) implies M1 = M2 ) assume that len M1 = len M and A26: for i, j being Nat 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 being Nat 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) ) ) ; ::_thesis: M1 = M2 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = M2 * (i,j) proof A28: Indices M = Indices M1 by MATRIX_1:26; let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) 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 M1 * (i,j) = M2 * (i,j) by A27, A29, A30; ::_thesis: verum end; hence M1 = M2 by MATRIX_1:27; ::_thesis: verum end; end; :: deftheorem Def6 defines RcolXScalar MATRIX12:def_6_:_ for n, m being Nat for K being Field for M being Matrix of n,m,K for l, k being Nat for a being Element of K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 holds for b8 being Matrix of n,m,K holds ( b8 = RcolXScalar (M,l,k,a) iff ( len b8 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds ( ( j = l implies b8 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b8 * (i,j) = M * (i,j) ) ) ) ) ); notation let n, m be Nat; let K be Field; 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 be Nat; let K be Field; 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 be Nat; let K be Field; 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: :: MATRIX12:15 for l, k, n, m being Nat for K being Field for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (ILine (M1,l,k)) @ = ICol (M,l,k) proof let l, k, n, m be Nat; ::_thesis: for K being Field for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (ILine (M1,l,k)) @ = ICol (M,l,k) let K be Field; ::_thesis: for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (ILine (M1,l,k)) @ = ICol (M,l,k) let M, M1 be Matrix of n,m,K; ::_thesis: ( 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) ) 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 @ ; ::_thesis: (ILine (M1,l,k)) @ = ICol (M,l,k) A6: width M = m by A3, MATRIX_1:23; A7: width (ILine (M1,l,k)) = width M1 by Th1; len M = n by A3, MATRIX_1:23; then A8: width M1 = n by A4, A5, A6, MATRIX_2:10; then A9: len ((ILine (M1,l,k)) @) = n by A3, A7, MATRIX_2:10; A10: len (ILine (M1,l,k)) = len M1 by Def1; len M1 = m by A4, A5, A6, MATRIX_2:10; then width ((ILine (M1,l,k)) @) = m by A3, A8, A10, A7, MATRIX_2:10; then A11: (ILine (M1,l,k)) @ is Matrix of n,m,K by A3, A9, MATRIX_1:20; then consider M2 being Matrix of n,m,K such that A12: M2 = (ILine (M1,l,k)) @ ; A13: for i, j being Nat 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 be Nat; ::_thesis: ( i in dom M & j in Seg (width M) implies ( ( 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) ) ) ) assume that A14: i in dom M and A15: j in Seg (width M) ; ::_thesis: ( ( 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) ) ) A16: [i,j] in Indices M by A14, A15, ZFMISC_1:87; then A17: [j,i] in Indices M1 by A5, MATRIX_1: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) ) ::_thesis: ( ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) ) proof A20: [i,k] in Indices M by A2, A14, ZFMISC_1:87; assume A21: j = l ; ::_thesis: M2 * (i,j) = M * (i,k) M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A12, A19, MATRIX_1:def_6 .= M1 * (k,i) by A18, A21, Def1 .= M * (i,k) by A5, A20, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,k) ; ::_thesis: verum end; thus ( j = k implies M2 * (i,j) = M * (i,l) ) ::_thesis: ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) proof A22: [i,l] in Indices M by A1, A14, ZFMISC_1:87; assume A23: j = k ; ::_thesis: M2 * (i,j) = M * (i,l) M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A12, A19, MATRIX_1:def_6 .= M1 * (l,i) by A18, A23, Def1 .= M * (i,l) by A5, A22, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,l) ; ::_thesis: verum end; assume A24: ( j <> l & j <> k ) ; ::_thesis: M2 * (i,j) = M * (i,j) M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A12, A19, MATRIX_1:def_6 .= M1 * (j,i) by A18, A24, Def1 .= M * (i,j) by A5, A16, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,j) ; ::_thesis: verum end; for i, j being Nat 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_1:26; let i, j be Nat; ::_thesis: ( [i,j] in Indices (ICol (M,l,k)) implies (ICol (M,l,k)) * (i,j) = ((ILine (M1,l,k)) @) * (i,j) ) assume [i,j] in Indices (ICol (M,l,k)) ; ::_thesis: (ICol (M,l,k)) * (i,j) = ((ILine (M1,l,k)) @) * (i,j) 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 (ICol (M,l,k)) * (i,j) = ((ILine (M1,l,k)) @) * (i,j) by A1, A2, A3, A4, A26, A27, A29, A30, A28, Def4; ::_thesis: verum end; hence (ILine (M1,l,k)) @ = ICol (M,l,k) by A11, MATRIX_1:27; ::_thesis: verum end; theorem Th16: :: MATRIX12:16 for l, n, m being Nat for K being Field for a being Element of K for M, M1 being Matrix of n,m,K st l in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (SXLine (M1,l,a)) @ = SXCol (M,l,a) proof let l, n, m be Nat; ::_thesis: for K being Field for a being Element of K for M, M1 being Matrix of n,m,K st l in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (SXLine (M1,l,a)) @ = SXCol (M,l,a) let K be Field; ::_thesis: for a being Element of K for M, M1 being Matrix of n,m,K st l in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (SXLine (M1,l,a)) @ = SXCol (M,l,a) let a be Element of K; ::_thesis: for M, M1 being Matrix of n,m,K st l in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (SXLine (M1,l,a)) @ = SXCol (M,l,a) let M, M1 be Matrix of n,m,K; ::_thesis: ( l in Seg (width M) & n > 0 & m > 0 & M1 = M @ implies (SXLine (M1,l,a)) @ = SXCol (M,l,a) ) assume that A1: l in Seg (width M) and A2: n > 0 and A3: m > 0 and A4: M1 = M @ ; ::_thesis: (SXLine (M1,l,a)) @ = SXCol (M,l,a) A5: width M = m by A2, MATRIX_1:23; A6: width (SXLine (M1,l,a)) = width M1 by Th1; len M = n by A2, MATRIX_1:23; then A7: width M1 = n by A3, A4, A5, MATRIX_2:10; then A8: len ((SXLine (M1,l,a)) @) = n by A2, A6, MATRIX_2:10; A9: len (SXLine (M1,l,a)) = len M1 by Def2; len M1 = m by A3, A4, A5, MATRIX_2:10; then width ((SXLine (M1,l,a)) @) = m by A2, A7, A9, A6, MATRIX_2:10; then A10: (SXLine (M1,l,a)) @ is Matrix of n,m,K by A2, A8, MATRIX_1:20; then consider M2 being Matrix of n,m,K such that A11: M2 = (SXLine (M1,l,a)) @ ; A12: for i, j being Nat 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 be Nat; ::_thesis: ( i in dom M & j in Seg (width M) implies ( ( j = l implies M2 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) ) assume ( i in dom M & j in Seg (width M) ) ; ::_thesis: ( ( j = l implies M2 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) then A13: [i,j] in Indices M by ZFMISC_1:87; then A14: [j,i] in Indices M1 by A4, MATRIX_1: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)) ) ::_thesis: ( j <> l implies M2 * (i,j) = M * (i,j) ) proof assume A17: j = l ; ::_thesis: M2 * (i,j) = a * (M * (i,l)) M2 * (i,j) = (SXLine (M1,l,a)) * (j,i) by A11, A16, MATRIX_1:def_6 .= a * (M1 * (l,i)) by A15, A17, Def2 .= a * (M * (i,l)) by A4, A13, A17, MATRIX_1:def_6 ; hence M2 * (i,j) = a * (M * (i,l)) ; ::_thesis: verum end; assume A18: j <> l ; ::_thesis: M2 * (i,j) = M * (i,j) M2 * (i,j) = (SXLine (M1,l,a)) * (j,i) by A11, A16, MATRIX_1:def_6 .= M1 * (j,i) by A15, A18, Def2 .= M * (i,j) by A4, A13, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,j) ; ::_thesis: verum end; for i, j being Nat 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_1:26; let i, j be Nat; ::_thesis: ( [i,j] in Indices (SXCol (M,l,a)) implies (SXCol (M,l,a)) * (i,j) = ((SXLine (M1,l,a)) @) * (i,j) ) assume [i,j] in Indices (SXCol (M,l,a)) ; ::_thesis: (SXCol (M,l,a)) * (i,j) = ((SXLine (M1,l,a)) @) * (i,j) 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 (SXCol (M,l,a)) * (i,j) = ((SXLine (M1,l,a)) @) * (i,j) by A1, A2, A3, A20, A21, A22, Def5; ::_thesis: verum end; hence (SXLine (M1,l,a)) @ = SXCol (M,l,a) by A10, MATRIX_1:27; ::_thesis: verum end; theorem Th17: :: MATRIX12:17 for l, k, n, m being Nat for K being Field for a being Element of K for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a) proof let l, k, n, m be Nat; ::_thesis: for K being Field for a being Element of K for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a) let K be Field; ::_thesis: for a being Element of K for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a) let a be Element of K; ::_thesis: for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a) let M, M1 be Matrix of n,m,K; ::_thesis: ( 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) ) 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 @ ; ::_thesis: (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a) A6: width M = m by A3, MATRIX_1:23; then A7: len M1 = m by A4, A5, MATRIX_2:10; A8: width (RLineXS (M1,l,k,a)) = width M1 by Th1; len M = n by A3, MATRIX_1:23; then A9: width M1 = n by A4, A5, A6, MATRIX_2:10; then A10: len ((RLineXS (M1,l,k,a)) @) = n by A3, A8, MATRIX_2:10; A11: dom M1 = Seg (len M1) by FINSEQ_1:def_3 .= Seg (width M) by A4, A5, A6, MATRIX_2:10 ; 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_2:10; then A12: (RLineXS (M1,l,k,a)) @ is Matrix of n,m,K by A3, A10, MATRIX_1:20; then consider M2 being Matrix of n,m,K such that A13: M2 = (RLineXS (M1,l,k,a)) @ ; A14: for i, j being Nat 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 be Nat; ::_thesis: ( i in dom M & j in Seg (width M) implies ( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) ) assume that A15: i in dom M and A16: j in Seg (width M) ; ::_thesis: ( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) A17: [i,j] in Indices M by A15, A16, ZFMISC_1:87; then A18: [j,i] in Indices M1 by A5, MATRIX_1:def_6; then A19: i in Seg (width M1) by ZFMISC_1:87; A20: len M1 = width M by A5, MATRIX_1: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)) ) ::_thesis: ( j <> l implies M2 * (i,j) = M * (i,j) ) proof A24: [i,k] in Indices M by A2, A15, ZFMISC_1:87; assume A25: j = l ; ::_thesis: M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) M2 * (i,j) = (RLineXS (M1,l,k,a)) * (j,i) by A13, A22, MATRIX_1: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_1:def_6 .= (a * (M * (i,k))) + (M * (i,l)) by A5, A17, A25, MATRIX_1:def_6 ; hence M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ; ::_thesis: verum end; A26: j in dom M1 by A18, ZFMISC_1:87; thus ( j <> l implies M2 * (i,j) = M * (i,j) ) ::_thesis: verum proof assume A27: j <> l ; ::_thesis: M2 * (i,j) = M * (i,j) M2 * (i,j) = (RLineXS (M1,l,k,a)) * (j,i) by A13, A22, MATRIX_1:def_6 .= M1 * (j,i) by A21, A26, A19, A27, Def3 .= M * (i,j) by A5, A17, MATRIX_1:def_6 ; hence M2 * (i,j) = M * (i,j) ; ::_thesis: verum end; end; for i, j being Nat 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_1:26; let i, j be Nat; ::_thesis: ( [i,j] in Indices (RColXS (M,l,k,a)) implies (RColXS (M,l,k,a)) * (i,j) = ((RLineXS (M1,l,k,a)) @) * (i,j) ) assume [i,j] in Indices (RColXS (M,l,k,a)) ; ::_thesis: (RColXS (M,l,k,a)) * (i,j) = ((RLineXS (M1,l,k,a)) @) * (i,j) 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 (RColXS (M,l,k,a)) * (i,j) = ((RLineXS (M1,l,k,a)) @) * (i,j) by A1, A2, A3, A4, A29, A30, A31, Def6; ::_thesis: verum end; hence (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a) by A12, MATRIX_1:27; ::_thesis: verum end; theorem :: MATRIX12:18 for l, n, k being Nat for K being Field for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k) proof 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)) & n > 0 holds A * (ICol ((1. (K,n)),l,k)) = ICol (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)) & n > 0 holds A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k) let A be Matrix of n,K; ::_thesis: ( 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) ) assume that A1: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) and A2: n > 0 ; ::_thesis: A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k) A3: len (1. (K,n)) = n by MATRIX_1:24; A4: width (1. (K,n)) = n by MATRIX_1:24; then A5: dom (1. (K,n)) = Seg (width (1. (K,n))) by A3, FINSEQ_1:def_3; A6: width (A @) = n by MATRIX_1:24; A7: ( width (ILine ((1. (K,n)),l,k)) = width (1. (K,n)) & len (A @) = n ) by Th1, MATRIX_1:24; A8: len A = n by MATRIX_1:24; A9: width A = n by MATRIX_1: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_2:13 .= A * ((ILine (((1. (K,n)) @),l,k)) @) by MATRIX_6:10 .= A * (ICol ((1. (K,n)),l,k)) by A1, A2, A5, Th15 ; hence A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k) by A1, A2, A10, Th15; ::_thesis: verum end; theorem :: MATRIX12:19 for l, n being Nat for K being Field for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) & n > 0 holds A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a) proof let l, n be Nat; ::_thesis: for K being Field for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) & n > 0 holds A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a) let K be Field; ::_thesis: for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) & n > 0 holds A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a) let a be Element of K; ::_thesis: for A being Matrix of n,K st l in dom (1. (K,n)) & n > 0 holds A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a) let A be Matrix of n,K; ::_thesis: ( l in dom (1. (K,n)) & n > 0 implies A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a) ) assume that A1: l in dom (1. (K,n)) and A2: n > 0 ; ::_thesis: A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a) A3: len (1. (K,n)) = n by MATRIX_1:24; A4: width (1. (K,n)) = n by MATRIX_1:24; then A5: dom (1. (K,n)) = Seg (width (1. (K,n))) by A3, FINSEQ_1:def_3; A6: width (A @) = n by MATRIX_1:24; A7: ( width (SXLine ((1. (K,n)),l,a)) = width (1. (K,n)) & len (A @) = n ) by Th1, MATRIX_1:24; A8: len A = n by MATRIX_1:24; A9: width A = n by MATRIX_1: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_2:13 .= A * ((SXLine (((1. (K,n)) @),l,a)) @) by MATRIX_6:10 .= A * (SXCol ((1. (K,n)),l,a)) by A1, A2, A5, Th16 ; hence A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a) by A1, A2, A10, Th16; ::_thesis: verum end; theorem :: MATRIX12:20 for l, n, k being Nat for K being Field for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a) proof let l, n, k be Nat; ::_thesis: for K being Field for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a) let K be Field; ::_thesis: for a being Element of K for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a) let a be Element of K; ::_thesis: for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a) let A be Matrix of n,K; ::_thesis: ( 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) ) assume that A1: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) and A2: n > 0 ; ::_thesis: A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a) A3: len (1. (K,n)) = n by MATRIX_1:24; A4: width (1. (K,n)) = n by MATRIX_1:24; then A5: dom (1. (K,n)) = Seg (width (1. (K,n))) by A3, FINSEQ_1:def_3; A6: width (A @) = n by MATRIX_1:24; A7: ( width (RLineXS ((1. (K,n)),l,k,a)) = width (1. (K,n)) & len (A @) = n ) by Th1, MATRIX_1:24; A8: len A = n by MATRIX_1:24; A9: width A = n by MATRIX_1: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_2:13 .= 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 A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a) by A1, A2, A10, Th17; ::_thesis: verum end; theorem :: MATRIX12:21 for l, n, k being Nat for K being Field st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds (ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k) proof let l, n, k be Nat; ::_thesis: for K being Field st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds (ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k) let K be Field; ::_thesis: ( 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) ) assume that A1: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) and A2: n > 0 ; ::_thesis: (ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k) A3: (ILine ((1. (K,n)),l,k)) ~ = ILine ((1. (K,n)),l,k) by A1, Th12; ( len (1. (K,n)) = n & width (1. (K,n)) = n ) by MATRIX_1: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 A1, A2, A3, Th12, MATRIX_6:13 .= ((ILine (((1. (K,n)) @),l,k)) @) ~ by MATRIX_6:10 .= (ICol ((1. (K,n)),l,k)) ~ by A1, A2, A4, Th15 ; hence (ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k) ; ::_thesis: verum end; theorem :: MATRIX12:22 for l, n, k being Nat for K being Field for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l & n > 0 holds (RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a)) proof let l, n, k be Nat; ::_thesis: for K being Field for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l & n > 0 holds (RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a)) let K be Field; ::_thesis: for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l & n > 0 holds (RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a)) let a be Element of K; ::_thesis: ( 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)) ) assume that A1: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) and A2: k <> l and A3: n > 0 ; ::_thesis: (RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a)) A4: (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) by A1, A2, Th13; ( len (1. (K,n)) = n & width (1. (K,n)) = n ) by MATRIX_1: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 A1, A2, A3, A4, Th13, MATRIX_6:13 .= ((RLineXS (((1. (K,n)) @),l,k,a)) @) ~ by MATRIX_6:10 .= (RColXS ((1. (K,n)),l,k,a)) ~ by A1, A3, A5, Th17 ; hence (RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a)) ; ::_thesis: verum end; theorem :: MATRIX12:23 for l, n being Nat for K being Field for a being Element of K st l in dom (1. (K,n)) & a <> 0. K & n > 0 holds (SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a ")) proof let l, n be Nat; ::_thesis: for K being Field for a being Element of K st l in dom (1. (K,n)) & a <> 0. K & n > 0 holds (SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a ")) let K be Field; ::_thesis: for a being Element of K st l in dom (1. (K,n)) & a <> 0. K & n > 0 holds (SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a ")) let a be Element of K; ::_thesis: ( l in dom (1. (K,n)) & a <> 0. K & n > 0 implies (SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a ")) ) assume that A1: l in dom (1. (K,n)) and A2: a <> 0. K and A3: n > 0 ; ::_thesis: (SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a ")) A4: (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) by A1, A2, Th14; ( len (1. (K,n)) = n & width (1. (K,n)) = n ) by MATRIX_1: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 A1, A2, A3, A4, Th14, MATRIX_6:13 .= ((SXLine (((1. (K,n)) @),l,a)) @) ~ by MATRIX_6:10 .= (SXCol ((1. (K,n)),l,a)) ~ by A1, A3, A5, Th16 ; hence (SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a ")) ; ::_thesis: verum end;