:: Matrices.
:: by Katarzyna Jankowska
::
:: Copyright (c) 1991-2017 Association of Mizar Users

definition
let f be FinSequence;
attr f is tabular means :Def1: :: MATRIX_0:def 1
ex n being Nat st
for x being object st x in rng f holds
ex s being FinSequence st
( s = x & len s = n );
end;

:: deftheorem Def1 defines tabular MATRIX_0:def 1 :
for f being FinSequence holds
( f is tabular iff ex n being Nat st
for x being object st x in rng f holds
ex s being FinSequence st
( s = x & len s = n ) );

registration
existence
ex b1 being FinSequence st b1 is tabular
proof end;
end;

theorem Th1: :: MATRIX_0:1
for D being non empty set
for d being Element of D holds is tabular
proof end;

theorem Th2: :: MATRIX_0:2
for x being object
for n, m being Nat holds m |-> (n |-> x) is tabular
proof end;

theorem Th3: :: MATRIX_0:3
for s being FinSequence holds <*s*> is tabular
proof end;

theorem Th4: :: MATRIX_0:4
for n being Nat
for s1, s2 being FinSequence st len s1 = n & len s2 = n holds
<*s1,s2*> is tabular
proof end;

theorem Th5: :: MATRIX_0:5
proof end;

theorem :: MATRIX_0:6
is tabular by ;

theorem :: MATRIX_0:7
for D being non empty set
for a1, a2 being Element of D holds <*<*a1*>,<*a2*>*> is tabular
proof end;

theorem :: MATRIX_0:8
for D being non empty set
for a1, a2, b1, b2 being Element of D holds <*<*a1,a2*>,<*b1,b2*>*> is tabular
proof end;

registration
let D be set ;
existence
ex b1 being FinSequence of D * st b1 is tabular
proof end;
end;

definition
let D be set ;
mode Matrix of D is tabular FinSequence of D * ;
end;

registration
let X be set ;
coherence
for b1 being Matrix of X holds b1 is Function-yielding
;
end;

registration
let D be non empty set ;
existence
not for b1 being Matrix of D holds b1 is empty-yielding
proof end;
end;

theorem Th9: :: MATRIX_0:9
for D being non empty set
for s being FinSequence holds
( s is Matrix of D iff ex n being Nat st
for x being object st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) )
proof end;

definition
let D be non empty set ;
let m, n be Nat;
let M be Matrix of D;
attr M is m,n -size means :Def2: :: MATRIX_0:def 2
( len M = m & ( for p being FinSequence of D st p in rng M holds
len p = n ) );
end;

:: deftheorem Def2 defines -size MATRIX_0:def 2 :
for D being non empty set
for m, n being Nat
for M being Matrix of D holds
( M is m,n -size iff ( len M = m & ( for p being FinSequence of D st p in rng M holds
len p = n ) ) );

registration
let D be non empty set ;
let m, n be Nat;
existence
ex b1 being Matrix of D st b1 is m,n -size
proof end;
end;

definition
let D be non empty set ;
let m, n be Nat;
mode Matrix of m,n,D is m,n -size Matrix of D;
end;

definition
let D be non empty set ;
let n be Nat;
mode Matrix of n,D is Matrix of n,n,D;
end;

theorem Th10: :: MATRIX_0:10
for n, m being Nat
for D being non empty set
for a being Element of D holds m |-> (n |-> a) is Matrix of m,n,D
proof end;

theorem Th11: :: MATRIX_0:11
for D being non empty set
for p being FinSequence of D holds <*p*> is Matrix of 1, len p,D
proof end;

theorem Th12: :: MATRIX_0:12
for n being Nat
for D being non empty set
for p1, p2 being FinSequence of D st len p1 = n & len p2 = n holds
<*p1,p2*> is Matrix of 2,n,D
proof end;

theorem Th13: :: MATRIX_0:13
for m being Nat
for D being non empty set holds {} is Matrix of 0 ,m,D
proof end;

theorem :: MATRIX_0:14
for D being non empty set holds is Matrix of 1, 0 ,D
proof end;

theorem :: MATRIX_0:15
for D being non empty set
for a being Element of D holds is Matrix of 1,D
proof end;

theorem :: MATRIX_0:16
for D being non empty set holds is Matrix of 2, 0 ,D
proof end;

theorem :: MATRIX_0:17
for D being non empty set
for a1, a2 being Element of D holds <*<*a1,a2*>*> is Matrix of 1,2,D
proof end;

theorem :: MATRIX_0:18
for D being non empty set
for a1, a2 being Element of D holds <*<*a1*>,<*a2*>*> is Matrix of 2,1,D
proof end;

theorem Th19: :: MATRIX_0:19
for D being non empty set
for a1, a2, b1, b2 being Element of D holds <*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D
proof end;

definition
let M be tabular FinSequence;
func width M -> Nat means :Def3: :: MATRIX_0:def 3
ex s being FinSequence st
( s in rng M & len s = it ) if len M > 0
otherwise it = 0 ;
existence
( ( len M > 0 implies ex b1 being Nat ex s being FinSequence st
( s in rng M & len s = b1 ) ) & ( not len M > 0 implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( len M > 0 & ex s being FinSequence st
( s in rng M & len s = b1 ) & ex s being FinSequence st
( s in rng M & len s = b2 ) implies b1 = b2 ) & ( not len M > 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Nat holds verum
;
end;

:: deftheorem Def3 defines width MATRIX_0:def 3 :
for M being tabular FinSequence
for b2 being Nat holds
( ( len M > 0 implies ( b2 = width M iff ex s being FinSequence st
( s in rng M & len s = b2 ) ) ) & ( not len M > 0 implies ( b2 = width M iff b2 = 0 ) ) );

theorem Th20: :: MATRIX_0:20
for D being non empty set
for M being Matrix of D st len M > 0 holds
for n being Nat holds
( M is Matrix of len M,n,D iff n = width M )
proof end;

definition
let M be tabular FinSequence;
func Indices M -> set equals :: MATRIX_0:def 4
[:(dom M),(Seg ()):];
coherence
[:(dom M),(Seg ()):] is set
;
end;

:: deftheorem defines Indices MATRIX_0:def 4 :
for M being tabular FinSequence holds Indices M = [:(dom M),(Seg ()):];

definition
let D be set ;
let M be Matrix of D;
let i, j be Nat;
assume A1: [i,j] in Indices M ;
func M * (i,j) -> Element of D means :Def5: :: MATRIX_0:def 5
ex p being FinSequence of D st
( p = M . i & it = p . j );
existence
ex b1 being Element of D ex p being FinSequence of D st
( p = M . i & b1 = p . j )
proof end;
uniqueness
for b1, b2 being Element of D st ex p being FinSequence of D st
( p = M . i & b1 = p . j ) & ex p being FinSequence of D st
( p = M . i & b2 = p . j ) holds
b1 = b2
;
end;

:: deftheorem Def5 defines * MATRIX_0:def 5 :
for D being set
for M being Matrix of D
for i, j being Nat st [i,j] in Indices M holds
for b5 being Element of D holds
( b5 = M * (i,j) iff ex p being FinSequence of D st
( p = M . i & b5 = p . j ) );

theorem Th21: :: MATRIX_0:21
for D being non empty set
for M1, M2 being Matrix of D st len M1 = len M2 & width M1 = width M2 & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) holds
M1 = M2
proof end;

scheme :: MATRIX_0:sch 1
MatrixLambda{ F1() -> non empty set , F2() -> Nat, F3() -> Nat, F4( set , set ) -> Element of F1() } :
ex M being Matrix of F2(),F3(),F1() st
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = F4(i,j)
proof end;

scheme :: MATRIX_0:sch 2
MatrixEx{ F1() -> non empty set , F2() -> Nat, F3() -> Nat, P1[ object , object , object ] } :
ex M being Matrix of F2(),F3(),F1() st
for i, j being Nat st [i,j] in Indices M holds
P1[i,j,M * (i,j)]
provided
A1: for i, j being Nat st [i,j] in [:(Seg F2()),(Seg F3()):] holds
ex x being Element of F1() st P1[i,j,x]
proof end;

theorem :: MATRIX_0:22
for m being Nat
for D being non empty set
for M being Matrix of 0 ,m,D holds
( len M = 0 & width M = 0 & Indices M = {} )
proof end;

theorem Th23: :: MATRIX_0:23
for n, m being Nat
for D being non empty set st n > 0 holds
for M being Matrix of n,m,D holds
( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] )
proof end;

theorem Th24: :: MATRIX_0:24
for n being Nat
for D being non empty set
for M being Matrix of n,D holds
( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] )
proof end;

theorem Th25: :: MATRIX_0:25
for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D holds
( len M = n & Indices M = [:(Seg n),(Seg ()):] )
proof end;

theorem :: MATRIX_0:26
for n, m being Nat
for D being non empty set
for M1, M2 being Matrix of n,m,D holds Indices M1 = Indices M2
proof end;

theorem :: MATRIX_0:27
for n, m being Nat
for D being non empty set
for M1, M2 being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) holds
M1 = M2
proof end;

theorem :: MATRIX_0:28
for n being Nat
for D being non empty set
for M1 being Matrix of n,D
for i, j being Nat st [i,j] in Indices M1 holds
[j,i] in Indices M1
proof end;

definition
let D be non empty set ;
let M be Matrix of D;
func M @ -> Matrix of D means :Def6: :: MATRIX_0:def 6
( len it = width M & ( for i, j being Nat holds
( [i,j] in Indices it iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
it * (i,j) = M * (j,i) ) );
existence
ex b1 being Matrix of D st
( len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) )
proof end;
uniqueness
for b1, b2 being Matrix of D st len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) & len b2 = width M & ( for i, j being Nat holds
( [i,j] in Indices b2 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b2 * (i,j) = M * (j,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines @ MATRIX_0:def 6 :
for D being non empty set
for M, b3 being Matrix of D holds
( b3 = M @ iff ( len b3 = width M & ( for i, j being Nat holds
( [i,j] in Indices b3 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b3 * (i,j) = M * (j,i) ) ) );

theorem Th29: :: MATRIX_0:29
for D being non empty set
for M being Matrix of D st width M > 0 holds
( len (M @) = width M & width (M @) = len M )
proof end;

registration
let n be Nat;
let D be non empty set ;
let M be Matrix of n,D;
cluster M @ -> n,n -size ;
coherence
M @ is n,n -size
proof end;
end;

definition
let D be non empty set ;
let M be Matrix of D;
let i be Nat;
func Line (M,i) -> FinSequence of D means :Def7: :: MATRIX_0:def 7
( len it = width M & ( for j being Nat st j in Seg () holds
it . j = M * (i,j) ) );
existence
ex b1 being FinSequence of D st
( len b1 = width M & ( for j being Nat st j in Seg () holds
b1 . j = M * (i,j) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of D st len b1 = width M & ( for j being Nat st j in Seg () holds
b1 . j = M * (i,j) ) & len b2 = width M & ( for j being Nat st j in Seg () holds
b2 . j = M * (i,j) ) holds
b1 = b2
proof end;
func Col (M,i) -> FinSequence of D means :Def8: :: MATRIX_0:def 8
( len it = len M & ( for j being Nat st j in dom M holds
it . j = M * (j,i) ) );
existence
ex b1 being FinSequence of D st
( len b1 = len M & ( for j being Nat st j in dom M holds
b1 . j = M * (j,i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of D st len b1 = len M & ( for j being Nat st j in dom M holds
b1 . j = M * (j,i) ) & len b2 = len M & ( for j being Nat st j in dom M holds
b2 . j = M * (j,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Line MATRIX_0:def 7 :
for D being non empty set
for M being Matrix of D
for i being Nat
for b4 being FinSequence of D holds
( b4 = Line (M,i) iff ( len b4 = width M & ( for j being Nat st j in Seg () holds
b4 . j = M * (i,j) ) ) );

:: deftheorem Def8 defines Col MATRIX_0:def 8 :
for D being non empty set
for M being Matrix of D
for i being Nat
for b4 being FinSequence of D holds
( b4 = Col (M,i) iff ( len b4 = len M & ( for j being Nat st j in dom M holds
b4 . j = M * (j,i) ) ) );

definition
let D be non empty set ;
let M be Matrix of D;
let i be Nat;
:: original: Line
redefine func Line (M,i) -> Element of () -tuples_on D;
coherence
Line (M,i) is Element of () -tuples_on D
proof end;
:: original: Col
redefine func Col (M,i) -> Element of (len M) -tuples_on D;
coherence
Col (M,i) is Element of (len M) -tuples_on D
proof end;
end;

theorem Th30: :: MATRIX_0:30
for D being set
for i, j being Nat
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
[i,j] in Indices M
proof end;

theorem :: MATRIX_0:31
for i, j, n, m being Nat
for D being non empty set
for M being Matrix of n,m,D st 1 <= i & i <= n & 1 <= j & j <= m holds
[i,j] in Indices M
proof end;

:: from GOBOARD5, 2008.03.08, A.T.
theorem Th32: :: MATRIX_0:32
for M being tabular FinSequence
for i, j being Nat st [i,j] in Indices M holds
( 1 <= i & i <= len M & 1 <= j & j <= width M )
proof end;

theorem :: MATRIX_0:33
for i, j, n, m being Nat
for D being non empty set
for M being Matrix of n,m,D st [i,j] in Indices M holds
( 1 <= i & i <= n & 1 <= j & j <= m )
proof end;

:: from GOBRD13, 2011.07.26, A.T.
definition
let F be Function-yielding Function;
func Values F -> set equals :: MATRIX_0:def 9
Union (rngs F);
correctness
coherence
Union (rngs F) is set
;
;
end;

:: deftheorem defines Values MATRIX_0:def 9 :
for F being Function-yielding Function holds Values F = Union (rngs F);

theorem Th34: :: MATRIX_0:34
for i being Nat
for D being non empty set
for M being FinSequence of D * holds M . i is FinSequence of D
proof end;

theorem Th35: :: MATRIX_0:35
for D being non empty set
for M being FinSequence of D * holds Values M = union { (rng f) where f is Element of D * : f in rng M }
proof end;

registration
let D be non empty set ;
let M be FinSequence of D * ;
coherence
Values M is finite
proof end;
end;

theorem Th36: :: MATRIX_0:36
for i being Nat
for D being non empty set
for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f holds
len f = width M
proof end;

theorem Th37: :: MATRIX_0:37
for i, j being Nat
for D being non empty set
for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f & j in dom f holds
[i,j] in Indices M
proof end;

theorem Th38: :: MATRIX_0:38
for i, j being Nat
for D being non empty set
for f being FinSequence of D
for M being Matrix of D st [i,j] in Indices M & M . i = f holds
( len f = width M & j in dom f )
proof end;

theorem Th39: :: MATRIX_0:39
for D being non empty set
for M being Matrix of D holds Values M = { (M * (i,j)) where i, j is Nat : [i,j] in Indices M }
proof end;

theorem :: MATRIX_0:40
for D being non empty set
for M being Matrix of D holds card () <= (len M) * ()
proof end;

theorem :: MATRIX_0:41
for D being non empty set
for i, j being Nat
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
M * (i,j) in Values M
proof end;

:: from GOBOARD1, 2012.02.25, A.T.
theorem Th42: :: MATRIX_0:42
for D being non empty set
for M being Matrix of D
for i, j being Nat st j in dom M & i in Seg () holds
(Col (M,i)) . j = (Line (M,j)) . i
proof end;

definition
let D be non empty set ;
let M be Matrix of D;
:: original: empty-yielding
redefine attr M is empty-yielding means :: MATRIX_0:def 10
( 0 = len M or 0 = width M );
compatibility
( M is empty-yielding iff ( 0 = len M or 0 = width M ) )
proof end;
end;

:: deftheorem defines empty-yielding MATRIX_0:def 10 :
for D being non empty set
for M being Matrix of D holds
( M is empty-yielding iff ( 0 = len M or 0 = width M ) );

theorem Th43: :: MATRIX_0:43
for n, m being Nat
for D being non empty set
for f being FinSequence of D
for i, k being Nat
for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
proof end;

theorem :: MATRIX_0:44
for D being non empty set
for M being Matrix of D holds
( M is V3() iff ( 0 < len M & 0 < width M ) ) ;

theorem :: MATRIX_0:45
for n, m being Nat
for D being non empty set
for M1 being Matrix of 0 ,n,D
for M2 being Matrix of 0 ,m,D holds M1 = M2
proof end;

definition
let n, m be Nat;
let a be object ;
func (n,m) --> a -> tabular FinSequence equals :: MATRIX_0:def 11
n |-> (m |-> a);
coherence
n |-> (m |-> a) is tabular FinSequence
by Th2;
end;

:: deftheorem defines --> MATRIX_0:def 11 :
for n, m being Nat
for a being object holds (n,m) --> a = n |-> (m |-> a);

definition
let D be non empty set ;
let n, m be Nat;
let d be Element of D;
:: original: -->
redefine func (n,m) --> d -> Matrix of n,m,D;
coherence
(n,m) --> d is Matrix of n,m,D
by Th10;
end;

theorem :: MATRIX_0:46
for i, j, n, m being Nat
for D being non empty set
for a being Element of D st [i,j] in Indices ((n,m) --> a) holds
((n,m) --> a) * (i,j) = a
proof end;

definition
let a, b, c, d be object ;
func (a,b) ][ (c,d) -> tabular FinSequence equals :: MATRIX_0:def 12
<*<*a,b*>,<*c,d*>*>;
correctness
coherence
<*<*a,b*>,<*c,d*>*> is tabular FinSequence
;
proof end;
end;

:: deftheorem defines ][ MATRIX_0:def 12 :
for a, b, c, d being object holds (a,b) ][ (c,d) = <*<*a,b*>,<*c,d*>*>;

theorem Th47: :: MATRIX_0:47
for x1, x2, y1, y2 being object holds
( len ((x1,x2) ][ (y1,y2)) = 2 & width ((x1,x2) ][ (y1,y2)) = 2 & Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] )
proof end;

theorem Th48: :: MATRIX_0:48
for x1, x2, y1, y2 being object holds
( [1,1] in Indices ((x1,x2) ][ (y1,y2)) & [1,2] in Indices ((x1,x2) ][ (y1,y2)) & [2,1] in Indices ((x1,x2) ][ (y1,y2)) & [2,2] in Indices ((x1,x2) ][ (y1,y2)) )
proof end;

definition
let D be non empty set ;
let a be Element of D;
:: original: <*
redefine func <*a*> -> Element of 1 -tuples_on D;
coherence
<*a*> is Element of 1 -tuples_on D
by FINSEQ_2:98;
end;

definition
let D be non empty set ;
let n be Nat;
let p be Element of n -tuples_on D;
:: original: <*
redefine func <*p*> -> Matrix of 1,n,D;
coherence
<*p*> is Matrix of 1,n,D
proof end;
end;

theorem :: MATRIX_0:49
for D being non empty set
for a being Element of D holds
( [1,1] in Indices & * (1,1) = a )
proof end;

definition
let D be non empty set ;
let a, b, c, d be Element of D;
:: original: ][
redefine func (a,b) ][ (c,d) -> Matrix of 2,D;
coherence
(a,b) ][ (c,d) is Matrix of 2,D
by Th19;
end;

theorem :: MATRIX_0:50
for D being non empty set
for a, b, c, d being Element of D holds
( ((a,b) ][ (c,d)) * (1,1) = a & ((a,b) ][ (c,d)) * (1,2) = b & ((a,b) ][ (c,d)) * (2,1) = c & ((a,b) ][ (c,d)) * (2,2) = d )
proof end;

theorem :: MATRIX_0:51
for n being Nat
for D being non empty set
for M being Matrix of D st len M = n holds
M is Matrix of n, width M,D
proof end;

theorem Th52: :: MATRIX_0:52
for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D
for k being Nat st k in Seg n holds
M . k = Line (M,k)
proof end;

Lm1: for D being non empty set
for M being Matrix of D
for k being Nat st k in dom M holds
M . k = Line (M,k)

proof end;

definition
let i be Nat;
let D be non empty set ;
let M be Matrix of D;
func DelCol (M,i) -> Matrix of D means :Def13: :: MATRIX_0:def 13
( len it = len M & ( for k being Nat st k in dom M holds
it . k = Del ((Line (M,k)),i) ) );
existence
ex b1 being Matrix of D st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) )
proof end;
uniqueness
for b1, b2 being Matrix of D st len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) & len b2 = len M & ( for k being Nat st k in dom M holds
b2 . k = Del ((Line (M,k)),i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines DelCol MATRIX_0:def 13 :
for i being Nat
for D being non empty set
for M, b4 being Matrix of D holds
( b4 = DelCol (M,i) iff ( len b4 = len M & ( for k being Nat st k in dom M holds
b4 . k = Del ((Line (M,k)),i) ) ) );

theorem Th53: :: MATRIX_0:53
for D being non empty set
for M1, M2 being Matrix of D st M1 @ = M2 @ & len M1 = len M2 holds
M1 = M2
proof end;

theorem Th54: :: MATRIX_0:54
for D being non empty set
for M being Matrix of D st width M > 0 holds
( len (M @) = width M & width (M @) = len M )
proof end;

theorem :: MATRIX_0:55
for D being non empty set
for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 & M1 @ = M2 @ holds
M1 = M2
proof end;

theorem :: MATRIX_0:56
for D being non empty set
for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 holds
( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) )
proof end;

theorem Th57: :: MATRIX_0:57
for D being non empty set
for M being Matrix of D st len M > 0 & width M > 0 holds
(M @) @ = M
proof end;

theorem Th58: :: MATRIX_0:58
for D being non empty set
for M being Matrix of D
for i being Nat st i in dom M holds
Line (M,i) = Col ((M @),i)
proof end;

theorem :: MATRIX_0:59
for D being non empty set
for M being Matrix of D
for j being Nat st j in Seg () holds
Line ((M @),j) = Col (M,j)
proof end;

theorem Th60: :: MATRIX_0:60
for D being non empty set
for M being Matrix of D
for i being Nat st i in dom M holds
M . i = Line (M,i)
proof end;

notation
let D be non empty set ;
let i be Nat;
let M be Matrix of D;
synonym DelLine (M,i) for Del (i,D);
end;

registration
let D be non empty set ;
let i be Nat;
let M be Matrix of D;
cluster DelLine (,M) -> tabular ;
coherence
DelLine (,M) is tabular
proof end;
end;

definition
let D be non empty set ;
let i be Nat;
let M be Matrix of D;
:: original: DelLine
redefine func DelLine (M,i) -> Matrix of D;
coherence
DelLine (,M) is Matrix of D
by FINSEQ_3:105;
end;

definition
let i, j, n be Nat;
let D be non empty set ;
let M be Matrix of n,D;
func Deleting (M,i,j) -> Matrix of D equals :: MATRIX_0:def 14
DelCol ((DelLine (M,i)),j);
coherence
DelCol ((DelLine (M,i)),j) is Matrix of D
;
end;

:: deftheorem defines Deleting MATRIX_0:def 14 :
for i, j, n being Nat
for D being non empty set
for M being Matrix of n,D holds Deleting (M,i,j) = DelCol ((DelLine (M,i)),j);

theorem :: MATRIX_0:61
for D being non empty set
for M being Matrix of D
for i being Nat st not i in Seg () holds
DelCol (M,i) = M
proof end;

:: from GOBOARD1, 2012.03.01, A.T.
theorem Th62: :: MATRIX_0:62
for D being non empty set
for G being Matrix of D
for i, k being Nat st k in dom G holds
Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i)
proof end;

theorem Th63: :: MATRIX_0:63
for D being non empty set
for G being Matrix of D
for i, m being Nat st i in Seg () & width G = m + 1 holds
width (DelCol (G,i)) = m
proof end;

theorem Th64: :: MATRIX_0:64
for D being non empty set
for G being Matrix of D
for i being Nat st i in Seg () & width G > 0 holds
width G = (width (DelCol (G,i))) + 1
proof end;

theorem :: MATRIX_0:65
for D being non empty set
for G being Matrix of D
for i being Nat st width G > 1 & i in Seg () holds
not DelCol (G,i) is V3()
proof end;

theorem Th66: :: MATRIX_0:66
for D being non empty set
for G being Matrix of D
for i, n, m being Nat st i in Seg () & width G > 1 & n in dom G & m in Seg (width (DelCol (G,i))) holds
(DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m
proof end;

theorem Th67: :: MATRIX_0:67
for D being non empty set
for G being Matrix of D
for i, k, m being Nat st i in Seg () & width G = m + 1 & m > 0 & 1 <= k & k < i holds
( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg () )
proof end;

theorem Th68: :: MATRIX_0:68
for D being non empty set
for G being Matrix of D
for i, k, m being Nat st i in Seg () & width G = m + 1 & m > 0 & i <= k & k <= m holds
( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg () )
proof end;

theorem Th69: :: MATRIX_0:69
for D being non empty set
for G being Matrix of D
for i, k, n, m being Nat st i in Seg () & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i holds
( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg () )
proof end;

theorem Th70: :: MATRIX_0:70
for D being non empty set
for G being Matrix of D
for i, k, n, m being Nat st i in Seg () & width G = m + 1 & m > 0 & n in dom G & i <= k & k <= m holds
( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 in Seg () )
proof end;

theorem :: MATRIX_0:71
for D being non empty set
for G being Matrix of D
for k, m being Nat st width G = m + 1 & m > 0 & k in Seg m holds
( Col ((DelCol (G,1)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,1))) & k + 1 in Seg () )
proof end;

theorem :: MATRIX_0:72
for D being non empty set
for G being Matrix of D
for k, n, m being Nat st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds
( (DelCol (G,1)) * (n,k) = G * (n,(k + 1)) & 1 in Seg () )
proof end;

theorem :: MATRIX_0:73
for D being non empty set
for G being Matrix of D
for k, m being Nat st width G = m + 1 & m > 0 & k in Seg m holds
( Col ((DelCol (G,())),k) = Col (G,k) & k in Seg (width (DelCol (G,()))) )
proof end;

theorem :: MATRIX_0:74
for D being non empty set
for G being Matrix of D
for k, n, m being Nat st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds
( k in Seg () & (DelCol (G,())) * (n,k) = G * (n,k) & width G in Seg () )
proof end;

theorem :: MATRIX_0:75
for i, n being Nat
for D being non empty set
for m being Nat
for f being FinSequence of D
for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg () & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))
proof end;