:: Basic Properties of Determinants of Square Matrices over a Field
:: by Karol P\c{a}k
::
:: Received March 21, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: MATRIX11:1
theorem Th2: :: MATRIX11:2
theorem Th3: :: MATRIX11:3
definition
let n be
Nat;
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
ex b1 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 b1 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b1 . {i,j} = - (1_ K) ) )
uniqueness
for b1, b2 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 b1 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b1 . {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 b2 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b2 . {i,j} = - (1_ K) ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Part_sgn MATRIX11:def 1 :
theorem Th4: :: MATRIX11:4
theorem Th5: :: MATRIX11:5
theorem Th6: :: MATRIX11:6
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)) ) )
theorem Th8: :: MATRIX11:8
theorem Th9: :: MATRIX11:9
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 ) )
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} ) ) )
:: deftheorem defines sgn MATRIX11:def 2 :
theorem Th11: :: MATRIX11:11
theorem Th12: :: MATRIX11:12
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} ) )
theorem Th13: :: MATRIX11:13
theorem Th14: :: MATRIX11:14
theorem Th15: :: MATRIX11:15
theorem Th16: :: MATRIX11:16
theorem Th17: :: MATRIX11:17
theorem Th18: :: MATRIX11:18
theorem Th19: :: MATRIX11:19
theorem Th20: :: MATRIX11:20
theorem Th21: :: MATRIX11:21
theorem Th22: :: MATRIX11:22
theorem Th23: :: MATRIX11:23
theorem Th24: :: MATRIX11:24
Lm3:
for n being Nat
for p being Element of Permutations n st n < 2 holds
( p is even & p = idseq n )
theorem Th25: :: MATRIX11:25
theorem Th26: :: MATRIX11:26
theorem Th27: :: MATRIX11:27
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;
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
for b1 being Matrix of n,m,D holds verum
;
existence
( ( len pD = width M implies ex b1 being Matrix of n,m,D st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b1 * i,j = M * i,j ) & ( i = l implies b1 * l,j = pD . j ) ) ) ) ) & ( not len pD = width M implies ex b1 being Matrix of n,m,D st b1 = M ) )
uniqueness
for b1, b2 being Matrix of n,m,D holds
( ( len pD = width M & len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b1 * i,j = M * i,j ) & ( i = l implies b1 * l,j = pD . j ) ) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b2 * i,j = M * i,j ) & ( i = l implies b2 * l,j = pD . j ) ) ) implies b1 = b2 ) & ( not len pD = width M & b1 = M & b2 = M implies b1 = b2 ) )
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
b7 being
Matrix of
n,
m,
D holds
( (
len pD = width M implies (
b7 = ReplaceLine M,
l,
pD iff (
len b7 = len M &
width b7 = width M & ( for
i,
j being
Nat st
[i,j] in Indices M holds
( (
i <> l implies
b7 * i,
j = M * i,
j ) & (
i = l implies
b7 * l,
j = pD . j ) ) ) ) ) ) & ( not
len pD = width M implies (
b7 = ReplaceLine M,
l,
pD iff
b7 = M ) ) );
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) )
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 ) )
theorem :: MATRIX11:29
theorem Th30: :: MATRIX11:30
Lm5:
for K being Field
for pK being FinSequence of K
for a being Element of K holds len pK = len (a * pK)
Lm6:
for K being Field
for pK, qK being FinSequence of K st len pK = len qK holds
len pK = len (pK + qK)
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))))
theorem Th32: :: MATRIX11:32
theorem Th33: :: MATRIX11:33
theorem Th34: :: MATRIX11:34
theorem :: MATRIX11:35
theorem Th36: :: MATRIX11:36
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
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;
:: 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
for b1 being Matrix of n,m,D holds
( b1 = F * M iff ( len b1 = len M & width b1 = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
b1 * i,j = M * k,j ) ) )
correctness
coherence
F * M is Matrix of n,m,D;
by Lm7;
end;
:: 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,
b6 being
Matrix of
n,
m,
D holds
(
b6 = M * F iff (
len b6 = len M &
width b6 = width M & ( for
i,
j,
k being
Nat st
[i,j] in Indices M &
F . i = k holds
b6 * i,
j = M * k,
j ) ) );
theorem Th37: :: MATRIX11:37
theorem Th38: :: MATRIX11:38
theorem Th39: :: MATRIX11:39
theorem Th40: :: MATRIX11:40
theorem Th41: :: MATRIX11:41
theorem Th42: :: MATRIX11:42
theorem Th43: :: MATRIX11:43
theorem Th44: :: MATRIX11:44
theorem Th45: :: MATRIX11:45
theorem Th46: :: MATRIX11:46
theorem Th47: :: MATRIX11:47
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 : not q is even } & 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 ) ) )
theorem :: MATRIX11:48
theorem Th49: :: MATRIX11:49
theorem Th50: :: MATRIX11:50
theorem Th51: :: MATRIX11:51
theorem Th52: :: MATRIX11:52
theorem :: MATRIX11:53
theorem Th54: :: MATRIX11:54
:: deftheorem Def5 defines addFinS MATRIX11:def 5 :
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)
theorem Th55: :: MATRIX11:55
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))) ) )
theorem Th57: :: MATRIX11:57
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 &
F is
having_an_inverseOp 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
theorem Th59: :: MATRIX11:59
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) )
theorem Th60: :: MATRIX11:60
theorem Th61: :: MATRIX11:61
theorem :: MATRIX11:62