:: by Katarzyna Jankowska

::

:: Received June 8, 1991

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

begin

:: deftheorem Def1 defines tabular MATRIX_1:def 1 :

for f being FinSequence holds

( f is tabular iff ex n being Nat st

for x being set 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 set 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 countable V172() tabular for set ;

existence ex b

proof end;

theorem :: MATRIX_1: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 V27() finite FinSequence-like FinSubsequence-like countable V171() V172() tabular for FinSequence of D * ;

existence ex b

proof 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 V27() finite FinSequence-like FinSubsequence-like countable V171() V172() tabular for FinSequence of D * ;

existence not for b

proof end;

theorem Th9: :: MATRIX_1: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 set 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 set 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;

ex b_{1} being Matrix of D st

( len b_{1} = m & ( for p being FinSequence of D st p in rng b_{1} holds

len p = n ) )

end;
let m, n be Nat;

mode Matrix of m,n,D -> Matrix of D means :Def2: :: MATRIX_1:def 2

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

len p = n ) );

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

len p = n ) );

ex b

( len b

len p = n ) )

proof end;

:: deftheorem Def2 defines Matrix MATRIX_1:def 2 :

for D being non empty set

for m, n being Nat

for b_{4} being Matrix of D holds

( b_{4} is Matrix of m,n,D iff ( len b_{4} = m & ( for p being FinSequence of D st p in rng b_{4} holds

len p = n ) ) );

for D being non empty set

for m, n being Nat

for b

( b

len p = n ) ) );

definition

let K be non empty 1-sorted ;

mode Matrix of K is Matrix of the carrier of K;

let n be Nat;

mode Matrix of n,K is Matrix of n,n, the carrier of K;

let m be Nat;

mode Matrix of n,m,K is Matrix of n,m, the carrier of K;

end;
mode Matrix of K is Matrix of the carrier of K;

let n be Nat;

mode Matrix of n,K is Matrix of n,n, the carrier of K;

let m be Nat;

mode Matrix of n,m,K is Matrix of n,m, the carrier of K;

theorem Th10: :: MATRIX_1:10

for m, n 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_1: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 :: MATRIX_1: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 Element of NAT ex s being FinSequence st

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

for b_{1}, b_{2} being Element of 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 Element of NAT holds verum
;

end;
func width M -> Element of NAT means :Def3: :: MATRIX_1: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_1:def 3 :

for M being tabular FinSequence

for b_{2} being Element of 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_1: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_1: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_1: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_1: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_1: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_1:sch 2

MatrixEx{ F_{1}() -> non empty set , F_{2}() -> Element of NAT , F_{3}() -> Element of NAT , P_{1}[ set , set , set ] } :

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_1: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_1: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_1: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_1: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 Th26: :: MATRIX_1: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 Th27: :: MATRIX_1: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_1: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_1: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_1: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

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

Lm2: for n being Element of NAT

for K being non empty set

for A being Matrix of n,K holds A @ is Matrix of n,K

proof end;

definition

let n be Nat;

let D be non empty set ;

let M be Matrix of n,D;

:: original: @

redefine func M @ -> Matrix of n,D;

coherence

M @ is Matrix of n,D

end;
let D be non empty set ;

let M be Matrix of n,D;

:: original: @

redefine func M @ -> Matrix of n,D;

coherence

M @ is Matrix of n,D

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

definition

let K be non empty doubleLoopStr ;

let n be Nat;

n -tuples_on (n -tuples_on the carrier of K) is set ;

coherence

n |-> (n |-> (0. K)) is Matrix of n,K by Th10;

ex b_{1} being Matrix of n,K st

( ( for i being Nat st [i,i] in Indices b_{1} holds

b_{1} * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b_{1} & i <> j holds

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

for b_{1}, b_{2} being Matrix of n,K st ( for i being Nat st [i,i] in Indices b_{1} holds

b_{1} * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b_{1} & i <> j holds

b_{1} * (i,j) = 0. K ) & ( for i being Nat st [i,i] in Indices b_{2} holds

b_{2} * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b_{2} & i <> j holds

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

b_{1} = b_{2}

ex b_{1} being Matrix of n,K st

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

b_{1} * (i,j) = - (A * (i,j))

for b_{1}, b_{2} being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds

b_{1} * (i,j) = - (A * (i,j)) ) & ( for i, j being Nat st [i,j] in Indices A holds

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

b_{1} = b_{2}

ex b_{1} being Matrix of n,K st

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

b_{1} * (i,j) = (A * (i,j)) + (B * (i,j))

for b_{1}, b_{2} being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds

b_{1} * (i,j) = (A * (i,j)) + (B * (i,j)) ) & ( for i, j being Nat st [i,j] in Indices A holds

b_{2} * (i,j) = (A * (i,j)) + (B * (i,j)) ) holds

b_{1} = b_{2}

end;
let n be Nat;

func n -Matrices_over K -> set equals :: MATRIX_1:def 9

n -tuples_on (n -tuples_on the carrier of K);

coherence n -tuples_on (n -tuples_on the carrier of K);

n -tuples_on (n -tuples_on the carrier of K) is set ;

coherence

n |-> (n |-> (0. K)) is Matrix of n,K by Th10;

func 1. (K,n) -> Matrix of n,K means :Def11: :: MATRIX_1:def 11

( ( for i being Nat st [i,i] in Indices it holds

it * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices it & i <> j holds

it * (i,j) = 0. K ) );

existence ( ( for i being Nat st [i,i] in Indices it holds

it * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices it & i <> j holds

it * (i,j) = 0. K ) );

ex b

( ( for i being Nat st [i,i] in Indices b

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

let A be Matrix of n,K;
func - A -> Matrix of n,K means :Def12: :: MATRIX_1:def 12

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

it * (i,j) = - (A * (i,j));

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

it * (i,j) = - (A * (i,j));

ex b

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

b

proof end;

uniqueness for b

b

b

b

proof end;

let B be Matrix of n,K;
func A + B -> Matrix of n,K means :Def13: :: MATRIX_1:def 13

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

it * (i,j) = (A * (i,j)) + (B * (i,j));

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

it * (i,j) = (A * (i,j)) + (B * (i,j));

ex b

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

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines -Matrices_over MATRIX_1:def 9 :

for K being non empty doubleLoopStr

for n being Nat holds n -Matrices_over K = n -tuples_on (n -tuples_on the carrier of K);

for K being non empty doubleLoopStr

for n being Nat holds n -Matrices_over K = n -tuples_on (n -tuples_on the carrier of K);

:: deftheorem defines 0. MATRIX_1:def 10 :

for K being non empty doubleLoopStr

for n being Nat holds 0. (K,n) = n |-> (n |-> (0. K));

for K being non empty doubleLoopStr

for n being Nat holds 0. (K,n) = n |-> (n |-> (0. K));

:: deftheorem Def11 defines 1. MATRIX_1:def 11 :

for K being non empty doubleLoopStr

for n being Nat

for b_{3} being Matrix of n,K holds

( b_{3} = 1. (K,n) iff ( ( for i being Nat st [i,i] in Indices b_{3} holds

b_{3} * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b_{3} & i <> j holds

b_{3} * (i,j) = 0. K ) ) );

for K being non empty doubleLoopStr

for n being Nat

for b

( b

b

b

:: deftheorem Def12 defines - MATRIX_1:def 12 :

for K being non empty doubleLoopStr

for n being Nat

for A, b_{4} being Matrix of n,K holds

( b_{4} = - A iff for i, j being Nat st [i,j] in Indices A holds

b_{4} * (i,j) = - (A * (i,j)) );

for K being non empty doubleLoopStr

for n being Nat

for A, b

( b

b

:: deftheorem Def13 defines + MATRIX_1:def 13 :

for K being non empty doubleLoopStr

for n being Nat

for A, B, b_{5} being Matrix of n,K holds

( b_{5} = A + B iff for i, j being Nat st [i,j] in Indices A holds

b_{5} * (i,j) = (A * (i,j)) + (B * (i,j)) );

for K being non empty doubleLoopStr

for n being Nat

for A, B, b

( b

b

registration
end;

theorem Th29: :: MATRIX_1:29

for i, j, n being Nat

for K being non empty doubleLoopStr st [i,j] in Indices (0. (K,n)) holds

(0. (K,n)) * (i,j) = 0. K

for K being non empty doubleLoopStr st [i,j] in Indices (0. (K,n)) holds

(0. (K,n)) * (i,j) = 0. K

proof end;

theorem Th30: :: MATRIX_1:30

for x being set

for n being Nat

for K being non empty doubleLoopStr holds

( x is Element of n -Matrices_over K iff x is Matrix of n,K )

for n being Nat

for K being non empty doubleLoopStr holds

( x is Element of n -Matrices_over K iff x is Matrix of n,K )

proof end;

:: deftheorem defines diagonal MATRIX_1:def 14 :

for K being non empty ZeroStr

for M being Matrix of K holds

( M is diagonal iff for i, j being Nat st [i,j] in Indices M & M * (i,j) <> 0. K holds

i = j );

for K being non empty ZeroStr

for M being Matrix of K holds

( M is diagonal iff for i, j being Nat st [i,j] in Indices M & M * (i,j) <> 0. K holds

i = j );

registration

let n be Nat;

let K be non empty doubleLoopStr ;

ex b_{1} being Matrix of n,K st b_{1} is diagonal

end;
let K be non empty doubleLoopStr ;

cluster Relation-like NAT -defined the carrier of K * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() tabular diagonal for Matrix of n,n, the carrier of K;

existence ex b

proof end;

definition
end;

theorem Th31: :: MATRIX_1:31

for n being Nat

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for A, B being Matrix of n,F holds A + B = B + A

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for A, B being Matrix of n,F holds A + B = B + A

proof end;

theorem Th32: :: MATRIX_1:32

for n being Nat

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for A, B, C being Matrix of n,F holds (A + B) + C = A + (B + C)

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for A, B, C being Matrix of n,F holds (A + B) + C = A + (B + C)

proof end;

theorem Th33: :: MATRIX_1:33

for n being Nat

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for A being Matrix of n,F holds A + (0. (F,n)) = A

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for A being Matrix of n,F holds A + (0. (F,n)) = A

proof end;

theorem Th34: :: MATRIX_1:34

for n being Nat

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for A being Matrix of n,F holds A + (- A) = 0. (F,n)

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for A being Matrix of n,F holds A + (- A) = 0. (F,n)

proof end;

definition

let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ;

let n be Nat;

ex b_{1} being strict AbGroup st

( the carrier of b_{1} = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b_{1} . (A,B) = A + B ) & 0. b_{1} = 0. (F,n) )

for b_{1}, b_{2} being strict AbGroup st the carrier of b_{1} = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b_{1} . (A,B) = A + B ) & 0. b_{1} = 0. (F,n) & the carrier of b_{2} = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b_{2} . (A,B) = A + B ) & 0. b_{2} = 0. (F,n) holds

b_{1} = b_{2}

end;
let n be Nat;

func n -G_Matrix_over F -> strict AbGroup means :: MATRIX_1:def 15

( the carrier of it = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of it . (A,B) = A + B ) & 0. it = 0. (F,n) );

existence ( the carrier of it = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of it . (A,B) = A + B ) & 0. it = 0. (F,n) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines -G_Matrix_over MATRIX_1:def 15 :

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for n being Nat

for b_{3} being strict AbGroup holds

( b_{3} = n -G_Matrix_over F iff ( the carrier of b_{3} = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b_{3} . (A,B) = A + B ) & 0. b_{3} = 0. (F,n) ) );

for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for n being Nat

for b

( b

theorem :: MATRIX_1:35

for n, m being Nat

for K being non empty doubleLoopStr

for M1 being Matrix of 0 ,n,K

for M2 being Matrix of 0 ,m,K holds M1 = M2

for K being non empty doubleLoopStr

for M1 being Matrix of 0 ,n,K

for M2 being Matrix of 0 ,m,K holds M1 = M2

proof end;

begin

:: from GOBOARD7, 2008.02.21, A.T.

theorem Th36: :: MATRIX_1:36

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

for n, m, i, j 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 Th38: :: MATRIX_1:38

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

for n, m, i, j 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_1:def 16 :

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

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

theorem Th40: :: MATRIX_1:40

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 Th41: :: MATRIX_1:41

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 Th42: :: MATRIX_1:42

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 Th43: :: MATRIX_1:43

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 Th44: :: MATRIX_1:44

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 Th45: :: MATRIX_1:45

for D being non empty set

for M being Matrix of D holds Values M = { (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M }

for M being Matrix of D holds Values M = { (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M }

proof end;

theorem :: MATRIX_1:47

for D being non empty set

for i, j being Element of 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 Element of 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;