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 ) )
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:
(
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 ) ) ) )
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
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:
theorem Th2:
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 ) )
theorem Th3:
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 ) )
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:
(
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 ) ) ) )
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
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:
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 ) )
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 ) )
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:
(
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 ) ) ) )
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
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:
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 ) )
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:
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
theorem Th7:
theorem Th8:
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
theorem
theorem
theorem Th11:
theorem Th12:
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 )
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
theorem Th13:
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) )
theorem Th14:
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 " ) )
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:
(
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 ) ) ) )
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
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:
(
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 ) ) ) )
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
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:
(
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 ) ) ) )
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
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;
let a be
Element of
K;
synonym RColXS M,
l,
k,
a for RcolXScalar M,
l,
k,
a;
end;
theorem Th15:
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
theorem Th16:
theorem Th17:
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
theorem
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
theorem
theorem
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
theorem
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
theorem
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)
theorem