environ
vocabularies HIDDEN, NUMBERS, NAT_1, VECTSP_1, FINSUB_1, TARSKI, XBOOLE_0, SUBSET_1, FINSEQ_2, FINSET_1, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_5, FUNCT_2, CARD_1, MATRIX_1, STRUCT_0, ALGSTR_0, SETWISEO, MATRIX_3, CALCUL_2, XXREAL_0, SUPINF_2, FUNCOP_1, BINOP_1, ARYTM_3, ORDINAL4, TREES_1, ZFMISC_1, ARYTM_1, CARD_3, ABIAN, INT_1, PARTFUN1, GROUP_1, FUNCT_7, MATRIX_9;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, ENUMSET1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, SETWISEO, GROUP_4, SETWOP_2, FINSUB_1, MATRIX_0, FINSEQ_4, FINSEQ_5, MATRIX_1, MATRIX_3, XXREAL_0;
definitions ;
theorems FINSEQ_1, FINSEQ_2, TARSKI, FUNCT_2, NAT_1, BINOP_1, FUNCT_1, SETWISEO, ZFMISC_1, FVSUM_1, SETWOP_2, MATRIX_0, MATRIX_1, FUNCOP_1, FINSUB_1, FINSEQ_3, RLVECT_1, RELAT_1, FINSOP_1, XBOOLE_0, XBOOLE_1, MATRIX_3, FINSEQ_5, ENUMSET1, FINSEQ_6, GROUP_4, XREAL_1, MATRIX_7, XXREAL_0, ORDINAL1, NAT_D, PARTFUN1, CARD_1, SUBSET_1;
schemes FUNCT_2, FINSET_1, NAT_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, GROUP_1, VECTSP_1, MATRIX_1, FVSUM_1, RELSET_1, FINSEQ_2, CARD_1;
constructors HIDDEN, BINOP_1, SETWISEO, NAT_1, NAT_D, FINSEQ_4, FINSOP_1, FINSEQ_5, ALGSTR_1, GROUP_4, MATRIX_7, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_2, FINSEQ_1, ALGSTR_0;
expansions ;
Lm1:
<*1,2*> <> <*2,1*>
by FINSEQ_1:77;
Lm2:
<*2,1*> in Permutations 2
by MATRIX_7:3, TARSKI:def 2;
theorem Th19:
Permutations 3
= {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
theorem Th20:
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*1,2,3*> holds
Path_matrix (
p,
M)
= <*a,e,i*>
theorem Th21:
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*3,2,1*> holds
Path_matrix (
p,
M)
= <*c,e,g*>
theorem Th22:
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*1,3,2*> holds
Path_matrix (
p,
M)
= <*a,f,h*>
theorem Th23:
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*2,3,1*> holds
Path_matrix (
p,
M)
= <*b,f,g*>
theorem Th24:
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*2,1,3*> holds
Path_matrix (
p,
M)
= <*b,d,i*>
theorem Th25:
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*3,1,2*> holds
Path_matrix (
p,
M)
= <*c,d,h*>
theorem Th27:
(
<*1,3,2*> in Permutations 3 &
<*2,3,1*> in Permutations 3 &
<*2,1,3*> in Permutations 3 &
<*3,1,2*> in Permutations 3 &
<*1,2,3*> in Permutations 3 &
<*3,2,1*> in Permutations 3 )
Lm3:
<*1,2,3*> <> <*3,2,1*>
by FINSEQ_1:78;
Lm4:
<*1,2,3*> <> <*1,3,2*>
by FINSEQ_1:78;
Lm5:
<*1,2,3*> <> <*2,1,3*>
by FINSEQ_1:78;
Lm6:
( <*1,2,3*> <> <*2,3,1*> & <*1,2,3*> <> <*3,1,2*> )
by FINSEQ_1:78;
Lm7:
( <*3,2,1*> <> <*2,3,1*> & <*3,2,1*> <> <*3,1,2*> )
by FINSEQ_1:78;
Lm8:
( <*3,2,1*> <> <*2,1,3*> & <*1,3,2*> <> <*2,1,3*> )
by FINSEQ_1:78;
Lm9:
( <*1,3,2*> <> <*2,3,1*> & <*1,3,2*> <> <*3,1,2*> )
by FINSEQ_1:78;
Lm10:
( <*3,2,1*> <> <*1,3,2*> & <*2,3,1*> <> <*3,1,2*> )
by FINSEQ_1:78;
Lm11:
( <*2,3,1*> <> <*2,1,3*> & <*2,1,3*> <> <*3,1,2*> )
by FINSEQ_1:78;
theorem Th37:
(
<*2,1,3*> * <*1,3,2*> = <*2,3,1*> &
<*1,3,2*> * <*2,1,3*> = <*3,1,2*> &
<*2,1,3*> * <*3,2,1*> = <*3,1,2*> &
<*3,2,1*> * <*2,1,3*> = <*2,3,1*> &
<*3,2,1*> * <*3,2,1*> = <*1,2,3*> &
<*2,1,3*> * <*2,1,3*> = <*1,2,3*> &
<*1,3,2*> * <*1,3,2*> = <*1,2,3*> &
<*1,3,2*> * <*2,3,1*> = <*3,2,1*> &
<*2,3,1*> * <*2,3,1*> = <*3,1,2*> &
<*2,3,1*> * <*3,1,2*> = <*1,2,3*> &
<*3,1,2*> * <*2,3,1*> = <*1,2,3*> &
<*3,1,2*> * <*3,1,2*> = <*2,3,1*> &
<*1,3,2*> * <*3,2,1*> = <*2,3,1*> &
<*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
Lm12:
<*1,2,3*> is even Permutation of (Seg 3)
by FINSEQ_2:53, MATRIX_1:16;
Lm13:
<*2,3,1*> is even Permutation of (Seg 3)
Lm14:
<*3,1,2*> is even Permutation of (Seg 3)
Lm15:
for p being Permutation of (Seg 3) holds p * <*1,2,3*> = p
Lm16:
for p being Permutation of (Seg 3) holds <*1,2,3*> * p = p
Lm17:
for l being FinSequence of (Group_of_Perm 3) st (len l) mod 2 = 0 & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) & not Product l = <*1,2,3*> & not Product l = <*2,3,1*> holds
Product l = <*3,1,2*>
theorem
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
theorem
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)
Lm18:
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M)) = 0. K