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 Association of Mizar Users

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;

uniqueness

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;

uniqueness

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 & a <> 0. K & 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 & l 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: ( l in dom M & 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;

uniqueness

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) & a <> 0. K 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 A1: ( l in Seg (width M) & k in Seg (width M) & n > 0 & 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;

uniqueness

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 A1: ( l in Seg (width M) & n > 0 & 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;

uniqueness

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 A1: ( l in Seg (width M) & k in Seg (width M) & n > 0 & 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;

uniqueness

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) & a <> 0. K & 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) & a <> 0. K & 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;