:: by Katarzyna Jankowska

::

:: Received June 8, 1991

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

definition

let K be non empty 1-sorted ;

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

let n be Nat;

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

let m be Nat;

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

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

let n be Nat;

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

let m be Nat;

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

definition

let K be non empty doubleLoopStr ;

let n be Nat;

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

coherence

n |-> (n |-> (0. K)) is Matrix of n,K by MATRIX_0:10;

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

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

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

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

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

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

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

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

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

b_{1} = b_{2}

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

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

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

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

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

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

b_{1} = b_{2}

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

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

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

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

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

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

b_{1} = b_{2}

end;
let n be Nat;

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

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

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

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

coherence

n |-> (n |-> (0. K)) is Matrix of n,K by MATRIX_0:10;

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

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

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

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

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

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

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

ex b

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

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

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

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

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

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

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

ex b

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

b

proof end;

uniqueness for b

b

b

b

proof end;

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

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

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

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

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

ex b

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

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines -Matrices_over MATRIX_1:def 1 :

for K being non empty doubleLoopStr

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

for K being non empty doubleLoopStr

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

:: deftheorem defines 0. MATRIX_1:def 2 :

for K being non empty doubleLoopStr

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

for K being non empty doubleLoopStr

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

:: deftheorem Def3 defines 1. MATRIX_1:def 3 :

for K being non empty doubleLoopStr

for n being Nat

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

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

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

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

for K being non empty doubleLoopStr

for n being Nat

for b

( b

b

b

:: deftheorem Def4 defines - MATRIX_1:def 4 :

for K being non empty doubleLoopStr

for n being Nat

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

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

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

for K being non empty doubleLoopStr

for n being Nat

for A, b

( b

b

:: deftheorem Def5 defines + MATRIX_1:def 5 :

for K being non empty doubleLoopStr

for n being Nat

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

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

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

for K being non empty doubleLoopStr

for n being Nat

for A, B, b

( b

b

registration
end;

theorem Th1: :: MATRIX_1:1

for i, j, n being Nat

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

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

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

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

proof end;

theorem Th2: :: MATRIX_1:2

for x being object

for n being Nat

for K being non empty doubleLoopStr holds

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

for n being Nat

for K being non empty doubleLoopStr holds

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

proof end;

:: deftheorem def6 defines diagonal MATRIX_1:def 6 :

for K being non empty ZeroStr

for M being Matrix of K holds

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

i = j );

for K being non empty ZeroStr

for M being Matrix of K holds

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

i = j );

registration

let n be Nat;

let K be non empty doubleLoopStr ;

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

end;
let K be non empty doubleLoopStr ;

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

existence ex b

proof end;

theorem Th3: :: MATRIX_1:3

for n being Nat

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

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

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

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

proof end;

theorem Th4: :: MATRIX_1:4

for n being Nat

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

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

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

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

proof end;

theorem Th5: :: MATRIX_1:5

for n being Nat

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

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

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

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

proof end;

theorem Th6: :: MATRIX_1:6

for n being Nat

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

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

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

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

proof end;

definition

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

let n be Nat;

ex b_{1} being strict AbGroup st

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

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

b_{1} = b_{2}

end;
let n be Nat;

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

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

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

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines -G_Matrix_over MATRIX_1:def 7 :

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

for n being Nat

for b_{3} being strict AbGroup holds

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

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

for n being Nat

for b

( b

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;

:: deftheorem defines upper_triangular MATRIX_1:def 8 :

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_1:def 9 :

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;

for b_{1} being diagonal Matrix of n,K holds

( b_{1} is upper_triangular & b_{1} is lower_triangular )
by def6;

end;
let K be Field;

cluster tabular V144( the carrier of K,n,n) diagonal -> diagonal upper_triangular lower_triangular for FinSequence of the carrier of K * ;

coherence for b

( b

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 V144( the carrier of K,n,n) upper_triangular lower_triangular for FinSequence of the carrier of K * ;

existence ex b

( b

proof end;

theorem :: MATRIX_1:7

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)

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 IT be set ;

end;
attr IT is permutational means :Def3: :: MATRIX_1:def 10

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 Def3 defines permutational MATRIX_1:def 10 :

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 ;

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;
func len P -> Nat means :Def4: :: MATRIX_1:def 11

ex s being FinSequence st

( s in P & it = len s );

existence ex s being FinSequence st

( s in P & it = len s );

ex b

( s in P & b

proof end;

uniqueness for b

( s in P & b

( s in P & b

b

proof end;

:: deftheorem Def4 defines len MATRIX_1:def 11 :

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 :Def5: :: MATRIX_1:def 12

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 Def5 defines Permutations MATRIX_1:def 12 :

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;

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 :Def6: :: MATRIX_1:def 13

( 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 Def6 defines Group_of_Perm MATRIX_1:def 13 :

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 Th6: :: MATRIX_1:12

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 Th7: :: MATRIX_1:13

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_1:def 14 :

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 :: MATRIX_1:def 15

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 defines even MATRIX_1:def 15 :

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 Ring;

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_1:def 16 :

for K being Ring

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 Ring

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

registration
end;