MATRIX12: Some Properties of Line and Column Operations on Matrices

:: Some Properties of Line and Column Operations on Matrices
:: by Xiquan Liang , Tao Sun and Dahai Hu
::
:: Received August 13, 2007
:: Copyright (c) 2007-2011 Association of Mizar Users

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

proof end;

proof end;

end;

:: deftheorem Def1 defines InterchangeLine MATRIX12:def 1 :

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

proof end;

proof end;

end;

:: deftheorem Def2 defines ScalarXLine MATRIX12:def 2 :

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

proof end;

proof end;

end;

:: deftheorem Def3 defines RlineXScalar MATRIX12:def 3 :

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

proof end;

proof end;

end;

:: deftheorem Def4 defines InterchangeCol MATRIX12:def 4 :

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

proof end;

proof end;

end;

:: deftheorem Def5 defines ScalarXCol MATRIX12:def 5 :

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

proof end;

proof end;

end;

:: deftheorem Def6 defines RcolXScalar MATRIX12:def 6 :

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