:: by Katarzyna Jankowska

::

:: Received May 20, 1992

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

begin

definition
end;

:: deftheorem defines --> MATRIX_2:def 1 :

for n, m being Nat

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

for n, m being Nat

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

definition

let D be non empty set ;

let n, m be Nat;

let d be Element of D;

:: original: -->

redefine func (n,m) --> d -> Matrix of n,m,D;

coherence

(n,m) --> d is Matrix of n,m,D by MATRIX_1:10;

end;
let n, m be Nat;

let d be Element of D;

:: original: -->

redefine func (n,m) --> d -> Matrix of n,m,D;

coherence

(n,m) --> d is Matrix of n,m,D by MATRIX_1:10;

theorem Th1: :: MATRIX_2:1

for i, j, n, m being Nat

for D being non empty set

for a being Element of D st [i,j] in Indices ((n,m) --> a) holds

((n,m) --> a) * (i,j) = a

for D being non empty set

for a being Element of D st [i,j] in Indices ((n,m) --> a) holds

((n,m) --> a) * (i,j) = a

proof end;

theorem :: MATRIX_2:2

for n being Nat

for K being Field

for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)

for K being Field

for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)

proof end;

definition

let a, b, c, d be set ;

correctness

coherence

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

end;
correctness

coherence

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

proof end;

:: deftheorem defines ][ MATRIX_2:def 2 :

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

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

theorem Th3: :: MATRIX_2:3

for x1, x2, y1, y2 being set holds

( len ((x1,x2) ][ (y1,y2)) = 2 & width ((x1,x2) ][ (y1,y2)) = 2 & Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] )

( len ((x1,x2) ][ (y1,y2)) = 2 & width ((x1,x2) ][ (y1,y2)) = 2 & Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] )

proof end;

theorem Th4: :: MATRIX_2:4

for x1, x2, y1, y2 being set holds

( [1,1] in Indices ((x1,x2) ][ (y1,y2)) & [1,2] in Indices ((x1,x2) ][ (y1,y2)) & [2,1] in Indices ((x1,x2) ][ (y1,y2)) & [2,2] in Indices ((x1,x2) ][ (y1,y2)) )

( [1,1] in Indices ((x1,x2) ][ (y1,y2)) & [1,2] in Indices ((x1,x2) ][ (y1,y2)) & [2,1] in Indices ((x1,x2) ][ (y1,y2)) & [2,2] in Indices ((x1,x2) ][ (y1,y2)) )

proof end;

definition

let D be non empty set ;

let a be Element of D;

:: original: <*

redefine func <*a*> -> Element of 1 -tuples_on D;

coherence

<*a*> is Element of 1 -tuples_on D by FINSEQ_2:98;

end;
let a be Element of D;

:: original: <*

redefine func <*a*> -> Element of 1 -tuples_on D;

coherence

<*a*> is Element of 1 -tuples_on D by FINSEQ_2:98;

definition

let D be non empty set ;

let n be Nat;

let p be Element of n -tuples_on D;

:: original: <*

redefine func <*p*> -> Matrix of 1,n,D;

coherence

<*p*> is Matrix of 1,n,D

end;
let n be Nat;

let p be Element of n -tuples_on D;

:: original: <*

redefine func <*p*> -> Matrix of 1,n,D;

coherence

<*p*> is Matrix of 1,n,D

proof end;

theorem :: MATRIX_2:5

for D being non empty set

for a being Element of D holds

( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * (1,1) = a )

for a being Element of D holds

( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * (1,1) = a )

proof end;

definition

let D be non empty set ;

let a, b, c, d be Element of D;

:: original: ][

redefine func (a,b) ][ (c,d) -> Matrix of 2,D;

coherence

(a,b) ][ (c,d) is Matrix of 2,D by MATRIX_1:19;

end;
let a, b, c, d be Element of D;

:: original: ][

redefine func (a,b) ][ (c,d) -> Matrix of 2,D;

coherence

(a,b) ][ (c,d) is Matrix of 2,D by MATRIX_1:19;

theorem :: MATRIX_2:6

for D being non empty set

for a, b, c, d being Element of D holds

( ((a,b) ][ (c,d)) * (1,1) = a & ((a,b) ][ (c,d)) * (1,2) = b & ((a,b) ][ (c,d)) * (2,1) = c & ((a,b) ][ (c,d)) * (2,2) = d )

for a, b, c, d being Element of D holds

( ((a,b) ][ (c,d)) * (1,1) = a & ((a,b) ][ (c,d)) * (1,2) = b & ((a,b) ][ (c,d)) * (2,1) = c & ((a,b) ][ (c,d)) * (2,2) = d )

proof end;

definition

let n be Nat;

let K be Field;

let M be Matrix of n,K;

end;
let K be Field;

let M be Matrix of n,K;

attr M is upper_triangular means :Def3: :: MATRIX_2:def 3

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

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

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

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

:: deftheorem Def3 defines upper_triangular MATRIX_2:def 3 :

for n being Nat

for K being Field

for M being Matrix of n,K holds

( M is upper_triangular iff for i, j being Nat st [i,j] in Indices M & i > j holds

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

for n being Nat

for K being Field

for M being Matrix of n,K holds

( M is upper_triangular iff for i, j being Nat st [i,j] in Indices M & i > j holds

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

:: deftheorem defines lower_triangular MATRIX_2:def 4 :

for n being Nat

for K being Field

for M being Matrix of n,K holds

( M is lower_triangular iff for i, j being Nat st [i,j] in Indices M & i < j holds

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

for n being Nat

for K being Field

for M being Matrix of n,K holds

( M is lower_triangular iff for i, j being Nat st [i,j] in Indices M & i < j holds

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

registration

let n be Nat;

let K be Field;

coherence

for b_{1} being Diagonal of n,K holds

( b_{1} is upper_triangular & b_{1} is lower_triangular )

end;
let K be Field;

coherence

for b

( b

proof end;

registration

let n be Nat;

let K be Field;

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

( b_{1} is lower_triangular & b_{1} is upper_triangular )

end;
let K be Field;

cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular upper_triangular lower_triangular for Matrix of n,n, the carrier of K;

existence ex b

( b

proof end;

definition

let n be Nat;

let K be Field;

mode Upper_Triangular_Matrix of n,K is upper_triangular Matrix of n,K;

mode Lower_Triangular_Matrix of n,K is lower_triangular Matrix of n,K;

end;
let K be Field;

mode Upper_Triangular_Matrix of n,K is upper_triangular Matrix of n,K;

mode Lower_Triangular_Matrix of n,K is lower_triangular Matrix of n,K;

theorem :: MATRIX_2:7

for n being Nat

for D being non empty set

for M being Matrix of D st len M = n holds

M is Matrix of n, width M,D

for D being non empty set

for M being Matrix of D st len M = n holds

M is Matrix of n, width M,D

proof end;

begin

theorem Th8: :: MATRIX_2:8

for n, m being Nat

for D being non empty set

for M being Matrix of n,m,D

for k being Nat st k in Seg n holds

M . k = Line (M,k)

for D being non empty set

for M being Matrix of n,m,D

for k being Nat st k in Seg n holds

M . k = Line (M,k)

proof end;

Lm1: for K being Field

for M being Matrix of K

for k being Nat st k in dom M holds

M . k = Line (M,k)

proof end;

definition

let i be Nat;

let K be Field;

let M be Matrix of K;

ex b_{1} being Matrix of K st

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

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

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

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

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

b_{1} = b_{2}

end;
let K be Field;

let M be Matrix of K;

func DelCol (M,i) -> Matrix of K means :: MATRIX_2:def 5

( len it = len M & ( for k being Nat st k in dom M holds

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

existence ( len it = len M & ( for k being Nat st k in dom M holds

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

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines DelCol MATRIX_2:def 5 :

for i being Nat

for K being Field

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

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

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

for i being Nat

for K being Field

for M, b

( b

b

theorem Th9: :: MATRIX_2:9

for D being non empty set

for M1, M2 being Matrix of D st M1 @ = M2 @ & len M1 = len M2 holds

M1 = M2

for M1, M2 being Matrix of D st M1 @ = M2 @ & len M1 = len M2 holds

M1 = M2

proof end;

theorem Th10: :: MATRIX_2:10

for D being non empty set

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

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

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

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

proof end;

theorem :: MATRIX_2:11

for D being non empty set

for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 & M1 @ = M2 @ holds

M1 = M2

for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 & M1 @ = M2 @ holds

M1 = M2

proof end;

theorem :: MATRIX_2:12

for D being non empty set

for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 holds

( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) )

for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 holds

( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) )

proof end;

theorem Th14: :: MATRIX_2:14

for D being non empty set

for M being Matrix of D

for i being Nat st i in dom M holds

Line (M,i) = Col ((M @),i)

for M being Matrix of D

for i being Nat st i in dom M holds

Line (M,i) = Col ((M @),i)

proof end;

theorem :: MATRIX_2:15

for D being non empty set

for M being Matrix of D

for j being Nat st j in Seg (width M) holds

Line ((M @),j) = Col (M,j)

for M being Matrix of D

for j being Nat st j in Seg (width M) holds

Line ((M @),j) = Col (M,j)

proof end;

theorem :: MATRIX_2:16

for D being non empty set

for M being Matrix of D

for i being Nat st i in dom M holds

M . i = Line (M,i)

for M being Matrix of D

for i being Nat st i in dom M holds

M . i = Line (M,i)

proof end;

registration
end;

definition

let K be Field;

let i be Nat;

let M be Matrix of K;

:: original: DelLine

redefine func DelLine (M,i) -> Matrix of K;

coherence

DelLine (,M) is Matrix of K by FINSEQ_3:105;

end;
let i be Nat;

let M be Matrix of K;

:: original: DelLine

redefine func DelLine (M,i) -> Matrix of K;

coherence

DelLine (,M) is Matrix of K by FINSEQ_3:105;

definition

let i, j, n be Nat;

let K be Field;

let M be Matrix of n,K;

coherence

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

end;
let K be Field;

let M be Matrix of n,K;

coherence

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

:: deftheorem defines Deleting MATRIX_2:def 6 :

for i, j, n being Nat

for K being Field

for M being Matrix of n,K holds Deleting (M,i,j) = DelCol ((DelLine (M,i)),j);

for i, j, n being Nat

for K being Field

for M being Matrix of n,K holds Deleting (M,i,j) = DelCol ((DelLine (M,i)),j);

begin

definition

let IT be set ;

end;
attr IT is permutational means :Def7: :: MATRIX_2:def 7

ex n being Nat st

for x being set st x in IT holds

x is Permutation of (Seg n);

ex n being Nat st

for x being set st x in IT holds

x is Permutation of (Seg n);

:: deftheorem Def7 defines permutational MATRIX_2:def 7 :

for IT being set holds

( IT is permutational iff ex n being Nat st

for x being set st x in IT holds

x is Permutation of (Seg n) );

for IT being set holds

( IT is permutational iff ex n being Nat st

for x being set st x in IT holds

x is Permutation of (Seg n) );

registration
end;

definition

let P be non empty permutational set ;

existence

ex b_{1} being Nat ex s being FinSequence st

( s in P & b_{1} = len s )

for b_{1}, b_{2} being Nat st ex s being FinSequence st

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

( s in P & b_{2} = len s ) holds

b_{1} = b_{2}

end;
existence

ex b

( s in P & b

proof end;

uniqueness for b

( s in P & b

( s in P & b

b

proof end;

:: deftheorem Def8 defines len MATRIX_2:def 8 :

for P being non empty permutational set

for b_{2} being Nat holds

( b_{2} = len P iff ex s being FinSequence st

( s in P & b_{2} = len s ) );

for P being non empty permutational set

for b

( b

( s in P & b

definition

let P be non empty permutational set ;

:: original: len

redefine func len P -> Element of NAT ;

coherence

len P is Element of NAT by ORDINAL1:def 12;

end;
:: original: len

redefine func len P -> Element of NAT ;

coherence

len P is Element of NAT by ORDINAL1:def 12;

definition

let P be non empty permutational set ;

:: original: Element

redefine mode Element of P -> Permutation of (Seg (len P));

coherence

for b_{1} being Element of P holds b_{1} is Permutation of (Seg (len P))

end;
:: original: Element

redefine mode Element of P -> Permutation of (Seg (len P));

coherence

for b

proof end;

definition

let n be Nat;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is Permutation of (Seg n) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is Permutation of (Seg n) ) ) & ( for x being set holds

( x in b_{2} iff x is Permutation of (Seg n) ) ) holds

b_{1} = b_{2}

end;
func Permutations n -> set means :Def9: :: MATRIX_2:def 9

for x being set holds

( x in it iff x is Permutation of (Seg n) );

existence for x being set holds

( x in it iff x is Permutation of (Seg n) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def9 defines Permutations MATRIX_2:def 9 :

for n being Nat

for b_{2} being set holds

( b_{2} = Permutations n iff for x being set holds

( x in b_{2} iff x is Permutation of (Seg n) ) );

for n being Nat

for b

( b

( x in b

registration

let n be Nat;

coherence

( Permutations n is permutational & not Permutations n is empty )

end;
coherence

( Permutations n is permutational & not Permutations n is empty )

proof end;

begin

definition

let n be Nat;

ex b_{1} being strict multMagma st

( the carrier of b_{1} = Permutations n & ( for q, p being Element of Permutations n holds the multF of b_{1} . (q,p) = p * q ) )

for b_{1}, b_{2} being strict multMagma st the carrier of b_{1} = Permutations n & ( for q, p being Element of Permutations n holds the multF of b_{1} . (q,p) = p * q ) & the carrier of b_{2} = Permutations n & ( for q, p being Element of Permutations n holds the multF of b_{2} . (q,p) = p * q ) holds

b_{1} = b_{2}

end;
func Group_of_Perm n -> strict multMagma means :Def10: :: MATRIX_2:def 10

( the carrier of it = Permutations n & ( for q, p being Element of Permutations n holds the multF of it . (q,p) = p * q ) );

existence ( the carrier of it = Permutations n & ( for q, p being Element of Permutations n holds the multF of it . (q,p) = p * q ) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines Group_of_Perm MATRIX_2:def 10 :

for n being Nat

for b_{2} being strict multMagma holds

( b_{2} = Group_of_Perm n iff ( the carrier of b_{2} = Permutations n & ( for q, p being Element of Permutations n holds the multF of b_{2} . (q,p) = p * q ) ) );

for n being Nat

for b

( b

theorem Th21: :: MATRIX_2:21

for n being Nat

for p being Element of Permutations n holds

( p * (idseq n) = p & (idseq n) * p = p )

for p being Element of Permutations n holds

( p * (idseq n) = p & (idseq n) * p = p )

proof end;

theorem Th22: :: MATRIX_2:22

for n being Nat

for p being Element of Permutations n holds

( p * (p ") = idseq n & (p ") * p = idseq n )

for p being Element of Permutations n holds

( p * (p ") = idseq n & (p ") * p = idseq n )

proof end;

registration

let n be Nat;

coherence

( Group_of_Perm n is associative & Group_of_Perm n is Group-like )

end;
coherence

( Group_of_Perm n is associative & Group_of_Perm n is Group-like )

proof end;

:: deftheorem defines being_transposition MATRIX_2:def 11 :

for n being Nat

for p being Permutation of (Seg n) holds

( p is being_transposition iff ex i, j being Nat st

( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds

p . k = k ) ) );

for n being Nat

for p being Permutation of (Seg n) holds

( p is being_transposition iff ex i, j being Nat st

( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds

p . k = k ) ) );

definition

let n be Nat;

let IT be Permutation of (Seg n);

end;
let IT be Permutation of (Seg n);

attr IT is even means :Def12: :: MATRIX_2:def 12

ex l being FinSequence of (Group_of_Perm n) st

( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations n st

( l . i = q & q is being_transposition ) ) );

ex l being FinSequence of (Group_of_Perm n) st

( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations n st

( l . i = q & q is being_transposition ) ) );

:: deftheorem Def12 defines even MATRIX_2:def 12 :

for n being Nat

for IT being Permutation of (Seg n) holds

( IT is even iff ex l being FinSequence of (Group_of_Perm n) st

( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations n st

( l . i = q & q is being_transposition ) ) ) );

for n being Nat

for IT being Permutation of (Seg n) holds

( IT is even iff ex l being FinSequence of (Group_of_Perm n) st

( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations n st

( l . i = q & q is being_transposition ) ) ) );

definition

let K be Field;

let n be Nat;

let x be Element of K;

let p be Element of Permutations n;

correctness

coherence

( ( p is even implies x is Element of K ) & ( not p is even implies - x is Element of K ) );

consistency

for b_{1} being Element of K holds verum;

;

end;
let n be Nat;

let x be Element of K;

let p be Element of Permutations n;

correctness

coherence

( ( p is even implies x is Element of K ) & ( not p is even implies - x is Element of K ) );

consistency

for b

;

:: deftheorem defines - MATRIX_2:def 13 :

for K being Field

for n being Nat

for x being Element of K

for p being Element of Permutations n holds

( ( p is even implies - (x,p) = x ) & ( not p is even implies - (x,p) = - x ) );

for K being Field

for n being Nat

for x being Element of K

for p being Element of Permutations n holds

( ( p is even implies - (x,p) = x ) & ( not p is even implies - (x,p) = - x ) );

definition
end;

:: deftheorem defines FinOmega MATRIX_2:def 14 :

for X being set st X is finite holds

FinOmega X = X;

for X being set st X is finite holds

FinOmega X = X;