begin
definition
let n be
Nat;
let K be
Field;
let perm2 be
Element of
Permutations (n + 2);
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;
theorem Th7:
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)))) ) )
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:
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} ) ) )
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} ) )
Lm3:
for n being Nat
for p being Element of Permutations n st n < 2 holds
( p is even & p = idseq n )
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;
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:
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) ) )
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:
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))))))
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
begin
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;
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) ) ) );
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 ) ) )
begin
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 Th56:
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 Th58:
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)
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) )
:: The partial sign of a permutation ::
::------------------------------------------::