:: MATRIX_2 semantic presentation

definition

let n, m be Nat;
let a be set ;
func n,m --> a -> tabular FinSequence equals :: MATRIX_2:def 1
n |-> (m |-> a);
coherence by MATRIX_1:2;

end;

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

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 by MATRIX_1:10;

end;

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

proof end;

theorem :: MATRIX_2:2

for n being Nat
for K being Field
for a', b' being Element of K holds (n,n --> a') + (n,n --> b') = n,n --> (a' + b')

proof end;

definition

let a, b, c, d be set ;
func a,b ][ c,d -> tabular FinSequence equals :: MATRIX_2:def 2
<*<*a,b*>,<*c,d*>*>;
correctness

proof end;

end;

:: deftheorem defines ][ MATRIX_2:def 2 :

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

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

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 by FINSEQ_2:118;

end;

definition

let D be non empty set ;
let n be Nat;
let p be Element of n -tuples_on D;
:: original: <*
redefine func <*p*> -> Matrix of 1,n,D;
coherence

proof end;

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 )

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 by MATRIX_1:19;

end;

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 )

proof end;

definition

let n be Nat;
let K be Field;
mode Upper_Triangular_Matrix of n,K -> Matrix of n,K means :: MATRIX_2:def 3
for i, j being Nat st [i,j] in Indices it & i > j holds
it * i,j = 0. K;
existence

proof end;

end;

:: deftheorem defines Upper_Triangular_Matrix MATRIX_2:def 3 :

definition

let n be Nat;
let K be Field;
mode Lower_Triangular_Matrix of n,K -> Matrix of n,K means :: MATRIX_2:def 4
for i, j being Nat st [i,j] in Indices it & i < j holds
it * i,j = 0. K;
existence

proof end;

end;

:: deftheorem defines Lower_Triangular_Matrix MATRIX_2:def 4 :

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

proof end;

theorem :: MATRIX_2:8

canceled;

theorem :: MATRIX_2:9

canceled;

theorem Th10: :: MATRIX_2:10

for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for k being Nat st k in Seg n holds
M . k = Line M,k

proof end;

definition

let i be Nat;
let K be Field;
let M be Matrix of K;
canceled;
assume A1: i in Seg (width M) ;
func DelCol M,i -> Matrix of K means :: MATRIX_2:def 6
( len it = len M & ( for k being Nat st k in dom M holds
it . k = Del (Line M,k),i ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem MATRIX_2:def 5 :

:: deftheorem defines DelCol MATRIX_2:def 6 :

theorem Th11: :: MATRIX_2:11

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

proof end;

theorem Th12: :: MATRIX_2:12

for D being non empty set
for M being Matrix of D st width M > 0 holds
( len (M @ ) = width M & width (M @ ) = len M )

proof end;

theorem :: MATRIX_2:13

for D being non empty set
for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 & M1 @ = M2 @ & width (M1 @ ) = width (M2 @ ) holds
M1 = M2

proof end;

theorem Th14: :: MATRIX_2:14

for D being non empty set
for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 holds
( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) )

proof end;

theorem Th15: :: MATRIX_2:15

for D being non empty set
for M being Matrix of D st len M > 0 & width M > 0 holds
(M @ ) @ = M

proof end;

theorem Th16: :: 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
Line M,i = Col (M @ ),i

proof end;

theorem Th17: :: MATRIX_2:17

for D being non empty set
for M being Matrix of D
for j being Nat st j in Seg (width M) holds
Line (M @ ),j = Col M,j

proof end;

theorem Th18: :: MATRIX_2:18

for D being non empty set
for M being Matrix of D
for i being Nat st i in dom M holds
M . i = Line M,i

proof end;

definition

let i be Nat;
let K be Field;
let M be Matrix of K;
assume A1: ( i in dom M & width M > 0 ) ;
func DelLine M,i -> Matrix of K means :: MATRIX_2:def 7
it = {} if len M = 1
otherwise ( width it = width M & ( for k being Nat st k in Seg (width M) holds
Col it,k = Del (Col M,k),i ) );
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem defines DelLine MATRIX_2:def 7 :

definition

let i, j, n be Nat;
let K be Field;
let M be Matrix of n,K;
func Deleting M,i,j -> Matrix of K equals :: MATRIX_2:def 8
{} if n = 1
otherwise DelCol (DelLine M,i),j;
coherence by MATRIX_1:13;
consistency ;

end;

:: deftheorem defines Deleting MATRIX_2:def 8 :

definition

let IT be set ;
attr IT is permutational means :Def9: :: MATRIX_2:def 9
ex n being Nat st
for x being set st x in IT holds
x is Permutation of Seg n;

end;

:: deftheorem Def9 defines permutational MATRIX_2:def 9 :

registration

cluster non empty permutational set ;
existence

proof end;

end;

definition

let P be non empty permutational set ;
func len P -> Nat means :Def10: :: MATRIX_2:def 10
ex s being FinSequence st
( s in P & it = len s );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines len MATRIX_2:def 10 :

definition

let P be non empty permutational set ;
:: original: Element
redefine mode Element of P -> Permutation of Seg (len P);
coherence

proof end;

end;

theorem :: MATRIX_2:19

for n being Nat ex P being non empty permutational set st len P = n

proof end;

definition

let n be Nat;
func Permutations n -> set means :Def11: :: MATRIX_2:def 11
for x being set holds
( x in it iff x is Permutation of Seg n );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Permutations MATRIX_2:def 11 :

registration

let n be Nat;
cluster Permutations n -> non empty permutational ;
coherence

proof end;

end;

theorem :: MATRIX_2:20

for n being Nat holds len (Permutations n) = n

proof end;

theorem :: MATRIX_2:21

Permutations 1 = {(idseq 1)}

proof end;

definition

let n be Nat;
let p be Element of Permutations n;
func len p -> Nat means :Def12: :: MATRIX_2:def 12
ex s being FinSequence st
( s = p & it = len s );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def12 defines len MATRIX_2:def 12 :

theorem :: MATRIX_2:22

for n being Nat
for p being Element of Permutations n holds len p = n

proof end;

definition

let n be Nat;
func Group_of_Perm n -> strict HGrStr means :Def13: :: MATRIX_2:def 13
( the carrier of it = Permutations n & ( for q, p being Element of Permutations n holds the mult of it . q,p = p * q ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Group_of_Perm MATRIX_2:def 13 :

registration

let n be Nat;
cluster Group_of_Perm n -> non empty strict ;
coherence

proof end;

end;

theorem Th23: :: MATRIX_2:23

for n being Nat holds idseq n is Element of (Group_of_Perm n)

proof end;

theorem Th24: :: MATRIX_2:24

for n being Nat
for p being Element of Permutations n holds
( p * (idseq n) = p & (idseq n) * p = p )

proof end;

theorem Th25: :: MATRIX_2:25

for n being Nat
for p being Element of Permutations n holds
( p * (p " ) = idseq n & (p " ) * p = idseq n )

proof end;

theorem Th26: :: MATRIX_2:26

for n being Nat
for p being Element of Permutations n holds p " is Element of (Group_of_Perm n)

proof end;

definition

let n be Nat;
mode permutation of n is Element of Permutations n;

end;

registration

let n be Nat;
cluster Group_of_Perm n -> non empty strict Group-like associative ;
coherence

proof end;

end;

theorem :: MATRIX_2:27

canceled;

theorem Th28: :: MATRIX_2:28

for n being Nat holds idseq n = 1. (Group_of_Perm n)

proof end;

definition

let n be Nat;
let p be Permutation of Seg n;
attr p is being_transposition means :: MATRIX_2:def 14
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 ) );

end;

:: deftheorem defines being_transposition MATRIX_2:def 14 :

notation

let n be Nat;
let p be Permutation of Seg n;
synonym p is_transposition for being_transposition p;

end;

definition

let n be Nat;
let IT be Permutation of Seg n;
attr IT is even means :Def15: :: MATRIX_2:def 15
ex l being FinSequence of the carrier 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_transposition ) ) );

end;

:: deftheorem Def15 defines even MATRIX_2:def 15 :

notation

let n be Nat;
let IT be Permutation of Seg n;
antonym odd IT for even IT;

end;

theorem :: MATRIX_2:29

for n being Nat holds id (Seg n) is even

proof end;

definition

let K be Field;
let n be Nat;
let x be Element of K;
let p be Element of Permutations n;
func - x,p -> Element of K equals :: MATRIX_2:def 16
x if p is even
otherwise - x;
correctness ;

end;

:: deftheorem defines - MATRIX_2:def 16 :

definition

let X be set ;
assume A1: X is finite ;
func FinOmega X -> Element of Fin X equals :: MATRIX_2:def 17
X;
coherence by A1, FINSUB_1:def 5;

end;

:: deftheorem defines FinOmega MATRIX_2:def 17 :

theorem :: MATRIX_2:30

for n being Nat holds Permutations n is finite

proof end;