:: Some Properties of Line and Column Operations on Matrices
:: by Xiquan Liang , Tao Sun and Dahai Hu
::
:: Copyright (c) 2007-2019 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 () & 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 () 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 () 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 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 () 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 () 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 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 () 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 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 () 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 () & 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 () 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 () holds
( ( i = l implies b1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) )
proof 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 () 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 () holds
( ( i = l implies b2 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds
b1 = b2
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 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 () 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 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 () & 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 () 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 () holds
( ( i = l implies b1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) )
proof 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 () 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 () 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 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 () 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 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 () and
A2: k in Seg () 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 () 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 () 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 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 () 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 () 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 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 () & k in Seg () & 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 () 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 () 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 () 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 () holds
( ( j = l implies b1 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) )
proof 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 () 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 () holds
( ( j = l implies b2 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds
b1 = b2
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 () & 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 () 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 () and
A2: k in Seg () 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 () 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 () holds
( ( j = l implies b1 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) )
proof 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 () 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 () 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 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 () & k in Seg () & 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 () 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 k, l, n, m being Nat
for K being Field
for M, M1 being Matrix of n,m,K st l in Seg () & k in Seg () & 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 () & 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 () & k in Seg () & 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;