:: Matrices.
:: by Katarzyna Jankowska
::
:: Received June 8, 1991
:: Copyright (c) 1991-2021 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

cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V103() tabular for set ;

existence
ex b₁ being FinSequence st b₁ is tabular

proof end;

end;

theorem Th1: :: MATRIX_0:1

for D being non empty set
for d being Element of D holds <*<*d*>*> 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

{} is tabular

proof end;

theorem :: MATRIX_0:6

<*{},{}*> is tabular by Th4, CARD_1:27;

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 ;

cluster Relation-like NAT -defined D * -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like V102() V103() tabular for FinSequence of D * ;

existence
ex b₁ being FinSequence of D * st b₁ 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 ;

cluster tabular -> Function-yielding for FinSequence of X * ;

coherence
for b₁ being Matrix of X holds b₁ is Function-yielding ;

end;

registration

let D be non empty set ;

cluster Relation-like non empty-yielding NAT -defined D * -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like V102() V103() tabular for FinSequence of D * ;

existence
not for b₁ being Matrix of D holds b₁ 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;

cluster Relation-like NAT -defined D * -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like V102() V103() tabular m,n -size for FinSequence of D * ;

existence
ex b₁ being Matrix of D st b₁ 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 <*<*a*>*> 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 b₁ being Nat ex s being FinSequence st
( s in rng M & len s = b₁ ) ) & ( not len M > 0 implies ex b₁ being Nat st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Nat holds
( ( len M > 0 & ex s being FinSequence st
( s in rng M & len s = b₁ ) & ex s being FinSequence st
( s in rng M & len s = b₂ ) implies b₁ = b₂ ) & ( not len M > 0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Nat holds verum ;

end;

:: deftheorem Def3 defines width MATRIX_0:def 3 :
for M being tabular FinSequence
for b₂ being Nat holds
( ( len M > 0 implies ( b₂ = width M iff ex s being FinSequence st
( s in rng M & len s = b₂ ) ) ) & ( not len M > 0 implies ( b₂ = width M iff b₂ = 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 (width M)):];

coherence
[:(dom M),(Seg (width M)):] is set ;

end;

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

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 b₁ being Element of D ex p being FinSequence of D st
( p = M . i & b₁ = p . j )

proof end;

uniqueness
for b₁, b₂ being Element of D st ex p being FinSequence of D st
( p = M . i & b₁ = p . j ) & ex p being FinSequence of D st
( p = M . i & b₂ = p . j ) holds
b₁ = b₂ ;

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 b₅ being Element of D holds
( b₅ = M * (i,j) iff ex p being FinSequence of D st
( p = M . i & b₅ = 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{ F₁() -> non empty set , F₂() -> Nat, F₃() -> Nat, F₄( set , set ) -> Element of F₁() } :

ex M being Matrix of F₂(),F₃(),F₁() st
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = F₄(i,j)

proof end;

scheme :: MATRIX_0:sch 2
MatrixEx{ F₁() -> non empty set , F₂() -> Nat, F₃() -> Nat, P₁[ object , object , object ] } :

ex M being Matrix of F₂(),F₃(),F₁() st
for i, j being Nat st [i,j] in Indices M holds
P₁[i,j,M * (i,j)]

provided

A1: for i, j being Nat st [i,j] in [:(Seg F₂()),(Seg F₃()):] holds
ex x being Element of F₁() st P₁[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 (width M)):] )

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 b₁ being Matrix of D st
( len b₁ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₁ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₁ * (i,j) = M * (j,i) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of D st len b₁ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₁ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₁ * (i,j) = M * (j,i) ) & len b₂ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₂ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₂ * (i,j) = M * (j,i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines @ MATRIX_0:def 6 :
for D being non empty set
for M, b₃ being Matrix of D holds
( b₃ = M @ iff ( len b₃ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₃ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₃ * (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 (width M) holds
it . j = M * (i,j) ) );

existence
ex b₁ being FinSequence of D st
( len b₁ = width M & ( for j being Nat st j in Seg (width M) holds
b₁ . j = M * (i,j) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of D st len b₁ = width M & ( for j being Nat st j in Seg (width M) holds
b₁ . j = M * (i,j) ) & len b₂ = width M & ( for j being Nat st j in Seg (width M) holds
b₂ . j = M * (i,j) ) holds
b₁ = b₂

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 b₁ being FinSequence of D st
( len b₁ = len M & ( for j being Nat st j in dom M holds
b₁ . j = M * (j,i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of D st len b₁ = len M & ( for j being Nat st j in dom M holds
b₁ . j = M * (j,i) ) & len b₂ = len M & ( for j being Nat st j in dom M holds
b₂ . j = M * (j,i) ) holds
b₁ = b₂

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 b₄ being FinSequence of D holds
( b₄ = Line (M,i) iff ( len b₄ = width M & ( for j being Nat st j in Seg (width M) holds
b₄ . 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 b₄ being FinSequence of D holds
( b₄ = Col (M,i) iff ( len b₄ = len M & ( for j being Nat st j in dom M holds
b₄ . 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 (width M) -tuples_on D;
coherence
Line (M,i) is Element of (width M) -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 * ;

cluster Values M -> finite ;

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 (Values M) <= (len M) * (width 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 (width M) 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 <*<*a*>*> & <*<*a*>*> * (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 b₁ being Matrix of D st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of D st len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) & len b₂ = len M & ( for k being Nat st k in dom M holds
b₂ . k = Del ((Line (M,k)),i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines DelCol MATRIX_0:def 13 :
for i being Nat
for D being non empty set
for M, b₄ being Matrix of D holds
( b₄ = DelCol (M,i) iff ( len b₄ = len M & ( for k being Nat st k in dom M holds
b₄ . 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 (width M) 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 (width M) 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) & 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) & 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 (width G) 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) & 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) & 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 (width G) )

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) & 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 (width G) )

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) & 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 (width G) )

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) & 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 (width G) )

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 (width G) )

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 (width G) )

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,(width G))),k) = Col (G,k) & k in Seg (width (DelCol (G,(width 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 (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) )

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 (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))

proof end;