:: 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;