:: by Katarzyna Jankowska

::

:: Received June 8, 1991

:: Copyright (c) 1991-2018 Association of Mizar Users

:: 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 ) );

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

ex b_{1} being FinSequence st b_{1} is tabular
end;

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

existence ex b

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

for a1, a2, b1, b2 being Element of D holds <*<*a1,a2*>,<*b1,b2*>*> is tabular

proof end;

registration

let D be set ;

ex b_{1} being FinSequence of D * st b_{1} is tabular

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

existence ex b

proof end;

registration
end;

registration

let D be non empty set ;

not for b_{1} being Matrix of D holds b_{1} is empty-yielding

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

existence not for b

proof 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 ) )

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;

end;
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 ) );

( len M = m & ( for p being FinSequence of D st p in rng M holds

len p = n ) );

:: 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 ) ) );

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;

ex b_{1} being Matrix of D st b_{1} is m,n -size

end;
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 Matrix of ;

existence ex b

proof end;

definition
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

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 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

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 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

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;

( ( len M > 0 implies ex b_{1} being Nat ex s being FinSequence st

( s in rng M & len s = b_{1} ) ) & ( not len M > 0 implies ex b_{1} being Nat st b_{1} = 0 ) )

for b_{1}, b_{2} being Nat holds

( ( len M > 0 & ex s being FinSequence st

( s in rng M & len s = b_{1} ) & ex s being FinSequence st

( s in rng M & len s = b_{2} ) implies b_{1} = b_{2} ) & ( not len M > 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Nat holds verum
;

end;
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 ex s being FinSequence st

( s in rng M & len s = it ) if len M > 0

otherwise it = 0 ;

( ( len M > 0 implies ex b

( s in rng M & len s = b

proof end;

uniqueness for b

( ( len M > 0 & ex s being FinSequence st

( s in rng M & len s = b

( s in rng M & len s = b

proof end;

consistency for b

:: deftheorem Def3 defines width MATRIX_0:def 3 :

for M being tabular FinSequence

for b_{2} being Nat holds

( ( len M > 0 implies ( b_{2} = width M iff ex s being FinSequence st

( s in rng M & len s = b_{2} ) ) ) & ( not len M > 0 implies ( b_{2} = width M iff b_{2} = 0 ) ) );

for M being tabular FinSequence

for b

( ( len M > 0 implies ( b

( s in rng M & len s = b

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 )

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;

:: deftheorem defines Indices MATRIX_0:def 4 :

for M being tabular FinSequence holds Indices M = [:(dom M),(Seg (width M)):];

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 ;

ex b_{1} being Element of D ex p being FinSequence of D st

( p = M . i & b_{1} = p . j )

for b_{1}, b_{2} being Element of D st ex p being FinSequence of D st

( p = M . i & b_{1} = p . j ) & ex p being FinSequence of D st

( p = M . i & b_{2} = p . j ) holds

b_{1} = b_{2}
;

end;
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 p being FinSequence of D st

( p = M . i & it = p . j );

ex b

( p = M . i & b

proof end;

uniqueness for b

( p = M . i & b

( p = M . i & b

b

:: 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_{5} being Element of D holds

( b_{5} = M * (i,j) iff ex p being FinSequence of D st

( p = M . i & b_{5} = p . j ) );

for D being set

for M being Matrix of D

for i, j being Nat st [i,j] in Indices M holds

for b

( b

( p = M . i & b

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

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 2

MatrixEx{ F_{1}() -> non empty set , F_{2}() -> Nat, F_{3}() -> Nat, P_{1}[ object , object , object ] } :

MatrixEx{ F

ex M being Matrix of F_{2}(),F_{3}(),F_{1}() st

for i, j being Nat st [i,j] in Indices M holds

P_{1}[i,j,M * (i,j)]

providedfor i, j being Nat st [i,j] in Indices M holds

P

A1:
for i, j being Nat st [i,j] in [:(Seg F_{2}()),(Seg F_{3}()):] holds

ex x being Element of F_{1}() st P_{1}[i,j,x]

ex x being Element of F

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 = {} )

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):] )

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):] )

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)):] )

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

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

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

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;

ex b_{1} being Matrix of D st

( len b_{1} = width M & ( for i, j being Nat holds

( [i,j] in Indices b_{1} iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds

b_{1} * (i,j) = M * (j,i) ) )

for b_{1}, b_{2} being Matrix of D st len b_{1} = width M & ( for i, j being Nat holds

( [i,j] in Indices b_{1} iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds

b_{1} * (i,j) = M * (j,i) ) & len b_{2} = width M & ( for i, j being Nat holds

( [i,j] in Indices b_{2} iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds

b_{2} * (i,j) = M * (j,i) ) holds

b_{1} = b_{2}

end;
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 ( 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) ) );

ex b

( len b

( [i,j] in Indices b

b

proof end;

uniqueness for b

( [i,j] in Indices b

b

( [i,j] in Indices b

b

b

proof end;

:: deftheorem Def6 defines @ MATRIX_0:def 6 :

for D being non empty set

for M, b_{3} being Matrix of D holds

( b_{3} = M @ iff ( len b_{3} = width M & ( for i, j being Nat holds

( [i,j] in Indices b_{3} iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds

b_{3} * (i,j) = M * (j,i) ) ) );

for D being non empty set

for M, b

( b

( [i,j] in Indices b

b

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 )

for M being Matrix of D st width M > 0 holds

( len (M @) = width M & width (M @) = len M )

proof end;

registration
end;

definition

let D be non empty set ;

let M be Matrix of D;

let i be Nat;

ex b_{1} being FinSequence of D st

( len b_{1} = width M & ( for j being Nat st j in Seg (width M) holds

b_{1} . j = M * (i,j) ) )

for b_{1}, b_{2} being FinSequence of D st len b_{1} = width M & ( for j being Nat st j in Seg (width M) holds

b_{1} . j = M * (i,j) ) & len b_{2} = width M & ( for j being Nat st j in Seg (width M) holds

b_{2} . j = M * (i,j) ) holds

b_{1} = b_{2}

ex b_{1} being FinSequence of D st

( len b_{1} = len M & ( for j being Nat st j in dom M holds

b_{1} . j = M * (j,i) ) )

for b_{1}, b_{2} being FinSequence of D st len b_{1} = len M & ( for j being Nat st j in dom M holds

b_{1} . j = M * (j,i) ) & len b_{2} = len M & ( for j being Nat st j in dom M holds

b_{2} . j = M * (j,i) ) holds

b_{1} = b_{2}

end;
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 ( len it = width M & ( for j being Nat st j in Seg (width M) holds

it . j = M * (i,j) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

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 ( len it = len M & ( for j being Nat st j in dom M holds

it . j = M * (j,i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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_{4} being FinSequence of D holds

( b_{4} = Line (M,i) iff ( len b_{4} = width M & ( for j being Nat st j in Seg (width M) holds

b_{4} . j = M * (i,j) ) ) );

for D being non empty set

for M being Matrix of D

for i being Nat

for b

( b

b

:: 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_{4} being FinSequence of D holds

( b_{4} = Col (M,i) iff ( len b_{4} = len M & ( for j being Nat st j in dom M holds

b_{4} . j = M * (j,i) ) ) );

for D being non empty set

for M being Matrix of D

for i being Nat

for b

( b

b

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

redefine func Col (M,i) -> Element of (len M) -tuples_on D;

coherence

Col (M,i) is Element of (len M) -tuples_on D

end;
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: Colredefine 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;

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

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

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 )

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 )

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.

:: deftheorem defines Values MATRIX_0:def 9 :

for F being Function-yielding Function holds Values F = Union (rngs F);

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

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 }

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
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

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

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 )

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 }

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: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

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

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;

( M is empty-yielding iff ( 0 = len M or 0 = width M ) )

end;
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 redefine attr M is empty-yielding means :: MATRIX_0:def 10

( 0 = len M or 0 = width M );

( M is empty-yielding iff ( 0 = len M or 0 = width M ) )

proof 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 ) );

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

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

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

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
end;

:: deftheorem defines --> MATRIX_0:def 11 :

for n, m being Nat

for a being object holds (n,m) --> a = n |-> (m |-> a);

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;
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;

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

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 ;

correctness

coherence

<*<*a,b*>,<*c,d*>*> is tabular FinSequence;

end;
correctness

coherence

<*<*a,b*>,<*c,d*>*> is tabular FinSequence;

proof end;

:: deftheorem defines ][ MATRIX_0:def 12 :

for a, b, c, d being object holds (a,b) ][ (c,d) = <*<*a,b*>,<*c,d*>*>;

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):] )

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

( [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;
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;

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

end;
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;

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 )

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;
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;

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 )

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

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)

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;

ex b_{1} being Matrix of D st

( len b_{1} = len M & ( for k being Nat st k in dom M holds

b_{1} . k = Del ((Line (M,k)),i) ) )

for b_{1}, b_{2} being Matrix of D st len b_{1} = len M & ( for k being Nat st k in dom M holds

b_{1} . k = Del ((Line (M,k)),i) ) & len b_{2} = len M & ( for k being Nat st k in dom M holds

b_{2} . k = Del ((Line (M,k)),i) ) holds

b_{1} = b_{2}

end;
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 ( len it = len M & ( for k being Nat st k in dom M holds

it . k = Del ((Line (M,k)),i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines DelCol MATRIX_0:def 13 :

for i being Nat

for D being non empty set

for M, b_{4} being Matrix of D holds

( b_{4} = DelCol (M,i) iff ( len b_{4} = len M & ( for k being Nat st k in dom M holds

b_{4} . k = Del ((Line (M,k)),i) ) ) );

for i being Nat

for D being non empty set

for M, b

( b

b

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

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 )

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

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 ) )

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 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)

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)

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)

for M being Matrix of D

for i being Nat st i in dom M holds

M . i = Line (M,i)

proof end;

notation
end;

registration

let D be non empty set ;

let i be Nat;

let M be Matrix of D;

coherence

DelLine (,M) is tabular

end;
let i be Nat;

let M be Matrix of D;

coherence

DelLine (,M) is tabular

proof 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;
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;

definition

let i, j, n be Nat;

let D be non empty set ;

let M be Matrix of n,D;

coherence

DelCol ((DelLine (M,i)),j) is Matrix of D ;

end;
let D be non empty set ;

let M be Matrix of n,D;

coherence

DelCol ((DelLine (M,i)),j) is Matrix of D ;

:: 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);

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

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)

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

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

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

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

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) )

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) )

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) )

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) )

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) )

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) )

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)))) )

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) )

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))

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;