:: by Karol P\c{a}k

::

:: Received August 28, 2007

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

begin

theorem Th1: :: MATRIX13:1

for D being non empty set

for n, m being Nat

for A being Matrix of n,m,D holds

( ( n = 0 implies m = 0 ) iff ( len A = n & width A = m ) )

for n, m being Nat

for A being Matrix of n,m,D holds

( ( n = 0 implies m = 0 ) iff ( len A = n & width A = m ) )

proof end;

theorem Th2: :: MATRIX13:2

for n being Nat

for K being Field

for M being Matrix of n,K holds

( M is Lower_Triangular_Matrix of n,K iff M @ is Upper_Triangular_Matrix of n,K )

for K being Field

for M being Matrix of n,K holds

( M is Lower_Triangular_Matrix of n,K iff M @ is Upper_Triangular_Matrix of n,K )

proof end;

theorem Th3: :: MATRIX13:3

for n being Nat

for K being Field

for M being Matrix of n,K holds diagonal_of_Matrix M = diagonal_of_Matrix (M @)

for K being Field

for M being Matrix of n,K holds diagonal_of_Matrix M = diagonal_of_Matrix (M @)

proof end;

theorem Th4: :: MATRIX13:4

for n being Nat

for perm being Element of Permutations n st perm <> idseq n holds

( ex i being Nat st

( i in Seg n & perm . i > i ) & ex j being Nat st

( j in Seg n & perm . j < j ) )

for perm being Element of Permutations n st perm <> idseq n holds

( ex i being Nat st

( i in Seg n & perm . i > i ) & ex j being Nat st

( j in Seg n & perm . j < j ) )

proof end;

theorem Th5: :: MATRIX13:5

for n being Nat

for K being Field

for M being Matrix of n,K

for perm being Element of Permutations n st perm <> idseq n & ( M is Lower_Triangular_Matrix of n,K or M is Upper_Triangular_Matrix of n,K ) holds

(Path_product M) . perm = 0. K

for K being Field

for M being Matrix of n,K

for perm being Element of Permutations n st perm <> idseq n & ( M is Lower_Triangular_Matrix of n,K or M is Upper_Triangular_Matrix of n,K ) holds

(Path_product M) . perm = 0. K

proof end;

theorem Th6: :: MATRIX13:6

for n being Nat

for K being Field

for M being Matrix of n,K

for I being Element of Permutations n st I = idseq n holds

diagonal_of_Matrix M = Path_matrix (I,M)

for K being Field

for M being Matrix of n,K

for I being Element of Permutations n st I = idseq n holds

diagonal_of_Matrix M = Path_matrix (I,M)

proof end;

theorem Th7: :: MATRIX13:7

for n being Nat

for K being Field

for M being Upper_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)

for K being Field

for M being Upper_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)

proof end;

theorem Th8: :: MATRIX13:8

for n being Nat

for K being Field

for M being Lower_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)

for K being Field

for M being Lower_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)

proof end;

theorem Th9: :: MATRIX13:9

for X being finite set

for n being Nat holds card { Y where Y is Subset of X : card Y = n } = (card X) choose n

for n being Nat holds card { Y where Y is Subset of X : card Y = n } = (card X) choose n

proof end;

theorem :: MATRIX13:11

for n being Nat

for R being Element of Permutations n st R = Rev (idseq n) holds

( R is even iff (n choose 2) mod 2 = 0 )

for R being Element of Permutations n st R = Rev (idseq n) holds

( R is even iff (n choose 2) mod 2 = 0 )

proof end;

theorem Th12: :: MATRIX13:12

for n being Nat

for K being Field

for M being Matrix of n,K

for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds

M * (i,j) = 0. K ) holds

M * R is Upper_Triangular_Matrix of n,K

for K being Field

for M being Matrix of n,K

for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds

M * (i,j) = 0. K ) holds

M * R is Upper_Triangular_Matrix of n,K

proof end;

theorem Th13: :: MATRIX13:13

for n being Nat

for K being Field

for M being Matrix of n,K

for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds

M * (i,j) = 0. K ) holds

M * R is Lower_Triangular_Matrix of n,K

for K being Field

for M being Matrix of n,K

for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds

M * (i,j) = 0. K ) holds

M * R is Lower_Triangular_Matrix of n,K

proof end;

theorem :: MATRIX13:14

for n being Nat

for K being Field

for M being Matrix of n,K

for R being Element of Permutations n st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds

M * (i,j) = 0. K or for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds

M * (i,j) = 0. K ) holds

Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)

for K being Field

for M being Matrix of n,K

for R being Element of Permutations n st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds

M * (i,j) = 0. K or for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds

M * (i,j) = 0. K ) holds

Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)

proof end;

theorem Th15: :: MATRIX13:15

for n being Nat

for K being Field

for M being Matrix of n,K

for M1, M2 being Upper_Triangular_Matrix of n,K st M = M1 * M2 holds

( M is Upper_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) )

for K being Field

for M being Matrix of n,K

for M1, M2 being Upper_Triangular_Matrix of n,K st M = M1 * M2 holds

( M is Upper_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) )

proof end;

theorem :: MATRIX13:16

for n being Nat

for K being Field

for M being Matrix of n,K

for M1, M2 being Lower_Triangular_Matrix of n,K st M = M1 * M2 holds

( M is Lower_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) )

for K being Field

for M being Matrix of n,K

for M1, M2 being Lower_Triangular_Matrix of n,K st M = M1 * M2 holds

( M is Lower_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) )

proof end;

begin

definition

let D be non empty set ;

let M be Matrix of D;

let n, m be Nat;

let nt be Element of n -tuples_on NAT;

let mt be Element of m -tuples_on NAT;

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

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

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

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

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

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

b_{1} = b_{2}

end;
let M be Matrix of D;

let n, m be Nat;

let nt be Element of n -tuples_on NAT;

let mt be Element of m -tuples_on NAT;

func Segm (M,nt,mt) -> Matrix of n,m,D means :Def1: :: MATRIX13:def 1

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

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

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

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

ex b

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

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines Segm MATRIX13:def 1 :

for D being non empty set

for M being Matrix of D

for n, m being Nat

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for b_{7} being Matrix of n,m,D holds

( b_{7} = Segm (M,nt,mt) iff for i, j being Nat st [i,j] in Indices b_{7} holds

b_{7} * (i,j) = M * ((nt . i),(mt . j)) );

for D being non empty set

for M being Matrix of D

for n, m being Nat

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for b

( b

b

theorem Th17: :: MATRIX13:17

for D being non empty set

for n, m, i, j being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds

( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A )

for n, m, i, j being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds

( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A )

proof end;

theorem Th18: :: MATRIX13:18

for D being non empty set

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT holds

not ( [:(rng nt),(rng mt):] c= Indices A & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & not (Segm (A,nt,mt)) @ = Segm ((A @),mt,nt) )

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT holds

not ( [:(rng nt),(rng mt):] c= Indices A & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & not (Segm (A,nt,mt)) @ = Segm ((A @),mt,nt) )

proof end;

theorem Th19: :: MATRIX13:19

for D being non empty set

for m, n being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A & ( m = 0 implies n = 0 ) holds

Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @

for m, n being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A & ( m = 0 implies n = 0 ) holds

Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @

proof end;

theorem Th21: :: MATRIX13:21

for D being non empty set

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st n = 1 & m = 1 holds

Segm (A,nt,mt) = <*<*(A * ((nt . 1),(mt . 1)))*>*>

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st n = 1 & m = 1 holds

Segm (A,nt,mt) = <*<*(A * ((nt . 1),(mt . 1)))*>*>

proof end;

theorem Th22: :: MATRIX13:22

for D being non empty set

for A being Matrix of 2,D holds A = ((A * (1,1)),(A * (1,2))) ][ ((A * (2,1)),(A * (2,2)))

for A being Matrix of 2,D holds A = ((A * (1,1)),(A * (1,2))) ][ ((A * (2,1)),(A * (2,2)))

proof end;

theorem Th23: :: MATRIX13:23

for D being non empty set

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st n = 2 & m = 2 holds

Segm (A,nt,mt) = ((A * ((nt . 1),(mt . 1))),(A * ((nt . 1),(mt . 2)))) ][ ((A * ((nt . 2),(mt . 1))),(A * ((nt . 2),(mt . 2))))

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st n = 2 & m = 2 holds

Segm (A,nt,mt) = ((A * ((nt . 1),(mt . 1))),(A * ((nt . 1),(mt . 2)))) ][ ((A * ((nt . 2),(mt . 1))),(A * ((nt . 2),(mt . 2))))

proof end;

theorem Th24: :: MATRIX13:24

for D being non empty set

for m, i, n being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st i in Seg n & rng mt c= Seg (width A) holds

Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt

for m, i, n being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st i in Seg n & rng mt c= Seg (width A) holds

Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt

proof end;

theorem Th25: :: MATRIX13:25

for D being non empty set

for m, i, n, j being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st i in Seg n & j in Seg n & nt . i = nt . j holds

Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)

for m, i, n, j being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st i in Seg n & j in Seg n & nt . i = nt . j holds

Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)

proof end;

theorem Th26: :: MATRIX13:26

for i, n, j being Nat

for K being Field

for nt, nt1 being Element of n -tuples_on NAT

for M being Matrix of K st i in Seg n & j in Seg n & nt . i = nt . j & i <> j holds

Det (Segm (M,nt,nt1)) = 0. K

for K being Field

for nt, nt1 being Element of n -tuples_on NAT

for M being Matrix of K st i in Seg n & j in Seg n & nt . i = nt . j & i <> j holds

Det (Segm (M,nt,nt1)) = 0. K

proof end;

theorem Th27: :: MATRIX13:27

for n being Nat

for K being Field

for nt, nt1 being Element of n -tuples_on NAT

for M being Matrix of K st not nt is one-to-one holds

Det (Segm (M,nt,nt1)) = 0. K

for K being Field

for nt, nt1 being Element of n -tuples_on NAT

for M being Matrix of K st not nt is one-to-one holds

Det (Segm (M,nt,nt1)) = 0. K

proof end;

theorem Th28: :: MATRIX13:28

for D being non empty set

for n, j, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st j in Seg m & rng nt c= Seg (len A) holds

Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt

for n, j, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st j in Seg m & rng nt c= Seg (len A) holds

Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt

proof end;

theorem Th29: :: MATRIX13:29

for D being non empty set

for n, i, m, j being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st i in Seg m & j in Seg m & mt . i = mt . j holds

Col ((Segm (A,nt,mt)),i) = Col ((Segm (A,nt,mt)),j)

for n, i, m, j being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st i in Seg m & j in Seg m & mt . i = mt . j holds

Col ((Segm (A,nt,mt)),i) = Col ((Segm (A,nt,mt)),j)

proof end;

theorem Th30: :: MATRIX13:30

for i, m, j being Nat

for K being Field

for mt, mt1 being Element of m -tuples_on NAT

for M being Matrix of K st i in Seg m & j in Seg m & mt . i = mt . j & i <> j holds

Det (Segm (M,mt1,mt)) = 0. K

for K being Field

for mt, mt1 being Element of m -tuples_on NAT

for M being Matrix of K st i in Seg m & j in Seg m & mt . i = mt . j & i <> j holds

Det (Segm (M,mt1,mt)) = 0. K

proof end;

theorem Th31: :: MATRIX13:31

for m being Nat

for K being Field

for mt, mt1 being Element of m -tuples_on NAT

for M being Matrix of K st not mt is one-to-one holds

Det (Segm (M,mt1,mt)) = 0. K

for K being Field

for mt, mt1 being Element of m -tuples_on NAT

for M being Matrix of K st not mt is one-to-one holds

Det (Segm (M,mt1,mt)) = 0. K

proof end;

theorem Th32: :: MATRIX13:32

for n being Nat

for nt, nt1 being Element of n -tuples_on NAT st nt is one-to-one & nt1 is one-to-one & rng nt = rng nt1 holds

ex perm being Permutation of (Seg n) st nt1 = nt * perm

for nt, nt1 being Element of n -tuples_on NAT st nt is one-to-one & nt1 is one-to-one & rng nt = rng nt1 holds

ex perm being Permutation of (Seg n) st nt1 = nt * perm

proof end;

theorem Th33: :: MATRIX13:33

for D being non empty set

for m, n being Nat

for A being Matrix of D

for nt1, nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for f being Function of (Seg n),(Seg n) st nt1 = nt * f holds

Segm (A,nt1,mt) = (Segm (A,nt,mt)) * f

for m, n being Nat

for A being Matrix of D

for nt1, nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for f being Function of (Seg n),(Seg n) st nt1 = nt * f holds

Segm (A,nt1,mt) = (Segm (A,nt,mt)) * f

proof end;

theorem Th34: :: MATRIX13:34

for D being non empty set

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt1, mt being Element of m -tuples_on NAT

for f being Function of (Seg m),(Seg m) st mt1 = mt * f holds

(Segm (A,nt,mt1)) @ = ((Segm (A,nt,mt)) @) * f

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt1, mt being Element of m -tuples_on NAT

for f being Function of (Seg m),(Seg m) st mt1 = mt * f holds

(Segm (A,nt,mt1)) @ = ((Segm (A,nt,mt)) @) * f

proof end;

theorem Th35: :: MATRIX13:35

for n being Nat

for K being Field

for nt1, nt2, nt being Element of n -tuples_on NAT

for M being Matrix of K

for perm being Element of Permutations n st nt1 = nt2 * perm holds

( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) & Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) )

for K being Field

for nt1, nt2, nt being Element of n -tuples_on NAT

for M being Matrix of K

for perm being Element of Permutations n st nt1 = nt2 * perm holds

( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) & Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) )

proof end;

Lm1: for n being Nat

for nt, nt1 being Element of n -tuples_on NAT st rng nt = rng nt1 & nt is one-to-one holds

nt1 is one-to-one

proof end;

theorem Th36: :: MATRIX13:36

for n being Nat

for K being Field

for M being Matrix of K

for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) holds

Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19)))

for K being Field

for M being Matrix of K

for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) holds

Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19)))

proof end;

theorem Th37: :: MATRIX13:37

for D being non empty set

for n9, m9, n, m being Nat

for A9 being Matrix of n9,m9,D

for F, Fmt being FinSequence of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds

for i, j being Nat st nt " {j} = {i} holds

RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)

for n9, m9, n, m being Nat

for A9 being Matrix of n9,m9,D

for F, Fmt being FinSequence of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds

for i, j being Nat st nt " {j} = {i} holds

RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)

proof end;

theorem Th38: :: MATRIX13:38

for D being non empty set

for n9, m9, m, n being Nat

for A9 being Matrix of n9,m9,D

for mt being Element of m -tuples_on NAT

for F being FinSequence of D

for i being Nat

for nt being Element of n -tuples_on NAT st not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds

Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)

for n9, m9, m, n being Nat

for A9 being Matrix of n9,m9,D

for mt being Element of m -tuples_on NAT

for F being FinSequence of D

for i being Nat

for nt being Element of n -tuples_on NAT st not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds

Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)

proof end;

theorem Th39: :: MATRIX13:39

for D being non empty set

for n9, m9, m, i, n, j being Nat

for A9 being Matrix of n9,m9,D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds

ex nt1 being Element of n -tuples_on NAT st

( rng nt1 = ((rng nt) \ {i}) \/ {j} & Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt) = Segm (A9,nt1,mt) )

for n9, m9, m, i, n, j being Nat

for A9 being Matrix of n9,m9,D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds

ex nt1 being Element of n -tuples_on NAT st

( rng nt1 = ((rng nt) \ {i}) \/ {j} & Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt) = Segm (A9,nt1,mt) )

proof end;

theorem Th40: :: MATRIX13:40

for D being non empty set

for n9, m9, i being Nat

for A9 being Matrix of n9,m9,D

for F being FinSequence of D st not i in Seg (len A9) holds

RLine (A9,i,F) = A9

for n9, m9, i being Nat

for A9 being Matrix of n9,m9,D

for F being FinSequence of D st not i in Seg (len A9) holds

RLine (A9,i,F) = A9

proof end;

definition

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let a be Element of K;

:: original: *

redefine func a * M -> Matrix of n,m,K;

coherence

a * M is Matrix of n,m,K

end;
let K be Field;

let M be Matrix of n,m,K;

let a be Element of K;

:: original: *

redefine func a * M -> Matrix of n,m,K;

coherence

a * M is Matrix of n,m,K

proof end;

theorem Th41: :: MATRIX13:41

for n, m being Nat

for K being Field

for a being Element of K

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds

a * (Segm (M,nt,mt)) = Segm ((a * M),nt,mt)

for K being Field

for a being Element of K

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds

a * (Segm (M,nt,mt)) = Segm ((a * M),nt,mt)

proof end;

theorem Th42: :: MATRIX13:42

for D being non empty set

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st nt = idseq (len A) & mt = idseq (width A) holds

Segm (A,nt,mt) = A

for n, m being Nat

for A being Matrix of D

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st nt = idseq (len A) & mt = idseq (width A) holds

Segm (A,nt,mt) = A

proof end;

registration

existence

ex b_{1} being Subset of NAT st

( b_{1} is empty & b_{1} is without_zero & b_{1} is finite )

ex b_{1} being Subset of NAT st

( not b_{1} is empty & b_{1} is without_zero & b_{1} is finite )

end;
ex b

( b

proof end;

existence ex b

( not b

proof end;

registration
end;

registration
end;

definition

let i be Nat;

:: original: {

redefine func {i} -> Subset of NAT;

coherence

{i} is Subset of NAT

:: original: {

redefine func {i,j} -> Subset of NAT;

coherence

{i,j} is Subset of NAT

end;
:: original: {

redefine func {i} -> Subset of NAT;

coherence

{i} is Subset of NAT

proof end;

let j be Nat;:: original: {

redefine func {i,j} -> Subset of NAT;

coherence

{i,j} is Subset of NAT

proof end;

definition

let N be finite without_zero Subset of NAT;

:: original: Sgm

redefine func Sgm N -> Element of (card N) -tuples_on NAT;

coherence

Sgm N is Element of (card N) -tuples_on NAT

end;
:: original: Sgm

redefine func Sgm N -> Element of (card N) -tuples_on NAT;

coherence

Sgm N is Element of (card N) -tuples_on NAT

proof end;

definition

let D be non empty set ;

let A be Matrix of D;

let P, Q be finite without_zero Subset of NAT;

coherence

Segm (A,(Sgm P),(Sgm Q)) is Matrix of card P, card Q,D ;

end;
let A be Matrix of D;

let P, Q be finite without_zero Subset of NAT;

coherence

Segm (A,(Sgm P),(Sgm Q)) is Matrix of card P, card Q,D ;

:: deftheorem defines Segm MATRIX13:def 2 :

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT holds Segm (A,P,Q) = Segm (A,(Sgm P),(Sgm Q));

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT holds Segm (A,P,Q) = Segm (A,(Sgm P),(Sgm Q));

theorem Th44: :: MATRIX13:44

for D being non empty set

for i0, j0 being non zero Nat

for A being Matrix of D holds Segm (A,{i0},{j0}) = <*<*(A * (i0,j0))*>*>

for i0, j0 being non zero Nat

for A being Matrix of D holds Segm (A,{i0},{j0}) = <*<*(A * (i0,j0))*>*>

proof end;

theorem Th45: :: MATRIX13:45

for D being non empty set

for i0, j0, n0, m0 being non zero Nat

for A being Matrix of D st i0 < j0 & n0 < m0 holds

Segm (A,{i0,j0},{n0,m0}) = ((A * (i0,n0)),(A * (i0,m0))) ][ ((A * (j0,n0)),(A * (j0,m0)))

for i0, j0, n0, m0 being non zero Nat

for A being Matrix of D st i0 < j0 & n0 < m0 holds

Segm (A,{i0,j0},{n0,m0}) = ((A * (i0,n0)),(A * (i0,m0))) ][ ((A * (j0,n0)),(A * (j0,m0)))

proof end;

theorem Th47: :: MATRIX13:47

for D being non empty set

for i being Nat

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st i in Seg (card P) & Q c= Seg (width A) holds

Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)

for i being Nat

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st i in Seg (card P) & Q c= Seg (width A) holds

Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)

proof end;

theorem Th48: :: MATRIX13:48

for D being non empty set

for i being Nat

for A being Matrix of D

for P being finite without_zero Subset of NAT st i in Seg (card P) holds

Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i))

for i being Nat

for A being Matrix of D

for P being finite without_zero Subset of NAT st i in Seg (card P) holds

Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i))

proof end;

theorem Th49: :: MATRIX13:49

for D being non empty set

for j being Nat

for A being Matrix of D

for Q, P being finite without_zero Subset of NAT st j in Seg (card Q) & P c= Seg (len A) holds

Col ((Segm (A,P,Q)),j) = (Col (A,((Sgm Q) . j))) * (Sgm P)

for j being Nat

for A being Matrix of D

for Q, P being finite without_zero Subset of NAT st j in Seg (card Q) & P c= Seg (len A) holds

Col ((Segm (A,P,Q)),j) = (Col (A,((Sgm Q) . j))) * (Sgm P)

proof end;

theorem Th50: :: MATRIX13:50

for D being non empty set

for j being Nat

for A being Matrix of D

for Q being finite without_zero Subset of NAT st j in Seg (card Q) holds

Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j))

for j being Nat

for A being Matrix of D

for Q being finite without_zero Subset of NAT st j in Seg (card Q) holds

Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j))

proof end;

theorem Th51: :: MATRIX13:51

for D being non empty set

for i being Nat

for A being Matrix of D holds Segm (A,((Seg (len A)) \ {i}),(Seg (width A))) = Del (A,i)

for i being Nat

for A being Matrix of D holds Segm (A,((Seg (len A)) \ {i}),(Seg (width A))) = Del (A,i)

proof end;

theorem Th52: :: MATRIX13:52

for i being Nat

for K being Field

for M being Matrix of K holds Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = DelCol (M,i)

for K being Field

for M being Matrix of K holds Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = DelCol (M,i)

proof end;

theorem Th53: :: MATRIX13:53

for X being set

for P being finite without_zero Subset of NAT holds (Sgm P) " X is finite without_zero Subset of NAT

for P being finite without_zero Subset of NAT holds (Sgm P) " X is finite without_zero Subset of NAT

proof end;

theorem Th54: :: MATRIX13:54

for X being set

for P being finite without_zero Subset of NAT st X c= P holds

Sgm X = (Sgm P) * (Sgm ((Sgm P) " X))

for P being finite without_zero Subset of NAT st X c= P holds

Sgm X = (Sgm P) * (Sgm ((Sgm P) " X))

proof end;

Lm2: for X being set

for P being finite without_zero Subset of NAT st X c= P holds

card X = card ((Sgm P) " X)

proof end;

theorem Th55: :: MATRIX13:55

for X, Y being set

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT holds [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm (A,P,Q))

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT holds [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm (A,P,Q))

proof end;

theorem Th56: :: MATRIX13:56

for D being non empty set

for A being Matrix of D

for P, P1, Q, Q1, P2, Q2 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 & P2 = (Sgm P1) " P & Q2 = (Sgm Q1) " Q holds

( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )

for A being Matrix of D

for P, P1, Q, Q1, P2, Q2 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 & P2 = (Sgm P1) " P & Q2 = (Sgm Q1) " Q holds

( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )

proof end;

theorem Th57: :: MATRIX13:57

for D being non empty set

for A being Matrix of D

for P, Q, P1, Q1 being finite without_zero Subset of NAT holds

not ( ( P = {} implies Q = {} ) & ( Q = {} implies P = {} ) & [:P,Q:] c= Indices (Segm (A,P1,Q1)) & ( for P2, Q2 being finite without_zero Subset of NAT holds

( not P2 c= P1 or not Q2 c= Q1 or not P2 = (Sgm P1) .: P or not Q2 = (Sgm Q1) .: Q or not card P2 = card P or not card Q2 = card Q or not Segm ((Segm (A,P1,Q1)),P,Q) = Segm (A,P2,Q2) ) ) )

for A being Matrix of D

for P, Q, P1, Q1 being finite without_zero Subset of NAT holds

not ( ( P = {} implies Q = {} ) & ( Q = {} implies P = {} ) & [:P,Q:] c= Indices (Segm (A,P1,Q1)) & ( for P2, Q2 being finite without_zero Subset of NAT holds

( not P2 c= P1 or not Q2 c= Q1 or not P2 = (Sgm P1) .: P or not Q2 = (Sgm Q1) .: Q or not card P2 = card P or not card Q2 = card Q or not Segm ((Segm (A,P1,Q1)),P,Q) = Segm (A,P2,Q2) ) ) )

proof end;

theorem Th58: :: MATRIX13:58

for n, i, j being Nat

for K being Field

for M being Matrix of n,K holds Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)

for K being Field

for M being Matrix of n,K holds Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)

proof end;

theorem Th59: :: MATRIX13:59

for D being non empty set

for n9, m9, i being Nat

for A9 being Matrix of n9,m9,D

for Q, P being finite without_zero Subset of NAT

for F, FQ being FinSequence of D st len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 holds

RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)

for n9, m9, i being Nat

for A9 being Matrix of n9,m9,D

for Q, P being finite without_zero Subset of NAT

for F, FQ being FinSequence of D st len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 holds

RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)

proof end;

theorem Th60: :: MATRIX13:60

for D being non empty set

for n9, m9 being Nat

for A9 being Matrix of n9,m9,D

for Q being finite without_zero Subset of NAT

for F being FinSequence of D

for i being Nat

for P being finite without_zero Subset of NAT st not i in P & [:P,Q:] c= Indices A9 holds

Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)

for n9, m9 being Nat

for A9 being Matrix of n9,m9,D

for Q being finite without_zero Subset of NAT

for F being FinSequence of D

for i being Nat

for P being finite without_zero Subset of NAT st not i in P & [:P,Q:] c= Indices A9 holds

Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)

proof end;

theorem :: MATRIX13:61

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT holds

not ( [:P,Q:] c= Indices A & ( card P = 0 implies card Q = 0 ) & ( card Q = 0 implies card P = 0 ) & not (Segm (A,P,Q)) @ = Segm ((A @),Q,P) )

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT holds

not ( [:P,Q:] c= Indices A & ( card P = 0 implies card Q = 0 ) & ( card Q = 0 implies card P = 0 ) & not (Segm (A,P,Q)) @ = Segm ((A @),Q,P) )

proof end;

theorem Th62: :: MATRIX13:62

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A & ( card Q = 0 implies card P = 0 ) holds

Segm (A,P,Q) = (Segm ((A @),Q,P)) @

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A & ( card Q = 0 implies card P = 0 ) holds

Segm (A,P,Q) = (Segm ((A @),Q,P)) @

proof end;

theorem Th63: :: MATRIX13:63

for K being Field

for a being Element of K

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds

a * (Segm (M,P,Q)) = Segm ((a * M),P,Q)

for a being Element of K

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds

a * (Segm (M,P,Q)) = Segm ((a * M),P,Q)

proof end;

definition

let D be non empty set ;

let A be Matrix of D;

let P, Q be finite without_zero Subset of NAT;

assume A1: card P = card Q ;

coherence

Segm (A,P,Q) is Matrix of card P,D by A1;

end;
let A be Matrix of D;

let P, Q be finite without_zero Subset of NAT;

assume A1: card P = card Q ;

coherence

Segm (A,P,Q) is Matrix of card P,D by A1;

:: deftheorem Def3 defines EqSegm MATRIX13:def 3 :

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st card P = card Q holds

EqSegm (A,P,Q) = Segm (A,P,Q);

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st card P = card Q holds

EqSegm (A,P,Q) = Segm (A,P,Q);

theorem Th64: :: MATRIX13:64

for K being Field

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT

for i, j being Nat st i in Seg (card P) & j in Seg (card P) & card P = card Q holds

( Delete ((EqSegm (M,P,Q)),i,j) = EqSegm (M,(P \ {((Sgm P) . i)}),(Q \ {((Sgm Q) . j)})) & card (P \ {((Sgm P) . i)}) = card (Q \ {((Sgm Q) . j)}) )

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT

for i, j being Nat st i in Seg (card P) & j in Seg (card P) & card P = card Q holds

( Delete ((EqSegm (M,P,Q)),i,j) = EqSegm (M,(P \ {((Sgm P) . i)}),(Q \ {((Sgm Q) . j)})) & card (P \ {((Sgm P) . i)}) = card (Q \ {((Sgm Q) . j)}) )

proof end;

Lm3: for K being Field

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT

for i being Nat st i in Seg (card P) & Det (EqSegm (M,P,Q)) <> 0. K holds

ex j being Nat st

( j in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )

proof end;

theorem Th65: :: MATRIX13:65

for K being Field

for M being Matrix of K

for P, P1, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & P c= P1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

ex Q being finite without_zero Subset of NAT st

( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )

for M being Matrix of K

for P, P1, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & P c= P1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

ex Q being finite without_zero Subset of NAT st

( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )

proof end;

Lm4: for j being Nat

for K being Field

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT

for i being Nat st j in Seg (card P) & Det (EqSegm (M,P,Q)) <> 0. K holds

ex i being Nat st

( i in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )

proof end;

theorem :: MATRIX13:66

for K being Field

for M being Matrix of K

for P1, Q, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & Q c= Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

ex P being finite without_zero Subset of NAT st

( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )

for M being Matrix of K

for P1, Q, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & Q c= Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

ex P being finite without_zero Subset of NAT st

( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )

proof end;

theorem Th67: :: MATRIX13:67

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st card P = card Q holds

( [:P,Q:] c= Indices A iff ( P c= Seg (len A) & Q c= Seg (width A) ) )

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st card P = card Q holds

( [:P,Q:] c= Indices A iff ( P c= Seg (len A) & Q c= Seg (width A) ) )

proof end;

theorem Th68: :: MATRIX13:68

for m9, n9 being Nat

for K being Field

for M9 being Matrix of n9,m9,K

for P, Q being finite without_zero Subset of NAT

for i being Nat

for j0 being non zero Nat st j0 in Seg n9 & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M9 holds

( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )

for K being Field

for M9 being Matrix of n9,m9,K

for P, Q being finite without_zero Subset of NAT

for i being Nat

for j0 being non zero Nat st j0 in Seg n9 & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M9 holds

( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )

proof end;

theorem Th69: :: MATRIX13:69

for D being non empty set

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st card P = card Q holds

( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @) )

for A being Matrix of D

for P, Q being finite without_zero Subset of NAT st card P = card Q holds

( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @) )

proof end;

theorem Th70: :: MATRIX13:70

for K being Field

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds

Det (EqSegm (M,P,Q)) = Det (EqSegm ((M @),Q,P))

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds

Det (EqSegm (M,P,Q)) = Det (EqSegm ((M @),Q,P))

proof end;

theorem Th71: :: MATRIX13:71

for n being Nat

for K being Field

for a being Element of K

for M being Matrix of n,K holds Det (a * M) = ((power K) . (a,n)) * (Det M)

for K being Field

for a being Element of K

for M being Matrix of n,K holds Det (a * M) = ((power K) . (a,n)) * (Det M)

proof end;

theorem Th72: :: MATRIX13:72

for K being Field

for a being Element of K

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds

Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q)))

for a being Element of K

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds

Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q)))

proof end;

definition

let K be Field;

let M be Matrix of K;

ex b_{1} being Element of NAT st

( ex P, Q being finite without_zero Subset of NAT st

( [:P,Q:] c= Indices M & card P = card Q & card P = b_{1} & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

card P1 <= b_{1} ) )

for b_{1}, b_{2} being Element of NAT st ex P, Q being finite without_zero Subset of NAT st

( [:P,Q:] c= Indices M & card P = card Q & card P = b_{1} & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

card P1 <= b_{1} ) & ex P, Q being finite without_zero Subset of NAT st

( [:P,Q:] c= Indices M & card P = card Q & card P = b_{2} & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

card P1 <= b_{2} ) holds

b_{1} = b_{2}

end;
let M be Matrix of K;

func the_rank_of M -> Element of NAT means :Def4: :: MATRIX13:def 4

( ex P, Q being finite without_zero Subset of NAT st

( [:P,Q:] c= Indices M & card P = card Q & card P = it & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

card P1 <= it ) );

existence ( ex P, Q being finite without_zero Subset of NAT st

( [:P,Q:] c= Indices M & card P = card Q & card P = it & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

card P1 <= it ) );

ex b

( ex P, Q being finite without_zero Subset of NAT st

( [:P,Q:] c= Indices M & card P = card Q & card P = b

card P1 <= b

proof end;

uniqueness for b

( [:P,Q:] c= Indices M & card P = card Q & card P = b

card P1 <= b

( [:P,Q:] c= Indices M & card P = card Q & card P = b

card P1 <= b

b

proof end;

:: deftheorem Def4 defines the_rank_of MATRIX13:def 4 :

for K being Field

for M being Matrix of K

for b_{3} being Element of NAT holds

( b_{3} = the_rank_of M iff ( ex P, Q being finite without_zero Subset of NAT st

( [:P,Q:] c= Indices M & card P = card Q & card P = b_{3} & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds

card P1 <= b_{3} ) ) );

for K being Field

for M being Matrix of K

for b

( b

( [:P,Q:] c= Indices M & card P = card Q & card P = b

card P1 <= b

theorem Th73: :: MATRIX13:73

for K being Field

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds

( card P <= len M & card Q <= width M )

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds

( card P <= len M & card Q <= width M )

proof end;

theorem Th74: :: MATRIX13:74

for K being Field

for M being Matrix of K holds

( the_rank_of M <= len M & the_rank_of M <= width M )

for M being Matrix of K holds

( the_rank_of M <= len M & the_rank_of M <= width M )

proof end;

Lm5: for n, m being Nat

for K being Field

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for M being Matrix of K holds

not ( [:(rng nt),(rng mt):] c= Indices M & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & ( for P1, P2 being finite without_zero Subset of NAT holds

( not P1 = rng nt or not P2 = rng mt ) ) )

proof end;

theorem Th75: :: MATRIX13:75

for n being Nat

for K being Field

for nt1, nt2 being Element of n -tuples_on NAT

for M being Matrix of K st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds

ex P1, P2 being finite without_zero Subset of NAT st

( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K )

for K being Field

for nt1, nt2 being Element of n -tuples_on NAT

for M being Matrix of K st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds

ex P1, P2 being finite without_zero Subset of NAT st

( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K )

proof end;

theorem Th76: :: MATRIX13:76

for K being Field

for M being Matrix of K

for RANK being Element of NAT holds

( the_rank_of M = RANK iff ( ex rt1, rt2 being Element of RANK -tuples_on NAT st

( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm (M,rt1,rt2)) <> 0. K ) & ( for n being Nat

for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds

n <= RANK ) ) )

for M being Matrix of K

for RANK being Element of NAT holds

( the_rank_of M = RANK iff ( ex rt1, rt2 being Element of RANK -tuples_on NAT st

( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm (M,rt1,rt2)) <> 0. K ) & ( for n being Nat

for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds

n <= RANK ) ) )

proof end;

theorem Th77: :: MATRIX13:77

for n, m being Nat

for K being Field

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for M being Matrix of K st ( n = 0 or m = 0 ) holds

the_rank_of (Segm (M,nt,mt)) = 0

for K being Field

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for M being Matrix of K st ( n = 0 or m = 0 ) holds

the_rank_of (Segm (M,nt,mt)) = 0

proof end;

theorem Th78: :: MATRIX13:78

for n, m being Nat

for K being Field

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds

the_rank_of M >= the_rank_of (Segm (M,nt,mt))

for K being Field

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds

the_rank_of M >= the_rank_of (Segm (M,nt,mt))

proof end;

theorem Th79: :: MATRIX13:79

for K being Field

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds

the_rank_of M >= the_rank_of (Segm (M,P,Q))

for M being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds

the_rank_of M >= the_rank_of (Segm (M,P,Q))

proof end;

theorem Th80: :: MATRIX13:80

for K being Field

for M being Matrix of K

for P, P1, Q, Q1 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 holds

the_rank_of (Segm (M,P,Q)) <= the_rank_of (Segm (M,P1,Q1))

for M being Matrix of K

for P, P1, Q, Q1 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 holds

the_rank_of (Segm (M,P,Q)) <= the_rank_of (Segm (M,P1,Q1))

proof end;

theorem Th81: :: MATRIX13:81

for f, g being Function st rng f c= rng g holds

ex h being Function st

( dom h = dom f & rng h c= dom g & f = g * h )

ex h being Function st

( dom h = dom f & rng h c= dom g & f = g * h )

proof end;

theorem Th82: :: MATRIX13:82

for n, m being Nat

for K being Field

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for M being Matrix of K st [:(rng nt),(rng mt):] = Indices M holds

the_rank_of M = the_rank_of (Segm (M,nt,mt))

for K being Field

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT

for M being Matrix of K st [:(rng nt),(rng mt):] = Indices M holds

the_rank_of M = the_rank_of (Segm (M,nt,mt))

proof end;

theorem Th83: :: MATRIX13:83

for n being Nat

for K being Field

for M being Matrix of n,K holds

( the_rank_of M = n iff Det M <> 0. K )

for K being Field

for M being Matrix of n,K holds

( the_rank_of M = n iff Det M <> 0. K )

proof end;

Lm6: for n being Nat

for K being Field

for a being Element of K st a <> 0. K holds

(power K) . (a,n) <> 0. K

proof end;

theorem :: MATRIX13:85

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for F being Permutation of (Seg n) holds the_rank_of M = the_rank_of (M * F)

for K being Field

for M being Matrix of n,m,K

for F being Permutation of (Seg n) holds the_rank_of M = the_rank_of (M * F)

proof end;

theorem :: MATRIX13:86

for K being Field

for a being Element of K

for M being Matrix of K st a <> 0. K holds

the_rank_of M = the_rank_of (a * M)

for a being Element of K

for M being Matrix of K st a <> 0. K holds

the_rank_of M = the_rank_of (a * M)

proof end;

theorem Th87: :: MATRIX13:87

for K being Field

for a being Element of K

for p, pf being FinSequence of K

for f being Function st pf = p * f & rng f c= dom p holds

(a * p) * f = a * pf

for a being Element of K

for p, pf being FinSequence of K

for f being Function st pf = p * f & rng f c= dom p holds

(a * p) * f = a * pf

proof end;

theorem Th88: :: MATRIX13:88

for K being Field

for p, pf, q, qf being FinSequence of K

for f being Function st pf = p * f & rng f c= dom p & qf = q * f & rng f c= dom q holds

(p + q) * f = pf + qf

for p, pf, q, qf being FinSequence of K

for f being Function st pf = p * f & rng f c= dom p & qf = q * f & rng f c= dom q holds

(p + q) * f = pf + qf

proof end;

theorem Th89: :: MATRIX13:89

for n9, m9, i being Nat

for K being Field

for a being Element of K

for M9 being Matrix of n9,m9,K st a <> 0. K holds

the_rank_of M9 = the_rank_of (RLine (M9,i,(a * (Line (M9,i)))))

for K being Field

for a being Element of K

for M9 being Matrix of n9,m9,K st a <> 0. K holds

the_rank_of M9 = the_rank_of (RLine (M9,i,(a * (Line (M9,i)))))

proof end;

theorem Th90: :: MATRIX13:90

for i being Nat

for K being Field

for M being Matrix of K st Line (M,i) = (width M) |-> (0. K) holds

the_rank_of (DelLine (M,i)) = the_rank_of M

for K being Field

for M being Matrix of K st Line (M,i) = (width M) |-> (0. K) holds

the_rank_of (DelLine (M,i)) = the_rank_of M

proof end;

theorem Th91: :: MATRIX13:91

for n9, m9, i being Nat

for K being Field

for M9 being Matrix of n9,m9,K

for p being FinSequence of K st len p = width M9 holds

the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))

for K being Field

for M9 being Matrix of n9,m9,K

for p being FinSequence of K st len p = width M9 holds

the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))

proof end;

theorem Th92: :: MATRIX13:92

for n9, m9, j, i being Nat

for K being Field

for a being Element of K

for M9 being Matrix of n9,m9,K st j in Seg (len M9) & ( i = j implies a <> - (1_ K) ) holds

the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))

for K being Field

for a being Element of K

for M9 being Matrix of n9,m9,K st j in Seg (len M9) & ( i = j implies a <> - (1_ K) ) holds

the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))

proof end;

theorem Th93: :: MATRIX13:93

for n9, m9, j, i being Nat

for K being Field

for a being Element of K

for M9 being Matrix of n9,m9,K st j in Seg (len M9) & j <> i holds

the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))

for K being Field

for a being Element of K

for M9 being Matrix of n9,m9,K st j in Seg (len M9) & j <> i holds

the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))

proof end;

theorem Th94: :: MATRIX13:94

for K being Field

for M being Matrix of K holds

( the_rank_of M > 0 iff ex i, j being Nat st

( [i,j] in Indices M & M * (i,j) <> 0. K ) )

for M being Matrix of K holds

( the_rank_of M > 0 iff ex i, j being Nat st

( [i,j] in Indices M & M * (i,j) <> 0. K ) )

proof end;

theorem :: MATRIX13:95

for K being Field

for M being Matrix of K holds

( the_rank_of M = 0 iff M = 0. (K,(len M),(width M)) )

for M being Matrix of K holds

( the_rank_of M = 0 iff M = 0. (K,(len M),(width M)) )

proof end;

theorem Th96: :: MATRIX13:96

for K being Field

for M being Matrix of K holds

( the_rank_of M = 1 iff ( ex i, j being Nat st

( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds

Det (EqSegm (M,{i0,j0},{n0,m0})) = 0. K ) ) )

for M being Matrix of K holds

( the_rank_of M = 1 iff ( ex i, j being Nat st

( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds

Det (EqSegm (M,{i0,j0},{n0,m0})) = 0. K ) ) )

proof end;

theorem Th97: :: MATRIX13:97

for K being Field

for M being Matrix of K holds

( the_rank_of M = 1 iff ( ex i, j being Nat st

( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds

(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n)) ) ) )

for M being Matrix of K holds

( the_rank_of M = 1 iff ( ex i, j being Nat st

( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds

(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n)) ) ) )

proof end;

theorem :: MATRIX13:98

for K being Field

for M being Matrix of K holds

( the_rank_of M = 1 iff ex i being Nat st

( i in Seg (len M) & ex j being Nat st

( j in Seg (width M) & M * (i,j) <> 0. K ) & ( for k being Nat st k in Seg (len M) holds

ex a being Element of K st Line (M,k) = a * (Line (M,i)) ) ) )

for M being Matrix of K holds

( the_rank_of M = 1 iff ex i being Nat st

( i in Seg (len M) & ex j being Nat st

( j in Seg (width M) & M * (i,j) <> 0. K ) & ( for k being Nat st k in Seg (len M) holds

ex a being Element of K st Line (M,k) = a * (Line (M,i)) ) ) )

proof end;

registration

let K be Field;

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

end;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular diagonal for FinSequence of the carrier of K * ;

existence ex b

proof end;

theorem Th99: :: MATRIX13:99

for K being Field

for M being diagonal Matrix of K

for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds

( P c= NonZero1 & Q c= NonZero1 )

for M being diagonal Matrix of K

for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds

( P c= NonZero1 & Q c= NonZero1 )

proof end;

theorem Th100: :: MATRIX13:100

for K being Field

for M being diagonal Matrix of K

for P being finite without_zero Subset of NAT st [:P,P:] c= Indices M holds

Segm (M,P,P) is V162(b_{1})

for M being diagonal Matrix of K

for P being finite without_zero Subset of NAT st [:P,P:] c= Indices M holds

Segm (M,P,P) is V162(b

proof end;

theorem :: MATRIX13:101

for K being Field

for M being diagonal Matrix of K

for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds

the_rank_of M = card NonZero1

for M being diagonal Matrix of K

for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds

the_rank_of M = card NonZero1

proof end;

theorem Th102: :: MATRIX13:102

for n being Nat

for K being Field

for a being Element of K

for v1, v2, v being Vector of (n -VectSp_over K)

for t1, t2, t being Element of n -tuples_on the carrier of K holds

( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )

for K being Field

for a being Element of K

for v1, v2, v being Vector of (n -VectSp_over K)

for t1, t2, t being Element of n -tuples_on the carrier of K holds

( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )

proof end;

registration

let K be Field;

let n be Nat;

coherence

( n -VectSp_over K is right_complementable & n -VectSp_over K is Abelian & n -VectSp_over K is add-associative & n -VectSp_over K is right_zeroed )

end;
let n be Nat;

coherence

( n -VectSp_over K is right_complementable & n -VectSp_over K is Abelian & n -VectSp_over K is add-associative & n -VectSp_over K is right_zeroed )

proof end;

registration

let K be Field;

let n be Nat;

correctness

coherence

for b_{1} being Vector of (n -VectSp_over K) holds

( b_{1} is Function-like & b_{1} is Relation-like );

end;
let n be Nat;

correctness

coherence

for b

( b

proof end;

Lm7: for m, n being Nat

for K being Field

for M being Matrix of m,n,K holds rng M is Subset of (n -VectSp_over K)

proof end;

notation

let K be Field;

let m, n be Nat;

let M be Matrix of m,n,K;

synonym lines M for rng K;

synonym without_repeated_line M for one-to-one ;

end;
let m, n be Nat;

let M be Matrix of m,n,K;

synonym lines M for rng K;

synonym without_repeated_line M for one-to-one ;

definition

let K be Field;

let m, n be Nat;

let M be Matrix of m,n,K;

:: original: lines

redefine func lines M -> Subset of (n -VectSp_over K);

coherence

lines is Subset of (n -VectSp_over K) by Lm7;

end;
let m, n be Nat;

let M be Matrix of m,n,K;

:: original: lines

redefine func lines M -> Subset of (n -VectSp_over K);

coherence

lines is Subset of (n -VectSp_over K) by Lm7;

theorem Th103: :: MATRIX13:103

for x being set

for n, m being Nat

for K being Field

for M being Matrix of m,n,K holds

( x in lines M iff ex i being Nat st

( i in Seg m & x = Line (M,i) ) )

for n, m being Nat

for K being Field

for M being Matrix of m,n,K holds

( x in lines M iff ex i being Nat st

( i in Seg m & x = Line (M,i) ) )

proof end;

theorem :: MATRIX13:104

for n being Nat

for K being Field

for V being finite Subset of (n -VectSp_over K) ex M being Matrix of card V,n,K st

( M is without_repeated_line & lines M = V )

for K being Field

for V being finite Subset of (n -VectSp_over K) ex M being Matrix of card V,n,K st

( M is without_repeated_line & lines M = V )

proof end;

definition

let K be Field;

let n be Nat;

let F be FinSequence of (n -VectSp_over K);

coherence

F is Matrix of len F,n,K

end;
let n be Nat;

let F be FinSequence of (n -VectSp_over K);

coherence

F is Matrix of len F,n,K

proof end;

:: deftheorem defines FinS2MX MATRIX13:def 5 :

for K being Field

for n being Nat

for F being FinSequence of (n -VectSp_over K) holds FinS2MX F = F;

for K being Field

for n being Nat

for F being FinSequence of (n -VectSp_over K) holds FinS2MX F = F;

definition

let K be Field;

let m, n be Nat;

let M be Matrix of m,n,K;

coherence

M is FinSequence of (n -VectSp_over K)

end;
let m, n be Nat;

let M be Matrix of m,n,K;

coherence

M is FinSequence of (n -VectSp_over K)

proof end;

:: deftheorem defines MX2FinS MATRIX13:def 6 :

for K being Field

for m, n being Nat

for M being Matrix of m,n,K holds MX2FinS M = M;

for K being Field

for m, n being Nat

for M being Matrix of m,n,K holds MX2FinS M = M;

theorem Th105: :: MATRIX13:105

for n, m being Nat

for K being Field

for M being Matrix of m,n,K st the_rank_of M = m holds

M is without_repeated_line

for K being Field

for M being Matrix of m,n,K st the_rank_of M = m holds

M is without_repeated_line

proof end;

theorem Th106: :: MATRIX13:106

for m, n, i being Nat

for K being Field

for a being Element of K

for L being Linear_Combination of n -VectSp_over K

for M being Matrix of m,n,K st i in Seg (len M) & a = L . (M . i) holds

Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i))

for K being Field

for a being Element of K

for L being Linear_Combination of n -VectSp_over K

for M being Matrix of m,n,K st i in Seg (len M) & a = L . (M . i) holds

Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i))

proof end;

theorem Th107: :: MATRIX13:107

for m, i, n being Nat

for K being Field

for L being Linear_Combination of n -VectSp_over K

for M being Matrix of m,n,K st M is without_repeated_line & Carrier L c= lines M & i in Seg n holds

(Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))

for K being Field

for L being Linear_Combination of n -VectSp_over K

for M being Matrix of m,n,K st M is without_repeated_line & Carrier L c= lines M & i in Seg n holds

(Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))

proof end;

theorem Th108: :: MATRIX13:108

for n, m being Nat

for K being Field

for M, M1 being Matrix of m,n,K st M is without_repeated_line & ( for i being Nat st i in Seg m holds

ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) holds

ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1

for K being Field

for M, M1 being Matrix of m,n,K st M is without_repeated_line & ( for i being Nat st i in Seg m holds

ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) holds

ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1

proof end;

theorem Th109: :: MATRIX13:109

for n, m being Nat

for K being Field

for M being Matrix of m,n,K st M is without_repeated_line holds

( ( ( for i being Nat st i in Seg m holds

Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds

ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds

Sum (Col (M1,j)) = 0. K ) holds

M1 = 0. (K,m,n) ) ) iff lines M is linearly-independent )

for K being Field

for M being Matrix of m,n,K st M is without_repeated_line holds

( ( ( for i being Nat st i in Seg m holds

Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds

ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds

Sum (Col (M1,j)) = 0. K ) holds

M1 = 0. (K,m,n) ) ) iff lines M is linearly-independent )

proof end;

theorem Th110: :: MATRIX13:110

for n, m being Nat

for K being Field

for M being Matrix of m,n,K st the_rank_of M = m holds

lines M is linearly-independent

for K being Field

for M being Matrix of m,n,K st the_rank_of M = m holds

lines M is linearly-independent

proof end;

theorem Th111: :: MATRIX13:111

for n being Nat

for K being Field

for M being Diagonal of n,K st the_rank_of M = n holds

lines M is Basis of n -VectSp_over K

for K being Field

for M being Diagonal of n,K st the_rank_of M = n holds

lines M is Basis of n -VectSp_over K

proof end;

Lm8: for n being Nat

for K being Field holds

( lines (1. (K,n)) is Basis of n -VectSp_over K & the_rank_of (1. (K,n)) = n )

proof end;

registration
end;

theorem Th113: :: MATRIX13:113

for n, m being Nat

for K being Field

for M being Matrix of m,n,K

for i being Nat

for a being Element of K st ( for j being Nat st j in Seg m holds

M * (j,i) = a ) holds

( M is without_repeated_line iff Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) is without_repeated_line )

for K being Field

for M being Matrix of m,n,K

for i being Nat

for a being Element of K st ( for j being Nat st j in Seg m holds

M * (j,i) = a ) holds

( M is without_repeated_line iff Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) is without_repeated_line )

proof end;

theorem Th114: :: MATRIX13:114

for n, m being Nat

for K being Field

for M being Matrix of m,n,K

for i being Nat st M is without_repeated_line & lines M is linearly-independent & ( for j being Nat st j in Seg m holds

M * (j,i) = 0. K ) holds

lines (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) is linearly-independent

for K being Field

for M being Matrix of m,n,K

for i being Nat st M is without_repeated_line & lines M is linearly-independent & ( for j being Nat st j in Seg m holds

M * (j,i) = 0. K ) holds

lines (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) is linearly-independent

proof end;

theorem Th115: :: MATRIX13:115

for K being Field

for a being Element of K

for V being VectSp of K

for U being finite Subset of V st U is linearly-independent holds

for u, v being Vector of V st u in U & v in U & u <> v holds

(U \ {u}) \/ {(u + (a * v))} is linearly-independent

for a being Element of K

for V being VectSp of K

for U being finite Subset of V st U is linearly-independent holds

for u, v being Vector of V st u in U & v in U & u <> v holds

(U \ {u}) \/ {(u + (a * v))} is linearly-independent

proof end;

theorem Th116: :: MATRIX13:116

for x being set

for K being Field

for V being VectSp of K

for u, v being Vector of V holds

( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )

for K being Field

for V being VectSp of K

for u, v being Vector of V holds

( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )

proof end;

theorem Th117: :: MATRIX13:117

for n, m being Nat

for K being Field

for a being Element of K

for M being Matrix of m,n,K st lines M is linearly-independent & M is without_repeated_line holds

for i, j being Nat st j in Seg (len M) & i <> j holds

( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )

for K being Field

for a being Element of K

for M being Matrix of m,n,K st lines M is linearly-independent & M is without_repeated_line holds

for i, j being Nat st j in Seg (len M) & i <> j holds

( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )

proof end;

theorem Th118: :: MATRIX13:118

for m, n being Nat

for K being Field

for P being finite without_zero Subset of NAT

for M being Matrix of m,n,K st P c= Seg m holds

lines (Segm (M,P,(Seg n))) c= lines M

for K being Field

for P being finite without_zero Subset of NAT

for M being Matrix of m,n,K st P c= Seg m holds

lines (Segm (M,P,(Seg n))) c= lines M

proof end;

theorem Th119: :: MATRIX13:119

for m, n being Nat

for K being Field

for P being finite without_zero Subset of NAT

for M being Matrix of m,n,K st P c= Seg m & lines M is linearly-independent holds

lines (Segm (M,P,(Seg n))) is linearly-independent

for K being Field

for P being finite without_zero Subset of NAT

for M being Matrix of m,n,K st P c= Seg m & lines M is linearly-independent holds

lines (Segm (M,P,(Seg n))) is linearly-independent

proof end;

theorem Th120: :: MATRIX13:120

for m, n being Nat

for K being Field

for P being finite without_zero Subset of NAT

for M being Matrix of m,n,K st P c= Seg m & M is without_repeated_line holds

Segm (M,P,(Seg n)) is without_repeated_line

for K being Field

for P being finite without_zero Subset of NAT

for M being Matrix of m,n,K st P c= Seg m & M is without_repeated_line holds

Segm (M,P,(Seg n)) is without_repeated_line

proof end;

theorem Th121: :: MATRIX13:121

for m, n being Nat

for K being Field

for M being Matrix of m,n,K holds

( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )

for K being Field

for M being Matrix of m,n,K holds

( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )

proof end;

theorem Th122: :: MATRIX13:122

for n, m being Nat

for K being Field

for M being Matrix of m,n,K

for U being Subset of (n -VectSp_over K) st U c= lines M holds

ex P being finite without_zero Subset of NAT st

( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )

for K being Field

for M being Matrix of m,n,K

for U being Subset of (n -VectSp_over K) st U c= lines M holds

ex P being finite without_zero Subset of NAT st

( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )

proof end;

theorem :: MATRIX13:123

for m, n being Nat

for K being Field

for M being Matrix of m,n,K

for RANK being Element of NAT holds

( the_rank_of M = RANK iff ( ex U being finite Subset of (n -VectSp_over K) st

( U is linearly-independent & U c= lines M & card U = RANK ) & ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds

card W <= RANK ) ) )

for K being Field

for M being Matrix of m,n,K

for RANK being Element of NAT holds

( the_rank_of M = RANK iff ( ex U being finite Subset of (n -VectSp_over K) st

( U is linearly-independent & U c= lines M & card U = RANK ) & ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds

card W <= RANK ) ) )

proof end;