:: MATRIX_2 semantic presentation

definition

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

end;

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

definition

let c₁ be non empty set ;
let c₂, c₃ be Nat;
let c₄ be Element of c₁;
redefine func --> as c₂,c₃ --> c₄ -> Matrix of a₂,a₃,a₁;
coherence by MATRIX_1:10;

end;

theorem Th1: :: MATRIX_2:1

for b₁, b₂, b₃, b₄ being Nat
for b₅ being non empty set
for b₆ being Element of b₅ st [b₁,b₂] in Indices (b₃,b₄ --> b₆) holds
(b₃,b₄ --> b₆) * b₁,b₂ = b₆

proof end;

theorem Th2: :: MATRIX_2:2

for b₁ being Nat
for b₂ being Field
for b₃, b₄ being Element of b₂ holds (b₁,b₁ --> b₃) + (b₁,b₁ --> b₄) = b₁,b₁ --> (b₃ + b₄)

proof end;

definition

let c₁, c₂, c₃, c₄ be set ;
func c₁,c₂ ][ c₃,c₄ -> tabular FinSequence equals :: MATRIX_2:def 2
<*<*a₁,a₂*>,<*a₃,a₄*>*>;
correctness

proof end;

end;

:: deftheorem Def2 defines ][ MATRIX_2:def 2 :

theorem Th3: :: MATRIX_2:3

for b₁, b₂, b₃, b₄ being set holds
( len (b₁,b₂ ][ b₃,b₄) = 2 & width (b₁,b₂ ][ b₃,b₄) = 2 & Indices (b₁,b₂ ][ b₃,b₄) = [:(Seg 2),(Seg 2):] )

proof end;

theorem Th4: :: MATRIX_2:4

for b₁, b₂, b₃, b₄ being set holds
( [1,1] in Indices (b₁,b₂ ][ b₃,b₄) & [1,2] in Indices (b₁,b₂ ][ b₃,b₄) & [2,1] in Indices (b₁,b₂ ][ b₃,b₄) & [2,2] in Indices (b₁,b₂ ][ b₃,b₄) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func <* as <*c₂*> -> Element of 1 -tuples_on a₁;
coherence by FINSEQ_2:118;

end;

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be Element of c₂ -tuples_on c₁;
redefine func <* as <*c₃*> -> Matrix of 1,a₂,a₁;
coherence

proof end;

end;

theorem Th5: :: MATRIX_2:5

for b₁ being non empty set
for b₂ being Element of b₁ holds
( [1,1] in Indices <*<*b₂*>*> & <*<*b₂*>*> * 1,1 = b₂ )

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃, c₄, c₅ be Element of c₁;
redefine func ][ as c₂,c₃ ][ c₄,c₅ -> Matrix of 2,a₁;
coherence by MATRIX_1:19;

end;

theorem Th6: :: MATRIX_2:6

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( (b₂,b₃ ][ b₄,b₅) * 1,1 = b₂ & (b₂,b₃ ][ b₄,b₅) * 1,2 = b₃ & (b₂,b₃ ][ b₄,b₅) * 2,1 = b₄ & (b₂,b₃ ][ b₄,b₅) * 2,2 = b₅ )

proof end;

definition

let c₁ be Nat;
let c₂ be Field;
mode Upper_Triangular_Matrix of c₁,c₂ -> Matrix of a₁,a₂ means :: MATRIX_2:def 3
for b₁, b₂ being Nat st [b₁,b₂] in Indices a₃ & b₁ > b₂ holds
a₃ * b₁,b₂ = 0. a₂;
existence

proof end;

end;

:: deftheorem Def3 defines Upper_Triangular_Matrix MATRIX_2:def 3 :

definition

let c₁ be Nat;
let c₂ be Field;
mode Lower_Triangular_Matrix of c₁,c₂ -> Matrix of a₁,a₂ means :: MATRIX_2:def 4
for b₁, b₂ being Nat st [b₁,b₂] in Indices a₃ & b₁ < b₂ holds
a₃ * b₁,b₂ = 0. a₂;
existence

proof end;

end;

:: deftheorem Def4 defines Lower_Triangular_Matrix MATRIX_2:def 4 :

theorem Th7: :: MATRIX_2:7

for b₁ being Nat
for b₂ being non empty set
for b₃ being Matrix of b₂ st len b₃ = b₁ holds
b₃ is Matrix of b₁, width b₃,b₂

proof end;

theorem Th8: :: MATRIX_2:8

canceled;

theorem Th9: :: MATRIX_2:9

canceled;

theorem Th10: :: MATRIX_2:10

for b₁, b₂ being Nat
for b₃ being Field
for b₄ being Matrix of b₁,b₂,b₃
for b₅ being Nat st b₅ in Seg b₁ holds
b₄ . b₅ = Line b₄,b₅

proof end;

definition

let c₁ be Nat;
let c₂ be Field;
let c₃ be Matrix of c₂;
canceled;
assume E5: c₁ in Seg (width c₃) ;
func DelCol c₃,c₁ -> Matrix of a₂ means :: MATRIX_2:def 6
( len a₄ = len a₃ & ( for b₁ being Nat st b₁ in dom a₃ holds
a₄ . b₁ = Del (Line a₃,b₁),a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 MATRIX_2:def 5 :

:: deftheorem Def6 defines DelCol MATRIX_2:def 6 :

theorem Th11: :: MATRIX_2:11

for b₁ being non empty set
for b₂, b₃ being Matrix of b₁ st b₂ @ = b₃ @ & len b₂ = len b₃ holds
b₂ = b₃

proof end;

theorem Th12: :: MATRIX_2:12

for b₁ being non empty set
for b₂ being Matrix of b₁ st width b₂ > 0 holds
( len (b₂ @ ) = width b₂ & width (b₂ @ ) = len b₂ )

proof end;

theorem Th13: :: MATRIX_2:13

for b₁ being non empty set
for b₂, b₃ being Matrix of b₁ st width b₂ > 0 & width b₃ > 0 & b₂ @ = b₃ @ & width (b₂ @ ) = width (b₃ @ ) holds
b₂ = b₃

proof end;

theorem Th14: :: MATRIX_2:14

for b₁ being non empty set
for b₂, b₃ being Matrix of b₁ st width b₂ > 0 & width b₃ > 0 holds
( b₂ = b₃ iff ( b₂ @ = b₃ @ & width b₂ = width b₃ ) )

proof end;

theorem Th15: :: MATRIX_2:15

for b₁ being non empty set
for b₂ being Matrix of b₁ st len b₂ > 0 & width b₂ > 0 holds
(b₂ @ ) @ = b₂

proof end;

theorem Th16: :: MATRIX_2:16

for b₁ being non empty set
for b₂ being Matrix of b₁
for b₃ being Nat st b₃ in dom b₂ holds
Line b₂,b₃ = Col (b₂ @ ),b₃

proof end;

theorem Th17: :: MATRIX_2:17

for b₁ being non empty set
for b₂ being Matrix of b₁
for b₃ being Nat st b₃ in Seg (width b₂) holds
Line (b₂ @ ),b₃ = Col b₂,b₃

proof end;

theorem Th18: :: MATRIX_2:18

for b₁ being non empty set
for b₂ being Matrix of b₁
for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ = Line b₂,b₃

proof end;

definition

let c₁ be Nat;
let c₂ be Field;
let c₃ be Matrix of c₂;
assume E12: ( c₁ in dom c₃ & width c₃ > 0 ) ;
func DelLine c₃,c₁ -> Matrix of a₂ means :: MATRIX_2:def 7
a₄ = {} if len a₃ = 1
otherwise ( width a₄ = width a₃ & ( for b₁ being Nat st b₁ in Seg (width a₃) holds
Col a₄,b₁ = Del (Col a₃,b₁),a₁ ) );
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def7 defines DelLine MATRIX_2:def 7 :

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Field;
let c₅ be Matrix of c₃,c₄;
func Deleting c₅,c₁,c₂ -> Matrix of a₄ equals :: MATRIX_2:def 8
{} if a₃ = 1
otherwise DelCol (DelLine a₅,a₁),a₂;
coherence by MATRIX_1:13;
consistency ;

end;

:: deftheorem Def8 defines Deleting MATRIX_2:def 8 :

definition

let c₁ be set ;
attr a₁ is permutational means :Def9: :: MATRIX_2:def 9
ex b₁ being Nat st
for b₂ being set st b₂ in a₁ holds
b₂ is Permutation of Seg b₁;

end;

:: deftheorem Def9 defines permutational MATRIX_2:def 9 :

registration

cluster non empty permutational set ;
existence

proof end;

end;

definition

let c₁ be non empty permutational set ;
func len c₁ -> Nat means :Def10: :: MATRIX_2:def 10
ex b₁ being FinSequence st
( b₁ in a₁ & a₂ = len b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines len MATRIX_2:def 10 :

definition

let c₁ be non empty permutational set ;
redefine mode Element as Element of c₁ -> Permutation of Seg (len a₁);
coherence

proof end;

end;

theorem Th19: :: MATRIX_2:19

for b₁ being Nat ex b₂ being non empty permutational set st len b₂ = b₁

proof end;

definition

let c₁ be Nat;
func Permutations c₁ -> set means :Def11: :: MATRIX_2:def 11
for b₁ being set holds
( b₁ in a₂ iff b₁ is Permutation of Seg a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Permutations MATRIX_2:def 11 :

registration

let c₁ be Nat;
cluster Permutations a₁ -> non empty permutational ;
coherence

proof end;

end;

theorem Th20: :: MATRIX_2:20

for b₁ being Nat holds len (Permutations b₁) = b₁

proof end;

theorem Th21: :: MATRIX_2:21

Permutations 1 = {(idseq 1)}

proof end;

definition

let c₁ be Nat;
let c₂ be Element of Permutations c₁;
func len c₂ -> Nat means :Def12: :: MATRIX_2:def 12
ex b₁ being FinSequence st
( b₁ = a₂ & a₃ = len b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def12 defines len MATRIX_2:def 12 :

theorem Th22: :: MATRIX_2:22

for b₁ being Nat
for b₂ being Element of Permutations b₁ holds len b₂ = b₁

proof end;

definition

let c₁ be Nat;
func Group_of_Perm c₁ -> strict HGrStr means :Def13: :: MATRIX_2:def 13
( the carrier of a₂ = Permutations a₁ & ( for b₁, b₂ being Element of Permutations a₁ holds the mult of a₂ . b₁,b₂ = b₂ * b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Group_of_Perm MATRIX_2:def 13 :

registration

let c₁ be Nat;
cluster Group_of_Perm a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th23: :: MATRIX_2:23

for b₁ being Nat holds idseq b₁ is Element of (Group_of_Perm b₁)

proof end;

theorem Th24: :: MATRIX_2:24

for b₁ being Nat
for b₂ being Element of Permutations b₁ holds
( b₂ * (idseq b₁) = b₂ & (idseq b₁) * b₂ = b₂ )

proof end;

theorem Th25: :: MATRIX_2:25

for b₁ being Nat
for b₂ being Element of Permutations b₁ holds
( b₂ * (b₂ " ) = idseq b₁ & (b₂ " ) * b₂ = idseq b₁ )

proof end;

theorem Th26: :: MATRIX_2:26

for b₁ being Nat
for b₂ being Element of Permutations b₁ holds b₂ " is Element of (Group_of_Perm b₁)

proof end;

definition

let c₁ be Nat;
mode permutation of a₁ is Element of Permutations a₁;

end;

registration

let c₁ be Nat;
cluster Group_of_Perm a₁ -> non empty strict Group-like associative ;
coherence

proof end;

end;

theorem Th27: :: MATRIX_2:27

canceled;

theorem Th28: :: MATRIX_2:28

for b₁ being Nat holds idseq b₁ = 1. (Group_of_Perm b₁)

proof end;

definition

let c₁ be Nat;
let c₂ be Permutation of Seg c₁;
attr a₂ is being_transposition means :: MATRIX_2:def 14
ex b₁, b₂ being Nat st
( b₁ in dom a₂ & b₂ in dom a₂ & b₁ <> b₂ & a₂ . b₁ = b₂ & a₂ . b₂ = b₁ & ( for b₃ being Nat st b₃ <> b₁ & b₃ <> b₂ & b₃ in dom a₂ holds
a₂ . b₃ = b₃ ) );

end;

:: deftheorem Def14 defines being_transposition MATRIX_2:def 14 :

notation

let c₁ be Nat;
let c₂ be Permutation of Seg c₁;
synonym c₂ is_transposition for being_transposition c₂;

end;

definition

let c₁ be Nat;
let c₂ be Permutation of Seg c₁;
attr a₂ is even means :Def15: :: MATRIX_2:def 15
ex b₁ being FinSequence of the carrier of (Group_of_Perm a₁) st
( (len b₁) mod 2 = 0 & a₂ = Product b₁ & ( for b₂ being Nat st b₂ in dom b₁ holds
ex b₃ being Element of Permutations a₁ st
( b₁ . b₂ = b₃ & b₃ is_transposition ) ) );

end;

:: deftheorem Def15 defines even MATRIX_2:def 15 :

notation

let c₁ be Nat;
let c₂ be Permutation of Seg c₁;
antonym odd c₂ for even c₂;

end;

theorem Th29: :: MATRIX_2:29

for b₁ being Nat holds id (Seg b₁) is even

proof end;

definition

let c₁ be Field;
let c₂ be Nat;
let c₃ be Element of c₁;
let c₄ be Element of Permutations c₂;
func - c₃,c₄ -> Element of a₁ equals :: MATRIX_2:def 16
a₃ if a₄ is even
otherwise - a₃;
correctness ;

end;

:: deftheorem Def16 defines - MATRIX_2:def 16 :

definition

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

end;

:: deftheorem Def17 defines FinOmega MATRIX_2:def 17 :

theorem Th30: :: MATRIX_2:30

for b₁ being Nat holds Permutations b₁ is finite

proof end;