:: by Karol P\c{a}k

::

:: Received March 21, 2007

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

begin

theorem Th1: :: MATRIX11:1

for X being set

for n being Nat holds

( X in 2Set (Seg n) iff ex i, j being Nat st

( i in Seg n & j in Seg n & i < j & X = {i,j} ) )

for n being Nat holds

( X in 2Set (Seg n) iff ex i, j being Nat st

( i in Seg n & j in Seg n & i < j & X = {i,j} ) )

proof end;

registration

let n be Nat;

coherence

( not 2Set (Seg (n + 2)) is empty & 2Set (Seg (n + 2)) is finite )

end;
coherence

( not 2Set (Seg (n + 2)) is empty & 2Set (Seg (n + 2)) is finite )

proof end;

registration

let n be Nat;

let x be set ;

let perm be Element of Permutations n;

coherence

perm . x is natural

end;
let x be set ;

let perm be Element of Permutations n;

coherence

perm . x is natural

proof end;

registration

let K be Field;

coherence

the multF of K is having_a_unity ;

coherence

the multF of K is associative ;

end;
coherence

the multF of K is having_a_unity ;

coherence

the multF of K is associative ;

definition

let n be Nat;

let K be Field;

let perm2 be Element of Permutations (n + 2);

ex b_{1} being Function of (2Set (Seg (n + 2))), the carrier of K st

for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds

( ( perm2 . i < perm2 . j implies b_{1} . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b_{1} . {i,j} = - (1_ K) ) )

for b_{1}, b_{2} being Function of (2Set (Seg (n + 2))), the carrier of K st ( for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds

( ( perm2 . i < perm2 . j implies b_{1} . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b_{1} . {i,j} = - (1_ K) ) ) ) & ( for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds

( ( perm2 . i < perm2 . j implies b_{2} . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b_{2} . {i,j} = - (1_ K) ) ) ) holds

b_{1} = b_{2}

end;
let K be Field;

let perm2 be Element of Permutations (n + 2);

func Part_sgn (perm2,K) -> Function of (2Set (Seg (n + 2))), the carrier of K means :Def1: :: MATRIX11:def 1

for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds

( ( perm2 . i < perm2 . j implies it . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies it . {i,j} = - (1_ K) ) );

existence for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds

( ( perm2 . i < perm2 . j implies it . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies it . {i,j} = - (1_ K) ) );

ex b

for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds

( ( perm2 . i < perm2 . j implies b

proof end;

uniqueness for b

( ( perm2 . i < perm2 . j implies b

( ( perm2 . i < perm2 . j implies b

b

proof end;

:: deftheorem Def1 defines Part_sgn MATRIX11:def 1 :

for n being Nat

for K being Field

for perm2 being Element of Permutations (n + 2)

for b_{4} being Function of (2Set (Seg (n + 2))), the carrier of K holds

( b_{4} = Part_sgn (perm2,K) iff for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds

( ( perm2 . i < perm2 . j implies b_{4} . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b_{4} . {i,j} = - (1_ K) ) ) );

for n being Nat

for K being Field

for perm2 being Element of Permutations (n + 2)

for b

( b

( ( perm2 . i < perm2 . j implies b

theorem Th4: :: MATRIX11:4

for n being Nat

for K being Field

for p2 being Element of Permutations (n + 2)

for X being Element of Fin (2Set (Seg (n + 2))) st ( for x being set st x in X holds

(Part_sgn (p2,K)) . x = 1_ K ) holds

the multF of K $$ (X,(Part_sgn (p2,K))) = 1_ K

for K being Field

for p2 being Element of Permutations (n + 2)

for X being Element of Fin (2Set (Seg (n + 2))) st ( for x being set st x in X holds

(Part_sgn (p2,K)) . x = 1_ K ) holds

the multF of K $$ (X,(Part_sgn (p2,K))) = 1_ K

proof end;

theorem Th5: :: MATRIX11:5

for n being Nat

for K being Field

for p2 being Element of Permutations (n + 2)

for s being Element of 2Set (Seg (n + 2)) holds

( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) )

for K being Field

for p2 being Element of Permutations (n + 2)

for s being Element of 2Set (Seg (n + 2)) holds

( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) )

proof end;

theorem Th6: :: MATRIX11:6

for n being Nat

for K being Field

for p2, q2 being Element of Permutations (n + 2)

for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j holds

(Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}

for K being Field

for p2, q2 being Element of Permutations (n + 2)

for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j holds

(Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}

proof end;

theorem Th7: :: MATRIX11:7

for n being Nat

for K being Field

for X being Element of Fin (2Set (Seg (n + 2)))

for p2, q2 being Element of Permutations (n + 2)

for F being finite set st F = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (q2,K)) . s ) } holds

( ( (card F) mod 2 = 0 implies the multF of K $$ (X,(Part_sgn (p2,K))) = the multF of K $$ (X,(Part_sgn (q2,K))) ) & ( (card F) mod 2 = 1 implies the multF of K $$ (X,(Part_sgn (p2,K))) = - ( the multF of K $$ (X,(Part_sgn (q2,K)))) ) )

for K being Field

for X being Element of Fin (2Set (Seg (n + 2)))

for p2, q2 being Element of Permutations (n + 2)

for F being finite set st F = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (q2,K)) . s ) } holds

( ( (card F) mod 2 = 0 implies the multF of K $$ (X,(Part_sgn (p2,K))) = the multF of K $$ (X,(Part_sgn (q2,K))) ) & ( (card F) mod 2 = 1 implies the multF of K $$ (X,(Part_sgn (p2,K))) = - ( the multF of K $$ (X,(Part_sgn (q2,K)))) ) )

proof end;

theorem Th8: :: MATRIX11:8

for n being Nat

for P being Permutation of (Seg n) st P is being_transposition holds

for i, j being Nat st i < j holds

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

P . k = k ) ) )

for P being Permutation of (Seg n) st P is being_transposition holds

for i, j being Nat st i < j holds

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

P . k = k ) ) )

proof end;

theorem Th9: :: MATRIX11:9

for n being Nat

for K being Field

for p2, q2, pq2 being Element of Permutations (n + 2)

for i, j being Nat st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j holds

for s being Element of 2Set (Seg (n + 2)) holds

( not (Part_sgn (p2,K)) . s <> (Part_sgn (pq2,K)) . s or i in s or j in s )

for K being Field

for p2, q2, pq2 being Element of Permutations (n + 2)

for i, j being Nat st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j holds

for s being Element of 2Set (Seg (n + 2)) holds

( not (Part_sgn (p2,K)) . s <> (Part_sgn (pq2,K)) . s or i in s or j in s )

proof end;

Lm1: for n being Nat

for K being Field

for p2 being Element of Permutations (n + 2)

for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & 1_ K <> - (1_ K) holds

( ( (Part_sgn (p2,K)) . {i,j} = 1_ K implies p2 . i < p2 . j ) & ( (Part_sgn (p2,K)) . {i,j} = - (1_ K) implies p2 . i > p2 . j ) )

proof end;

theorem Th10: :: MATRIX11:10

for n being Nat

for p2, q2, pq2 being Element of Permutations (n + 2)

for i, j being Nat

for K being Field st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j & 1_ K <> - (1_ K) holds

( (Part_sgn (p2,K)) . {i,j} <> (Part_sgn (pq2,K)) . {i,j} & ( for k being Nat st k in Seg (n + 2) & i <> k & j <> k holds

( (Part_sgn (p2,K)) . {i,k} <> (Part_sgn (pq2,K)) . {i,k} iff (Part_sgn (p2,K)) . {j,k} <> (Part_sgn (pq2,K)) . {j,k} ) ) )

for p2, q2, pq2 being Element of Permutations (n + 2)

for i, j being Nat

for K being Field st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j & 1_ K <> - (1_ K) holds

( (Part_sgn (p2,K)) . {i,j} <> (Part_sgn (pq2,K)) . {i,j} & ( for k being Nat st k in Seg (n + 2) & i <> k & j <> k holds

( (Part_sgn (p2,K)) . {i,k} <> (Part_sgn (pq2,K)) . {i,k} iff (Part_sgn (p2,K)) . {j,k} <> (Part_sgn (pq2,K)) . {j,k} ) ) )

proof end;

::------------------------------------------::

:: The sign of a permutation ::

::------------------------------------------::

:: The sign of a permutation ::

::------------------------------------------::

definition

let n be Nat;

let K be Field;

let perm2 be Element of Permutations (n + 2);

the multF of K $$ ((FinOmega (2Set (Seg (n + 2)))),(Part_sgn (perm2,K))) is Element of K ;

end;
let K be Field;

let perm2 be Element of Permutations (n + 2);

func sgn (perm2,K) -> Element of K equals :: MATRIX11:def 2

the multF of K $$ ((FinOmega (2Set (Seg (n + 2)))),(Part_sgn (perm2,K)));

coherence the multF of K $$ ((FinOmega (2Set (Seg (n + 2)))),(Part_sgn (perm2,K)));

the multF of K $$ ((FinOmega (2Set (Seg (n + 2)))),(Part_sgn (perm2,K))) is Element of K ;

:: deftheorem defines sgn MATRIX11:def 2 :

for n being Nat

for K being Field

for perm2 being Element of Permutations (n + 2) holds sgn (perm2,K) = the multF of K $$ ((FinOmega (2Set (Seg (n + 2)))),(Part_sgn (perm2,K)));

for n being Nat

for K being Field

for perm2 being Element of Permutations (n + 2) holds sgn (perm2,K) = the multF of K $$ ((FinOmega (2Set (Seg (n + 2)))),(Part_sgn (perm2,K)));

theorem Th11: :: MATRIX11:11

for n being Nat

for K being Field

for p2 being Element of Permutations (n + 2) holds

( sgn (p2,K) = 1_ K or sgn (p2,K) = - (1_ K) )

for K being Field

for p2 being Element of Permutations (n + 2) holds

( sgn (p2,K) = 1_ K or sgn (p2,K) = - (1_ K) )

proof end;

theorem Th12: :: MATRIX11:12

for n being Nat

for K being Field

for Id being Element of Permutations (n + 2) st Id = idseq (n + 2) holds

sgn (Id,K) = 1_ K

for K being Field

for Id being Element of Permutations (n + 2) st Id = idseq (n + 2) holds

sgn (Id,K) = 1_ K

proof end;

Lm2: for X being set

for n, i being Nat st X in 2Set (Seg n) & i in X holds

( i in Seg n & ex j being Nat st

( j in Seg n & i <> j & X = {i,j} ) )

proof end;

theorem Th13: :: MATRIX11:13

for n being Nat

for K being Field

for p2, q2, pq2 being Element of Permutations (n + 2) st pq2 = p2 * q2 & q2 is being_transposition holds

sgn (pq2,K) = - (sgn (p2,K))

for K being Field

for p2, q2, pq2 being Element of Permutations (n + 2) st pq2 = p2 * q2 & q2 is being_transposition holds

sgn (pq2,K) = - (sgn (p2,K))

proof end;

::------------------------------------------::

:: The sign of a transposition ::

::------------------------------------------::

:: The sign of a transposition ::

::------------------------------------------::

theorem Th14: :: MATRIX11:14

for n being Nat

for K being Field

for tr being Element of Permutations (n + 2) st tr is being_transposition holds

sgn (tr,K) = - (1_ K)

for K being Field

for tr being Element of Permutations (n + 2) st tr is being_transposition holds

sgn (tr,K) = - (1_ K)

proof end;

theorem Th15: :: MATRIX11:15

for n being Nat

for K being Field

for P being FinSequence of (Group_of_Perm (n + 2))

for p2 being Element of Permutations (n + 2) st p2 = Product P & ( for i being Nat st i in dom P holds

ex trans being Element of Permutations (n + 2) st

( P . i = trans & trans is being_transposition ) ) holds

( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )

for K being Field

for P being FinSequence of (Group_of_Perm (n + 2))

for p2 being Element of Permutations (n + 2) st p2 = Product P & ( for i being Nat st i in dom P holds

ex trans being Element of Permutations (n + 2) st

( P . i = trans & trans is being_transposition ) ) holds

( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )

proof end;

theorem Th16: :: MATRIX11:16

for i, j, n being Nat st i < j & i in Seg n & j in Seg n holds

ex tr being Element of Permutations n st

( tr is being_transposition & tr . i = j )

ex tr being Element of Permutations n st

( tr is being_transposition & tr . i = j )

proof end;

theorem Th17: :: MATRIX11:17

for k being Nat

for p being Element of Permutations (k + 1) st p . (k + 1) <> k + 1 holds

ex tr being Element of Permutations (k + 1) st

( tr is being_transposition & tr . (p . (k + 1)) = k + 1 & (tr * p) . (k + 1) = k + 1 )

for p being Element of Permutations (k + 1) st p . (k + 1) <> k + 1 holds

ex tr being Element of Permutations (k + 1) st

( tr is being_transposition & tr . (p . (k + 1)) = k + 1 & (tr * p) . (k + 1) = k + 1 )

proof end;

theorem Th18: :: MATRIX11:18

for X, x being set st not x in X holds

for p1 being Permutation of (X \/ {x}) st p1 . x = x holds

ex p being Permutation of X st p1 | X = p

for p1 being Permutation of (X \/ {x}) st p1 . x = x holds

ex p being Permutation of X st p1 | X = p

proof end;

theorem Th19: :: MATRIX11:19

for X, x being set

for p, q being Permutation of X

for p1, q1 being Permutation of (X \/ {x}) st p1 | X = p & q1 | X = q & p1 . x = x & q1 . x = x holds

( (p1 * q1) | X = p * q & (p1 * q1) . x = x )

for p, q being Permutation of X

for p1, q1 being Permutation of (X \/ {x}) st p1 | X = p & q1 | X = q & p1 . x = x & q1 . x = x holds

( (p1 * q1) | X = p * q & (p1 * q1) . x = x )

proof end;

theorem Th20: :: MATRIX11:20

for k being Nat

for tr being Element of Permutations k st tr is being_transposition holds

( tr * tr = idseq k & tr = tr " )

for tr being Element of Permutations k st tr is being_transposition holds

( tr * tr = idseq k & tr = tr " )

proof end;

::------------------------------------------::

:: A general theorem about ::

:: the representation of a permutation as ::

:: a product of transpositions ::

::------------------------------------------::

:: A general theorem about ::

:: the representation of a permutation as ::

:: a product of transpositions ::

::------------------------------------------::

theorem Th21: :: MATRIX11:21

for n being Nat

for perm being Element of Permutations n ex P being FinSequence of (Group_of_Perm n) st

( perm = Product P & ( for i being Nat st i in dom P holds

ex trans being Element of Permutations n st

( P . i = trans & trans is being_transposition ) ) )

for perm being Element of Permutations n ex P being FinSequence of (Group_of_Perm n) st

( perm = Product P & ( for i being Nat st i in dom P holds

ex trans being Element of Permutations n st

( P . i = trans & trans is being_transposition ) ) )

proof end;

::------------------------------------------::

:: The relation between sign and parity ::

:: of permutations ::

::------------------------------------------::

:: The relation between sign and parity ::

:: of permutations ::

::------------------------------------------::

theorem Th23: :: MATRIX11:23

for n being Nat

for perm2 being Element of Permutations (n + 2)

for K being Fanoian Field holds

( ( perm2 is even implies sgn (perm2,K) = 1_ K ) & ( sgn (perm2,K) = 1_ K implies perm2 is even ) & ( perm2 is odd implies sgn (perm2,K) = - (1_ K) ) & ( sgn (perm2,K) = - (1_ K) implies perm2 is odd ) )

for perm2 being Element of Permutations (n + 2)

for K being Fanoian Field holds

( ( perm2 is even implies sgn (perm2,K) = 1_ K ) & ( sgn (perm2,K) = 1_ K implies perm2 is even ) & ( perm2 is odd implies sgn (perm2,K) = - (1_ K) ) & ( sgn (perm2,K) = - (1_ K) implies perm2 is odd ) )

proof end;

::------------------------------------------::

:: The sign of a composition of ::

:: permutations ::

::------------------------------------------::

:: The sign of a composition of ::

:: permutations ::

::------------------------------------------::

theorem Th24: :: MATRIX11:24

for n being Nat

for K being Field

for p2, q2, pq2 being Element of Permutations (n + 2) st pq2 = p2 * q2 holds

sgn (pq2,K) = (sgn (p2,K)) * (sgn (q2,K))

for K being Field

for p2, q2, pq2 being Element of Permutations (n + 2) st pq2 = p2 * q2 holds

sgn (pq2,K) = (sgn (p2,K)) * (sgn (q2,K))

proof end;

Lm3: for n being Nat

for p being Element of Permutations n st n < 2 holds

( p is even & p = idseq n )

proof end;

theorem Th25: :: MATRIX11:25

for n being Nat

for p, q being Element of Permutations n holds

( ( ( p is even & q is even ) or ( p is odd & q is odd ) ) iff p * q is even )

for p, q being Element of Permutations n holds

( ( ( p is even & q is even ) or ( p is odd & q is odd ) ) iff p * q is even )

proof end;

theorem Th26: :: MATRIX11:26

for n being Nat

for K being Field

for a being Element of K

for perm2 being Element of Permutations (n + 2) holds - (a,perm2) = (sgn (perm2,K)) * a

for K being Field

for a being Element of K

for perm2 being Element of Permutations (n + 2) holds - (a,perm2) = (sgn (perm2,K)) * a

proof end;

theorem Th27: :: MATRIX11:27

for n being Nat

for tr being Element of Permutations (n + 2) st tr is being_transposition holds

tr is odd

for tr being Element of Permutations (n + 2) st tr is being_transposition holds

tr is odd

proof end;

registration

let n be Nat;

ex b_{1} being Permutation of (Seg (n + 2)) st b_{1} is odd

end;
cluster Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty total quasi_total onto bijective finite odd for Element of bool [:(Seg (n + 2)),(Seg (n + 2)):];

existence ex b

proof end;

begin

definition

let l, n, m be Nat;

let D be non empty set ;

let M be Matrix of n,m,D;

let pD be FinSequence of D;

for b_{1} being Matrix of n,m,D holds verum
;

existence

( ( len pD = width M implies ex b_{1} being Matrix of n,m,D st

( len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( i <> l implies b_{1} * (i,j) = M * (i,j) ) & ( i = l implies b_{1} * (l,j) = pD . j ) ) ) ) ) & ( not len pD = width M implies ex b_{1} being Matrix of n,m,D st b_{1} = M ) )

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

( ( len pD = width M & len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( i <> l implies b_{1} * (i,j) = M * (i,j) ) & ( i = l implies b_{1} * (l,j) = pD . j ) ) ) & len b_{2} = len M & width b_{2} = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( i <> l implies b_{2} * (i,j) = M * (i,j) ) & ( i = l implies b_{2} * (l,j) = pD . j ) ) ) implies b_{1} = b_{2} ) & ( not len pD = width M & b_{1} = M & b_{2} = M implies b_{1} = b_{2} ) )

end;
let D be non empty set ;

let M be Matrix of n,m,D;

let pD be FinSequence of D;

func ReplaceLine (M,l,pD) -> Matrix of n,m,D means :Def3: :: MATRIX11:def 3

( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( i <> l implies it * (i,j) = M * (i,j) ) & ( i = l implies it * (l,j) = pD . j ) ) ) ) if len pD = width M

otherwise it = M;

consistency ( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( i <> l implies it * (i,j) = M * (i,j) ) & ( i = l implies it * (l,j) = pD . j ) ) ) ) if len pD = width M

otherwise it = M;

for b

existence

( ( len pD = width M implies ex b

( len b

( ( i <> l implies b

proof end;

uniqueness for b

( ( len pD = width M & len b

( ( i <> l implies b

( ( i <> l implies b

proof end;

:: deftheorem Def3 defines ReplaceLine MATRIX11:def 3 :

for l, n, m being Nat

for D being non empty set

for M being Matrix of n,m,D

for pD being FinSequence of D

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

( ( len pD = width M implies ( b_{7} = ReplaceLine (M,l,pD) iff ( len b_{7} = len M & width b_{7} = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( i <> l implies b_{7} * (i,j) = M * (i,j) ) & ( i = l implies b_{7} * (l,j) = pD . j ) ) ) ) ) ) & ( not len pD = width M implies ( b_{7} = ReplaceLine (M,l,pD) iff b_{7} = M ) ) );

for l, n, m being Nat

for D being non empty set

for M being Matrix of n,m,D

for pD being FinSequence of D

for b

( ( len pD = width M implies ( b

( ( i <> l implies b

notation

let l, n, m be Nat;

let D be non empty set ;

let M be Matrix of n,m,D;

let pD be FinSequence of D;

synonym RLine (M,l,pD) for ReplaceLine (M,l,pD);

end;
let D be non empty set ;

let M be Matrix of n,m,D;

let pD be FinSequence of D;

synonym RLine (M,l,pD) for ReplaceLine (M,l,pD);

Lm4: for m, n being Nat

for D being non empty set

for l being Nat

for M being Matrix of n,m,D

for pD being FinSequence of D holds

( Indices M = Indices (RLine (M,l,pD)) & len M = len (RLine (M,l,pD)) & width M = width (RLine (M,l,pD)) )

proof end;

theorem Th28: :: MATRIX11:28

for m, n being Nat

for D being non empty set

for l being Nat

for M being Matrix of n,m,D

for pD being FinSequence of D

for i being Nat st i in Seg n holds

( ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )

for D being non empty set

for l being Nat

for M being Matrix of n,m,D

for pD being FinSequence of D

for i being Nat st i in Seg n holds

( ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )

proof end;

theorem :: MATRIX11:29

for m, n, l being Nat

for D being non empty set

for M being Matrix of n,m,D

for pD being FinSequence of D st len pD = width M holds

for p9 being Element of D * st pD = p9 holds

RLine (M,l,pD) = Replace (M,l,p9)

for D being non empty set

for M being Matrix of n,m,D

for pD being FinSequence of D st len pD = width M holds

for p9 being Element of D * st pD = p9 holds

RLine (M,l,pD) = Replace (M,l,p9)

proof end;

theorem Th30: :: MATRIX11:30

for n, m, l being Nat

for D being non empty set

for M being Matrix of n,m,D holds M = RLine (M,l,(Line (M,l)))

for D being non empty set

for M being Matrix of n,m,D holds M = RLine (M,l,(Line (M,l)))

proof end;

Lm5: for K being Field

for pK being FinSequence of K

for a being Element of K holds len pK = len (a * pK)

proof end;

Lm6: for K being Field

for pK, qK being FinSequence of K st len pK = len qK holds

len pK = len (pK + qK)

proof end;

theorem Th31: :: MATRIX11:31

for n being Nat

for K being Field

for a, b being Element of K

for l being Nat

for pK, qK being FinSequence of K

for perm being Element of Permutations n st l in Seg n & len pK = n & len qK = n holds

for M being Matrix of n,K holds the multF of K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) = (a * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))))) + (b * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK))))))

for K being Field

for a, b being Element of K

for l being Nat

for pK, qK being FinSequence of K

for perm being Element of Permutations n st l in Seg n & len pK = n & len qK = n holds

for M being Matrix of n,K holds the multF of K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) = (a * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))))) + (b * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK))))))

proof end;

theorem Th32: :: MATRIX11:32

for n being Nat

for K being Field

for a, b being Element of K

for l being Nat

for pK, qK being FinSequence of K

for perm being Element of Permutations n st l in Seg n & len pK = n & len qK = n holds

for M being Matrix of n,K holds (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))

for K being Field

for a, b being Element of K

for l being Nat

for pK, qK being FinSequence of K

for perm being Element of Permutations n st l in Seg n & len pK = n & len qK = n holds

for M being Matrix of n,K holds (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))

proof end;

::------------------------------------------::

:: The determinant of a linear ::

:: combination of lines ::

::------------------------------------------::

:: The determinant of a linear ::

:: combination of lines ::

::------------------------------------------::

theorem Th33: :: MATRIX11:33

for n being Nat

for K being Field

for a, b being Element of K

for l being Nat

for pK, qK being FinSequence of K st l in Seg n & len pK = n & len qK = n holds

for M being Matrix of n,K holds Det (RLine (M,l,((a * pK) + (b * qK)))) = (a * (Det (RLine (M,l,pK)))) + (b * (Det (RLine (M,l,qK))))

for K being Field

for a, b being Element of K

for l being Nat

for pK, qK being FinSequence of K st l in Seg n & len pK = n & len qK = n holds

for M being Matrix of n,K holds Det (RLine (M,l,((a * pK) + (b * qK)))) = (a * (Det (RLine (M,l,pK)))) + (b * (Det (RLine (M,l,qK))))

proof end;

theorem Th34: :: MATRIX11:34

for l, n being Nat

for K being Field

for a being Element of K

for pK being FinSequence of K

for A being Matrix of n,K st l in Seg n & len pK = n holds

Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))

for K being Field

for a being Element of K

for pK being FinSequence of K

for A being Matrix of n,K st l in Seg n & len pK = n holds

Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))

proof end;

theorem :: MATRIX11:35

for l, n being Nat

for K being Field

for a being Element of K

for A being Matrix of n,K st l in Seg n holds

Det (RLine (A,l,(a * (Line (A,l))))) = a * (Det A)

for K being Field

for a being Element of K

for A being Matrix of n,K st l in Seg n holds

Det (RLine (A,l,(a * (Line (A,l))))) = a * (Det A)

proof end;

theorem Th36: :: MATRIX11:36

for l, n being Nat

for K being Field

for pK, qK being FinSequence of K

for A being Matrix of n,K st l in Seg n & len pK = n & len qK = n holds

Det (RLine (A,l,(pK + qK))) = (Det (RLine (A,l,pK))) + (Det (RLine (A,l,qK)))

for K being Field

for pK, qK being FinSequence of K

for A being Matrix of n,K st l in Seg n & len pK = n & len qK = n holds

Det (RLine (A,l,(pK + qK))) = (Det (RLine (A,l,pK))) + (Det (RLine (A,l,qK)))

proof end;

Lm7: for n, m being Nat

for D being non empty set

for F being Function of (Seg n),(Seg n)

for M being Matrix of n,m,D holds M * F is Matrix of n,m,D

proof end;

begin

:: and with a Repeated Line

definition

let n, m be Nat;

let D be non empty set ;

let F be Function of (Seg n),(Seg n);

let M be Matrix of n,m,D;

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

( b_{1} = F * M iff ( len b_{1} = len M & width b_{1} = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds

b_{1} * (i,j) = M * (k,j) ) ) )

coherence

F * M is Matrix of n,m,D;

by Lm7;

end;
let D be non empty set ;

let F be Function of (Seg n),(Seg n);

let M be Matrix of n,m,D;

:: original: *

redefine func M * F -> Matrix of n,m,D means :Def4: :: MATRIX11:def 4

( len it = len M & width it = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds

it * (i,j) = M * (k,j) ) );

compatibility redefine func M * F -> Matrix of n,m,D means :Def4: :: MATRIX11:def 4

( len it = len M & width it = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds

it * (i,j) = M * (k,j) ) );

for b

( b

b

proof end;

correctness coherence

F * M is Matrix of n,m,D;

by Lm7;

:: deftheorem Def4 defines * MATRIX11:def 4 :

for n, m being Nat

for D being non empty set

for F being Function of (Seg n),(Seg n)

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

( b_{6} = M * F iff ( len b_{6} = len M & width b_{6} = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds

b_{6} * (i,j) = M * (k,j) ) ) );

for n, m being Nat

for D being non empty set

for F being Function of (Seg n),(Seg n)

for M, b

( b

b

theorem Th37: :: MATRIX11:37

for n, m being Nat

for D being non empty set

for F being Function of (Seg n),(Seg n)

for M being Matrix of n,m,D holds

( Indices M = Indices (M * F) & ( for i, j being Nat st [i,j] in Indices M holds

ex k being Nat st

( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) ) )

for D being non empty set

for F being Function of (Seg n),(Seg n)

for M being Matrix of n,m,D holds

( Indices M = Indices (M * F) & ( for i, j being Nat st [i,j] in Indices M holds

ex k being Nat st

( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) ) )

proof end;

theorem Th38: :: MATRIX11:38

for n, m being Nat

for D being non empty set

for M being Matrix of n,m,D

for F being Function of (Seg n),(Seg n)

for k being Nat st k in Seg n holds

Line ((M * F),k) = M . (F . k)

for D being non empty set

for M being Matrix of n,m,D

for F being Function of (Seg n),(Seg n)

for k being Nat st k in Seg n holds

Line ((M * F),k) = M . (F . k)

proof end;

theorem Th40: :: MATRIX11:40

for n being Nat

for K being Field

for A being Matrix of n,K

for p being Element of Permutations n

for Perm being Permutation of (Seg n)

for q being Element of Permutations n st q = p * (Perm ") holds

Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm

for K being Field

for A being Matrix of n,K

for p being Element of Permutations n

for Perm being Permutation of (Seg n)

for q being Element of Permutations n st q = p * (Perm ") holds

Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm

proof end;

theorem Th41: :: MATRIX11:41

for n being Nat

for K being Field

for A being Matrix of n,K

for p being Element of Permutations n

for Perm being Permutation of (Seg n)

for q being Element of Permutations n st q = p * (Perm ") holds

the multF of K $$ (Path_matrix (p,(A * Perm))) = the multF of K $$ (Path_matrix (q,A))

for K being Field

for A being Matrix of n,K

for p being Element of Permutations n

for Perm being Permutation of (Seg n)

for q being Element of Permutations n st q = p * (Perm ") holds

the multF of K $$ (Path_matrix (p,(A * Perm))) = the multF of K $$ (Path_matrix (q,A))

proof end;

theorem Th42: :: MATRIX11:42

for n being Nat

for K being Field

for p2, q2 being Element of Permutations (n + 2) st q2 = p2 " holds

sgn (p2,K) = sgn (q2,K)

for K being Field

for p2, q2 being Element of Permutations (n + 2) st q2 = p2 " holds

sgn (p2,K) = sgn (q2,K)

proof end;

theorem Th43: :: MATRIX11:43

for n being Nat

for K being Field

for M being Matrix of n + 2,K

for perm2 being Element of Permutations (n + 2)

for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds

for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 ") holds

(Path_product M) . q2 = (sgn (perm2,K)) * ((Path_product (M * Perm2)) . p2)

for K being Field

for M being Matrix of n + 2,K

for perm2 being Element of Permutations (n + 2)

for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds

for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 ") holds

(Path_product M) . q2 = (sgn (perm2,K)) * ((Path_product (M * Perm2)) . p2)

proof end;

theorem Th44: :: MATRIX11:44

for n being Nat

for perm being Element of Permutations n ex P being Permutation of (Permutations n) st

for p being Element of Permutations n holds P . p = p * perm

for perm being Element of Permutations n ex P being Permutation of (Permutations n) st

for p being Element of Permutations n holds P . p = p * perm

proof end;

theorem Th45: :: MATRIX11:45

for n being Nat

for K being Field

for M being Matrix of n + 2,n + 2,K

for perm2 being Element of Permutations (n + 2)

for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds

Det (M * Perm2) = (sgn (perm2,K)) * (Det M)

for K being Field

for M being Matrix of n + 2,n + 2,K

for perm2 being Element of Permutations (n + 2)

for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds

Det (M * Perm2) = (sgn (perm2,K)) * (Det M)

proof end;

::------------------------------------------::

:: The determinant of a matrix with ::

:: permutated lines ::

::------------------------------------------::

:: The determinant of a matrix with ::

:: permutated lines ::

::------------------------------------------::

theorem Th46: :: MATRIX11:46

for n being Nat

for K being Field

for M being Matrix of n,K

for perm being Element of Permutations n

for Perm being Permutation of (Seg n) st perm = Perm holds

Det (M * Perm) = - ((Det M),perm)

for K being Field

for M being Matrix of n,K

for perm being Element of Permutations n

for Perm being Permutation of (Seg n) st perm = Perm holds

Det (M * Perm) = - ((Det M),perm)

proof end;

theorem Th47: :: MATRIX11:47

for n being Nat

for PERM being Permutation of (Permutations n)

for perm being Element of Permutations n st perm is odd & ( for p being Element of Permutations n holds PERM . p = p * perm ) holds

PERM .: { p where p is Element of Permutations n : p is even } = { q where q is Element of Permutations n : q is odd }

for PERM being Permutation of (Permutations n)

for perm being Element of Permutations n st perm is odd & ( for p being Element of Permutations n holds PERM . p = p * perm ) holds

PERM .: { p where p is Element of Permutations n : p is even } = { q where q is Element of Permutations n : q is odd }

proof end;

Lm8: for n, i, j being Nat st i in Seg n & j in Seg n & i < j holds

ex ODD, EVEN being finite set st

( EVEN = { p where p is Element of Permutations n : p is even } & ODD = { q where q is Element of Permutations n : q is odd } & EVEN /\ ODD = {} & EVEN \/ ODD = Permutations n & ex PERM being Function of EVEN,ODD ex perm being Element of Permutations n st

( perm is being_transposition & perm . i = j & dom PERM = EVEN & PERM is bijective & ( for p being Element of Permutations n st p in EVEN holds

PERM . p = p * perm ) ) )

proof end;

theorem :: MATRIX11:48

for n being Nat st n >= 2 holds

ex ODD, EVEN being finite set st

( EVEN = { p where p is Element of Permutations n : p is even } & ODD = { q where q is Element of Permutations n : q is odd } & EVEN /\ ODD = {} & EVEN \/ ODD = Permutations n & card EVEN = card ODD )

ex ODD, EVEN being finite set st

( EVEN = { p where p is Element of Permutations n : p is even } & ODD = { q where q is Element of Permutations n : q is odd } & EVEN /\ ODD = {} & EVEN \/ ODD = Permutations n & card EVEN = card ODD )

proof end;

theorem Th49: :: MATRIX11:49

for n being Nat

for K being Field

for i, j being Nat st i in Seg n & j in Seg n & i < j holds

for M being Matrix of n,K st Line (M,i) = Line (M,j) holds

for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds

(Path_product M) . q = - ((Path_product M) . p)

for K being Field

for i, j being Nat st i in Seg n & j in Seg n & i < j holds

for M being Matrix of n,K st Line (M,i) = Line (M,j) holds

for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds

(Path_product M) . q = - ((Path_product M) . p)

proof end;

::------------------------------------------::

:: The determinant of a matrix with ::

:: a repeated line ::

::------------------------------------------::

:: The determinant of a matrix with ::

:: a repeated line ::

::------------------------------------------::

theorem Th50: :: MATRIX11:50

for n being Nat

for K being Field

for i, j being Nat st i in Seg n & j in Seg n & i < j holds

for M being Matrix of n,K st Line (M,i) = Line (M,j) holds

Det M = 0. K

for K being Field

for i, j being Nat st i in Seg n & j in Seg n & i < j holds

for M being Matrix of n,K st Line (M,i) = Line (M,j) holds

Det M = 0. K

proof end;

theorem Th51: :: MATRIX11:51

for n being Nat

for K being Field

for A being Matrix of n,K

for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

Det (RLine (A,i,(Line (A,j)))) = 0. K

for K being Field

for A being Matrix of n,K

for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

Det (RLine (A,i,(Line (A,j)))) = 0. K

proof end;

theorem Th52: :: MATRIX11:52

for n being Nat

for K being Field

for a being Element of K

for A being Matrix of n,K

for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

Det (RLine (A,i,(a * (Line (A,j))))) = 0. K

for K being Field

for a being Element of K

for A being Matrix of n,K

for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

Det (RLine (A,i,(a * (Line (A,j))))) = 0. K

proof end;

theorem :: MATRIX11:53

for n being Nat

for K being Field

for a being Element of K

for A being Matrix of n,K

for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

Det A = Det (RLine (A,i,((Line (A,i)) + (a * (Line (A,j))))))

for K being Field

for a being Element of K

for A being Matrix of n,K

for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

Det A = Det (RLine (A,i,((Line (A,i)) + (a * (Line (A,j))))))

proof end;

theorem Th54: :: MATRIX11:54

for n being Nat

for K being Field

for F being Function of (Seg n),(Seg n)

for A being Matrix of n,K st not F in Permutations n holds

Det (A * F) = 0. K

for K being Field

for F being Function of (Seg n),(Seg n)

for A being Matrix of n,K st not F in Permutations n holds

Det (A * F) = 0. K

proof end;

begin

definition

let K be non empty addLoopStr ;

ex b_{1} being BinOp of ( the carrier of K *) st

for p1, p2 being Element of the carrier of K * holds b_{1} . (p1,p2) = p1 + p2

for b_{1}, b_{2} being BinOp of ( the carrier of K *) st ( for p1, p2 being Element of the carrier of K * holds b_{1} . (p1,p2) = p1 + p2 ) & ( for p1, p2 being Element of the carrier of K * holds b_{2} . (p1,p2) = p1 + p2 ) holds

b_{1} = b_{2}

end;
func addFinS K -> BinOp of ( the carrier of K *) means :Def5: :: MATRIX11:def 5

for p1, p2 being Element of the carrier of K * holds it . (p1,p2) = p1 + p2;

existence for p1, p2 being Element of the carrier of K * holds it . (p1,p2) = p1 + p2;

ex b

for p1, p2 being Element of the carrier of K * holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines addFinS MATRIX11:def 5 :

for K being non empty addLoopStr

for b_{2} being BinOp of ( the carrier of K *) holds

( b_{2} = addFinS K iff for p1, p2 being Element of the carrier of K * holds b_{2} . (p1,p2) = p1 + p2 );

for K being non empty addLoopStr

for b

( b

Lm9: for K being non empty addLoopStr

for p1, p2 being Element of the carrier of K * holds dom (p1 + p2) = (dom p1) /\ (dom p2)

proof end;

registration
end;

registration
end;

theorem Th55: :: MATRIX11:55

for K being Field

for A, B being Matrix of K st width A = len B & len B > 0 holds

for i being Nat st i in Seg (len A) holds

ex P being FinSequence of the carrier of K * st

( len P = len B & Line ((A * B),i) = (addFinS K) "**" P & ( for j being Nat st j in Seg (len B) holds

P . j = (A * (i,j)) * (Line (B,j)) ) )

for A, B being Matrix of K st width A = len B & len B > 0 holds

for i being Nat st i in Seg (len A) holds

ex P being FinSequence of the carrier of K * st

( len P = len B & Line ((A * B),i) = (addFinS K) "**" P & ( for j being Nat st j in Seg (len B) holds

P . j = (A * (i,j)) * (Line (B,j)) ) )

proof end;

theorem Th56: :: MATRIX11:56

for n being Nat

for K being Field

for A, B, C being Matrix of n,K

for i being Nat st i in Seg n holds

ex P being FinSequence of K st

( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds

P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )

for K being Field

for A, B, C being Matrix of n,K

for i being Nat st i in Seg n holds

ex P being FinSequence of K st

( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds

P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )

proof end;

theorem Th57: :: MATRIX11:57

for X being set

for Y being non empty set

for x being set st not x in X holds

ex BIJECT being Function of [:(Funcs (X,Y)),Y:],(Funcs ((X \/ {x}),Y)) st

( BIJECT is bijective & ( for f being Function of X,Y

for F being Function of (X \/ {x}),Y st F | X = f holds

BIJECT . (f,(F . x)) = F ) )

for Y being non empty set

for x being set st not x in X holds

ex BIJECT being Function of [:(Funcs (X,Y)),Y:],(Funcs ((X \/ {x}),Y)) st

( BIJECT is bijective & ( for f being Function of X,Y

for F being Function of (X \/ {x}),Y st F | X = f holds

BIJECT . (f,(F . x)) = F ) )

proof end;

theorem Th58: :: MATRIX11:58

for D being non empty set

for X being finite set

for Y being non empty finite set

for x being set st not x in X holds

for F being BinOp of D st F is having_a_unity & F is commutative & F is associative holds

for f being Function of (Funcs (X,Y)),D

for g being Function of (Funcs ((X \/ {x}),Y)),D st ( for H being Function of X,Y

for SF being Element of Fin (Funcs ((X \/ {x}),Y)) st SF = { h where h is Function of (X \/ {x}),Y : h | X = H } holds

F $$ (SF,g) = f . H ) holds

F $$ ((FinOmega (Funcs (X,Y))),f) = F $$ ((FinOmega (Funcs ((X \/ {x}),Y))),g)

for X being finite set

for Y being non empty finite set

for x being set st not x in X holds

for F being BinOp of D st F is having_a_unity & F is commutative & F is associative holds

for f being Function of (Funcs (X,Y)),D

for g being Function of (Funcs ((X \/ {x}),Y)),D st ( for H being Function of X,Y

for SF being Element of Fin (Funcs ((X \/ {x}),Y)) st SF = { h where h is Function of (X \/ {x}),Y : h | X = H } holds

F $$ (SF,g) = f . H ) holds

F $$ ((FinOmega (Funcs (X,Y))),f) = F $$ ((FinOmega (Funcs ((X \/ {x}),Y))),g)

proof end;

theorem Th59: :: MATRIX11:59

for n, m being Nat

for D being non empty set

for A, B being Matrix of n,m,D

for i being Nat st i <= n & 0 < n holds

for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st

( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds

( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )

for D being non empty set

for A, B being Matrix of n,m,D

for i being Nat st i <= n & 0 < n holds

for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st

( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds

( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )

proof end;

Lm10: for n being Nat

for K being Field

for A, B being Matrix of n,n,K

for i being Nat st i <= n & 0 < n holds

ex P being Function of (Funcs ((Seg i),(Seg n))), the carrier of K st

for F being Function of (Seg i),(Seg n)

for M being Matrix of n,n,K st M = (A * B) +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds

( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = (A * B) . j ) ) ) holds

ex Path being FinSequence of K st

( len Path = i & ( for Fj, j being Nat st j in Seg i & Fj = F . j holds

Path . j = A * (j,Fj) ) & P . F = ( the multF of K $$ Path) * (Det M) )

proof end;

theorem Th60: :: MATRIX11:60

for n being Nat

for K being Field

for A, B being Matrix of n,K st 0 < n holds

ex P being Function of (Funcs ((Seg n),(Seg n))), the carrier of K st

( ( for F being Function of (Seg n),(Seg n) ex Path being FinSequence of K st

( len Path = n & ( for Fj, j being Nat st j in Seg n & Fj = F . j holds

Path . j = A * (j,Fj) ) & P . F = ( the multF of K $$ Path) * (Det (B * F)) ) ) & Det (A * B) = the addF of K $$ ((FinOmega (Funcs ((Seg n),(Seg n)))),P) )

for K being Field

for A, B being Matrix of n,K st 0 < n holds

ex P being Function of (Funcs ((Seg n),(Seg n))), the carrier of K st

( ( for F being Function of (Seg n),(Seg n) ex Path being FinSequence of K st

( len Path = n & ( for Fj, j being Nat st j in Seg n & Fj = F . j holds

Path . j = A * (j,Fj) ) & P . F = ( the multF of K $$ Path) * (Det (B * F)) ) ) & Det (A * B) = the addF of K $$ ((FinOmega (Funcs ((Seg n),(Seg n)))),P) )

proof end;

theorem Th61: :: MATRIX11:61

for n being Nat

for K being Field

for A, B being Matrix of n,K st 0 < n holds

ex P being Function of (Permutations n), the carrier of K st

( Det (A * B) = the addF of K $$ ((FinOmega (Permutations n)),P) & ( for perm being Element of Permutations n holds P . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) )

for K being Field

for A, B being Matrix of n,K st 0 < n holds

ex P being Function of (Permutations n), the carrier of K st

( Det (A * B) = the addF of K $$ ((FinOmega (Permutations n)),P) & ( for perm being Element of Permutations n holds P . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) )

proof end;

::------------------------------------------::

:: Determinant of a product of ::

:: two square matrices ::

::------------------------------------------::

:: Determinant of a product of ::

:: two square matrices ::

::------------------------------------------::

theorem :: MATRIX11:62

for n being Nat

for K being Field

for A, B being Matrix of n,K st 0 < n holds

Det (A * B) = (Det A) * (Det B)

for K being Field

for A, B being Matrix of n,K st 0 < n holds

Det (A * B) = (Det A) * (Det B)

proof end;

:: The partial sign of a permutation ::

::------------------------------------------::