begin
theorem Th1:
theorem Th2:
theorem Th3:
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:
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 :
for n being Nat
for K being Field
for perm2 being Element of Permutations (n + 2)
for b4 being Function of (2Set (Seg (n + 2))), the carrier of K holds
( b4 = 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 b4 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b4 . {i,j} = - (1_ K) ) ) );
theorem Th4:
theorem Th5:
theorem Th6:
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)))) ) )
theorem Th8:
theorem Th9:
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} ) ) )
:: 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)));
theorem Th11:
theorem Th12:
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:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
Lm3:
for n being Nat
for p being Element of Permutations n st n < 2 holds
( p is even & p = idseq n )
theorem Th25:
theorem Th26:
theorem Th27:
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;
func ReplaceLine (
M,
l,
pD)
-> Matrix of
n,
m,
D means :
Def3:
(
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:
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
theorem Th30:
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))))))
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem Th36:
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;
*redefine func M * F -> Matrix of
n,
m,
D means :
Def4:
(
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:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
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
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem Th54:
begin
:: deftheorem Def5 defines addFinS MATRIX11:def 5 :
for K being non empty addLoopStr
for b2 being BinOp of ( the carrier of K *) holds
( b2 = addFinS K iff for p1, p2 being Element of the carrier of K * holds b2 . (p1,p2) = p1 + p2 );
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:
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 Th57:
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)
theorem Th59:
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:
theorem Th61:
theorem