environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, NAT_1, XBOOLE_0, MATRIX11, FINSEQ_1, ARYTM_3, VECTSP_1, MATRIX_1, RELAT_1, FINSEQ_3, ARYTM_1, TREES_1, CARD_1, XXREAL_0, FUNCT_1, INCSP_1, TARSKI, ALGSTR_0, ZFMISC_1, STRUCT_0, REALSET1, SETWOP_2, FUNCT_2, FINSUB_1, GROUP_1, SETWISEO, INT_1, FINSET_1, ABIAN, FINSEQ_2, BINOP_1, QC_LANG1, AFINSQ_1, ABSVALUE, MATRIX_3, SUPINF_2, CARD_3, FINSOP_1, RVSUM_1, FVSUM_1, MESFUNC1, MATRIX_6, LAPLACE, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FINSET_1, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, SETWISEO, SETWOP_2, FINSEQ_2, MATRIX_0, FINSUB_1, MATRIX_1, NAT_1, FVSUM_1, FINSOP_1, MATRIX_3, CARD_1, FINSEQ_7, NEWTON, MATRIX_7, FINSEQ_3, MATRIX11, MATRIX_6, NAT_D;
definitions TARSKI;
theorems FINSEQ_1, FINSEQ_2, TARSKI, FUNCT_2, NAT_1, FUNCT_1, SETWISEO, VECTSP_1, ZFMISC_1, FVSUM_1, SETWOP_2, MATRIX_0, MATRIX_1, FINSUB_1, FINSEQ_3, RELAT_1, FINSOP_1, XBOOLE_0, XBOOLE_1, MATRIX_3, XREAL_1, MATRIX_7, ORDINAL1, CARD_1, CARD_2, MATRIX_9, STIRL2_1, SGRAPH1, CARD_FIN, HURWITZ, NEWTON, COMPUT_1, MATRIX11, GROUP_1, MATRIX_4, MATRIX_6, MATRIXR1, NAT_D, SUBSET_1, XXREAL_0, MATRIXR2, XREAL_0;
schemes FUNCT_2, NAT_1, FINSEQ_1, FUNCT_1, SETWISEO, MATRIX_0;
registrations FUNCT_1, FINSUB_1, FINSET_1, STRUCT_0, FVSUM_1, MATRIX_1, VECTSP_1, FUNCT_2, PARTFUN1, XBOOLE_0, ORDINAL1, XXREAL_0, NAT_1, INT_1, RELAT_1, CARD_1, MATRIX11, XCMPLX_0, RELSET_1, FINSEQ_2, FINSEQ_1, MATRIX_0, MATRIX_6, VECTSP_2;
constructors HIDDEN, SETWISEO, FINSOP_1, SETWOP_2, ALGSTR_1, FVSUM_1, BINOP_1, FINSEQ_4, FINSEQ_7, WELLORD2, NEWTON, MATRIX_6, MATRIX_7, MATRIX11, NAT_D, BINOP_2, RELSET_1, XXREAL_0, NAT_1, VECTSP_2;
requirements HIDDEN, ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
equalities FINSEQ_2, FINSEQ_1, MATRIX_0, MATRIX_3, FVSUM_1, MATRIX11, RELAT_1, ALGSTR_0;
expansions FINSEQ_1, TARSKI;
theorem Th10:
for
n,
i,
j being
Nat st
i in Seg (n + 1) &
n >= 2 holds
ex
Proj being
Function of
(2Set (Seg n)),
(2Set (Seg (n + 1))) st
(
rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } &
Proj is
one-to-one & ( for
k,
m being
Nat st
k < m &
{k,m} in 2Set (Seg n) holds
( (
m < i &
k < i implies
Proj . {k,m} = {k,m} ) & (
m >= i &
k < i implies
Proj . {k,m} = {k,(m + 1)} ) & (
m >= i &
k >= i implies
Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )
theorem Th12:
for
X,
Y,
D being non
empty set for
f being
Function of
X,
(Fin Y) for
g being
Function of
(Fin Y),
D for
F being
BinOp of
D st ( for
A,
B being
Element of
Fin Y st
A misses B holds
F . (
(g . A),
(g . B))
= g . (A \/ B) ) &
F is
commutative &
F is
associative &
F is
having_a_unity &
g . {} = the_unity_wrt F holds
for
I being
Element of
Fin X st ( for
x,
y being
object st
x in I &
y in I &
f . x meets f . y holds
x = y ) holds
(
F $$ (
I,
(g * f))
= F $$ (
(f .: I),
g) &
F $$ (
(f .: I),
g)
= g . (union (f .: I)) &
union (f .: I) is
Element of
Fin Y )
theorem Th13:
for
n being
Nat for
K being
Field for
M being
Matrix of
n,
K for
i,
j being
Nat st
i in Seg n &
j in Seg n holds
for
k,
m being
Nat st
k in Seg (n -' 1) &
m in Seg (n -' 1) holds
( (
k < i &
m < j implies
(Delete (M,i,j)) * (
k,
m)
= M * (
k,
m) ) & (
k < i &
m >= j implies
(Delete (M,i,j)) * (
k,
m)
= M * (
k,
(m + 1)) ) & (
k >= i &
m < j implies
(Delete (M,i,j)) * (
k,
m)
= M * (
(k + 1),
m) ) & (
k >= i &
m >= j implies
(Delete (M,i,j)) * (
k,
m)
= M * (
(k + 1),
(m + 1)) ) )
definition
let c,
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 = len 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
( ( j <> c implies b1 * (i,j) = M * (i,j) ) & ( j = c implies b1 * (i,c) = pD . i ) ) ) ) ) & ( not len pD = len 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 = len M & len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b1 * (i,j) = M * (i,j) ) & ( j = c implies b1 * (i,c) = pD . i ) ) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b2 * (i,j) = M * (i,j) ) & ( j = c implies b2 * (i,c) = pD . i ) ) ) implies b1 = b2 ) & ( not len pD = len M & b1 = M & b2 = M implies b1 = b2 ) )
end;
::
deftheorem Def2 defines
ReplaceCol LAPLACE:def 2 :
for c, 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 = len M implies ( b7 = ReplaceCol (M,c,pD) iff ( len b7 = len M & width b7 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b7 * (i,j) = M * (i,j) ) & ( j = c implies b7 * (i,c) = pD . i ) ) ) ) ) ) & ( not len pD = len M implies ( b7 = ReplaceCol (M,c,pD) iff b7 = M ) ) );
theorem
for
c,
m,
n being
Nat for
D being non
empty set for
AD being
Matrix of
n,
m,
D for
pD being
FinSequence of
D for
i being
Nat st
i in Seg (width AD) holds
( (
i = c &
len pD = len AD implies
Col (
(RCol (AD,c,pD)),
i)
= pD ) & (
i <> c implies
Col (
(RCol (AD,c,pD)),
i)
= Col (
AD,
i) ) )
theorem Th19:
for
c,
m,
n being
Nat for
D being non
empty set for
pD being
FinSequence of
D for
A being
Matrix of
n,
m,
D for
A9 being
Matrix of
m,
n,
D st
A9 = A @ & (
m = 0 implies
n = 0 ) holds
ReplaceCol (
A,
c,
pD)
= (ReplaceLine (A9,c,pD)) @
definition
let i,
n be
Nat;
let perm be
Element of
Permutations (n + 1);
assume A1:
i in Seg (n + 1)
;
func Rem (
perm,
i)
-> Element of
Permutations n means :
Def3:
for
k being
Nat st
k in Seg n holds
( (
k < i implies ( (
perm . k < perm . i implies
it . k = perm . k ) & (
perm . k >= perm . i implies
it . k = (perm . k) - 1 ) ) ) & (
k >= i implies ( (
perm . (k + 1) < perm . i implies
it . k = perm . (k + 1) ) & (
perm . (k + 1) >= perm . i implies
it . k = (perm . (k + 1)) - 1 ) ) ) );
existence
ex b1 being Element of Permutations n st
for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b1 . k = perm . k ) & ( perm . k >= perm . i implies b1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b1 . k = (perm . (k + 1)) - 1 ) ) ) )
uniqueness
for b1, b2 being Element of Permutations n st ( for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b1 . k = perm . k ) & ( perm . k >= perm . i implies b1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b1 . k = (perm . (k + 1)) - 1 ) ) ) ) ) & ( for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b2 . k = perm . k ) & ( perm . k >= perm . i implies b2 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b2 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b2 . k = (perm . (k + 1)) - 1 ) ) ) ) ) holds
b1 = b2
end;
definition
let n be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
existence
ex b1 being Matrix of n,K st
for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = Cofactor (M,i,j)
uniqueness
for b1, b2 being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = Cofactor (M,i,j) ) & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * (i,j) = Cofactor (M,i,j) ) holds
b1 = b2
end;
definition
let n,
i be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
existence
ex b1 being FinSequence of K st
( len b1 = n & ( for j being Nat st j in dom b1 holds
b1 . j = (M * (i,j)) * (Cofactor (M,i,j)) ) )
uniqueness
for b1, b2 being FinSequence of K st len b1 = n & ( for j being Nat st j in dom b1 holds
b1 . j = (M * (i,j)) * (Cofactor (M,i,j)) ) & len b2 = n & ( for j being Nat st j in dom b2 holds
b2 . j = (M * (i,j)) * (Cofactor (M,i,j)) ) holds
b1 = b2
end;
definition
let n,
j be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
existence
ex b1 being FinSequence of K st
( len b1 = n & ( for i being Nat st i in dom b1 holds
b1 . i = (M * (i,j)) * (Cofactor (M,i,j)) ) )
uniqueness
for b1, b2 being FinSequence of K st len b1 = n & ( for i being Nat st i in dom b1 holds
b1 . i = (M * (i,j)) * (Cofactor (M,i,j)) ) & len b2 = n & ( for i being Nat st i in dom b2 holds
b2 . i = (M * (i,j)) * (Cofactor (M,i,j)) ) holds
b1 = b2
end;