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

Lm1: for n, m 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
ex b₁ being Matrix of n,m,K st
( len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₁ * (i,j) = M * (k,j) ) & ( i = k implies b₁ * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b₁ * (i,j) = M * (i,j) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of n,m,K st len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₁ * (i,j) = M * (k,j) ) & ( i = k implies b₁ * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b₁ * (i,j) = M * (i,j) ) ) ) & len b₂ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₂ * (i,j) = M * (k,j) ) & ( i = k implies b₂ * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b₂ * (i,j) = M * (i,j) ) ) ) holds
b₁ = b₂

proof 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 b₇ being Matrix of n,m,K holds
( b₇ = InterchangeLine (M,l,k) iff ( len b₇ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₇ * (i,j) = M * (k,j) ) & ( i = k implies b₇ * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b₇ * (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 end;

theorem Th2: :: MATRIX12:2

for k, l, n, m 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 n, m 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 n, m 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
ex b₁ being Matrix of n,m,K st
( len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₁ * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b₁ * (i,j) = M * (i,j) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of n,m,K st len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₁ * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b₁ * (i,j) = M * (i,j) ) ) ) & len b₂ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₂ * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b₂ * (i,j) = M * (i,j) ) ) ) holds
b₁ = b₂

proof 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 b₇ being Matrix of n,m,K holds
( b₇ = ScalarXLine (M,l,a) iff ( len b₇ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₇ * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b₇ * (i,j) = M * (i,j) ) ) ) ) );

theorem Th4: :: MATRIX12:4

for l, n, m, 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 j, k, l, n, m, i 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
ex b₁ being Matrix of n,m,K st
( len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₁ * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b₁ * (i,j) = M * (i,j) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of n,m,K st len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₁ * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b₁ * (i,j) = M * (i,j) ) ) ) & len b₂ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₂ * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b₂ * (i,j) = M * (i,j) ) ) ) holds
b₁ = b₂

proof 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 b₈ being Matrix of n,m,K holds
( b₈ = RlineXScalar (M,l,k,a) iff ( len b₈ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₈ * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b₈ * (i,j) = M * (i,j) ) ) ) ) );

theorem Th5: :: MATRIX12:5

for k, l, n, m, 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 k, l, n 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 k, 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)) & 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 k, n, m 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 k, l, n, m 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 k, l, n, m 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 k, l, n 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 k, l, n 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
ex b₁ being Matrix of n,m,K st
( len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₁ * (i,j) = M * (i,k) ) & ( j = k implies b₁ * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b₁ * (i,j) = M * (i,j) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of n,m,K st len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₁ * (i,j) = M * (i,k) ) & ( j = k implies b₁ * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b₁ * (i,j) = M * (i,j) ) ) ) & len b₂ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₂ * (i,j) = M * (i,k) ) & ( j = k implies b₂ * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b₂ * (i,j) = M * (i,j) ) ) ) holds
b₁ = b₂

proof 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 b₇ being Matrix of n,m,K holds
( b₇ = InterchangeCol (M,l,k) iff ( len b₇ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₇ * (i,j) = M * (i,k) ) & ( j = k implies b₇ * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b₇ * (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 b₁ being Matrix of n,m,K st
( len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₁ * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b₁ * (i,j) = M * (i,j) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of n,m,K st len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₁ * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b₁ * (i,j) = M * (i,j) ) ) ) & len b₂ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₂ * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b₂ * (i,j) = M * (i,j) ) ) ) holds
b₁ = b₂

proof 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 b₇ being Matrix of n,m,K holds
( b₇ = ScalarXCol (M,l,a) iff ( len b₇ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₇ * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b₇ * (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 b₁ being Matrix of n,m,K st
( len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₁ * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b₁ * (i,j) = M * (i,j) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of n,m,K st len b₁ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₁ * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b₁ * (i,j) = M * (i,j) ) ) ) & len b₂ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₂ * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b₂ * (i,j) = M * (i,j) ) ) ) holds
b₁ = b₂

proof 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 b₈ being Matrix of n,m,K holds
( b₈ = RcolXScalar (M,l,k,a) iff ( len b₈ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₈ * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b₈ * (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 k, l, 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 k, 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) & 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 k, l, n 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 k, 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)) & 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 k, l, n 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 k, l, n 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;