let n be Nat; for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds
for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K
let K be commutative Ring; ( not K is degenerated & K is well-unital & K is domRing-like implies for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K )
assume A0:
( not K is degenerated & K is well-unital & K is domRing-like )
; for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K
let i, j be Nat; ( i in Seg n & j in Seg n & i < j implies for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K )
assume that
A1:
i in Seg n
and
A2:
j in Seg n
and
A3:
i < j
; for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K
set P = Permutations n;
consider Q, E being finite set such that
( E = { p where p is Element of Permutations n : p is even } & Q = { q where q is Element of Permutations n : q is odd } )
and
A4:
( E /\ Q = {} & E \/ Q = Permutations n )
and
A5:
ex P being Function of E,Q ex tr being Element of Permutations n st
( tr is being_transposition & tr . i = j & dom P = E & P is bijective & ( for p being Element of Permutations n st p in E holds
P . p = p * tr ) )
by A1, A2, A3, Lm8;
A6:
E c= Permutations n
by A4, XBOOLE_1:7;
set KK = the carrier of K;
set aa = the addF of K;
let M be Matrix of n,K; ( Line (M,i) = Line (M,j) implies Det M = 0. K )
assume A7:
Line (M,i) = Line (M,j)
; Det M = 0. K
A8:
Q c= Permutations n
by A4, XBOOLE_1:7;
set PathM = Path_product M;
consider PERM being Function of E,Q, tr being Element of Permutations n such that
A9:
tr is being_transposition
and
A10:
tr . i = j
and
A11:
dom PERM = E
and
A12:
PERM is bijective
and
A13:
for p being Element of Permutations n st p in E holds
PERM . p = p * tr
by A5;
reconsider E = E, Q = Q as Element of Fin (Permutations n) by A6, A8, FINSUB_1:def 5;
the addF of K is having_a_unity
by FVSUM_1:8;
then consider GE being Function of (Fin (Permutations n)), the carrier of K such that
A14:
the addF of K $$ (E,(Path_product M)) = GE . E
and
A15:
for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
GE . {} = e
and
A16:
for x being Element of Permutations n holds GE . {x} = (Path_product M) . x
and
A17:
for B9 being Element of Fin (Permutations n) st B9 c= E & B9 <> {} holds
for x being Element of Permutations n st x in E \ B9 holds
GE . (B9 \/ {x}) = the addF of K . ((GE . B9),((Path_product M) . x))
by SETWISEO:def 3;
A18:
E misses Q
by A4;
the addF of K is having_a_unity
by FVSUM_1:8;
then consider GQ being Function of (Fin (Permutations n)), the carrier of K such that
A19:
the addF of K $$ (Q,(Path_product M)) = GQ . Q
and
A20:
for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
GQ . {} = e
and
A21:
for x being Element of Permutations n holds GQ . {x} = (Path_product M) . x
and
A22:
for B9 being Element of Fin (Permutations n) st B9 c= Q & B9 <> {} holds
for x being Element of Permutations n st x in Q \ B9 holds
GQ . (B9 \/ {x}) = the addF of K . ((GQ . B9),((Path_product M) . x))
by SETWISEO:def 3;
defpred S1[ Nat] means for B, PB being Element of Fin (Permutations n) st card B = $1 & B c= E & PERM .: B = PB holds
(GE . B) + (GQ . PB) = 0. K;
A23:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A24:
S1[
k]
;
S1[k + 1]
let B,
PB be
Element of
Fin (Permutations n);
( card B = k + 1 & B c= E & PERM .: B = PB implies (GE . B) + (GQ . PB) = 0. K )
assume that A25:
card B = k + 1
and A26:
B c= E
and A27:
PERM .: B = PB
;
(GE . B) + (GQ . PB) = 0. K
now ( ( k = 0 & (GE . B) + (GQ . PB) = 0. K ) or ( k > 0 & (GQ . PB) + (GE . B) = 0. K ) )per cases
( k = 0 or k > 0 )
;
case
k = 0
;
(GE . B) + (GQ . PB) = 0. Kthen consider x being
object such that A28:
B = {x}
by A25, CARD_2:42;
A29:
x in B
by A28, TARSKI:def 1;
B c= Permutations n
by FINSUB_1:def 5;
then reconsider x =
x as
Element of
Permutations n by A29;
x * tr is
Element of
Permutations n
by MATRIX_9:39;
then reconsider Px =
PERM . x as
Element of
Permutations n by A13, A26, A29;
A30:
Im (
PERM,
x)
= {Px}
by A11, A26, A29, FUNCT_1:59;
A31:
GE . {x} = (Path_product M) . x
by A16;
A32:
GQ . {(PERM . x)} = (Path_product M) . Px
by A21;
Px = x * tr
by A13, A26, A29;
then
- (GE . B) = GQ . PB
by A0, A1, A2, A3, A7, A9, A10, A27, A28, A31, A32, A30, Th49;
hence
(GE . B) + (GQ . PB) = 0. K
by RLVECT_1:def 10;
verum end; case A33:
k > 0
;
(GQ . PB) + (GE . B) = 0. Kconsider x being
object such that A34:
x in B
by A25, CARD_1:27, XBOOLE_0:def 1;
B c= Permutations n
by FINSUB_1:def 5;
then reconsider x =
x as
Element of
Permutations n by A34;
x * tr is
Element of
Permutations n
by MATRIX_9:39;
then reconsider Px =
PERM . x as
Element of
Permutations n by A13, A26, A34;
A35:
Im (
PERM,
x)
= {Px}
by A11, A26, A34, FUNCT_1:59;
Px = x * tr
by A13, A26, A34;
then A36:
- ((Path_product M) . x) = (Path_product M) . Px
by A0, A1, A2, A3, A7, A9, A10, Th49;
A37:
Q c= Permutations n
by FINSUB_1:def 5;
B c= Permutations n
by FINSUB_1:def 5;
then A38:
B \ {x} c= Permutations n
;
A39:
rng PERM = Q
by A12, FUNCT_2:def 3;
then A40:
Px in Q
by A11, A26, A34, FUNCT_1:def 3;
PERM .: (B \ {x}) c= rng PERM
by RELAT_1:111;
then
PERM .: (B \ {x}) c= Permutations n
by A39, A37;
then reconsider B9 =
B \ {x},
PeBx =
PERM .: (B \ {x}) as
Element of
Fin (Permutations n) by A38, FINSUB_1:def 5;
A41:
Px in {Px}
by TARSKI:def 1;
A42:
{x} \/ B9 = B
by A34, ZFMISC_1:116;
then A43:
PERM .: B = (Im (PERM,x)) \/ PeBx
by RELAT_1:120;
B9 misses {x}
by XBOOLE_1:79;
then
B9 /\ {x} = {}
;
then
PERM .: {} = {Px} /\ PeBx
by A12, A35, FUNCT_1:62;
then
not
Px in PeBx
by A41, XBOOLE_0:def 4;
then A44:
Px in Q \ PeBx
by A40, XBOOLE_0:def 5;
A45:
not
x in B9
by ZFMISC_1:56;
then A46:
x in E \ B9
by A26, A34, XBOOLE_0:def 5;
A47:
k + 1
= (card B9) + 1
by A25, A42, A45, CARD_2:41;
then consider y being
object such that A48:
y in B9
by A33, CARD_1:27, XBOOLE_0:def 1;
B \ {x} c= E
by A26;
then
PERM . y in PeBx
by A11, A48, FUNCT_1:def 6;
then
GQ . PB = the
addF of
K . (
(GQ . PeBx),
((Path_product M) . Px))
by A22, A27, A39, A43, A35, A44, RELAT_1:111;
hence (GQ . PB) + (GE . B) =
((GQ . PeBx) - ((Path_product M) . x)) + ((GE . B9) + ((Path_product M) . x))
by A17, A26, A33, A42, A47, A46, A36, CARD_1:27, XBOOLE_1:1
.=
(GQ . PeBx) + ((- ((Path_product M) . x)) + ((GE . B9) + ((Path_product M) . x)))
by RLVECT_1:def 3
.=
(GQ . PeBx) + ((GE . B9) + (((Path_product M) . x) - ((Path_product M) . x)))
by RLVECT_1:def 3
.=
(GQ . PeBx) + ((GE . B9) + (0. K))
by RLVECT_1:def 10
.=
((GQ . PeBx) + (GE . B9)) + (0. K)
by RLVECT_1:def 3
.=
(0. K) + (0. K)
by A24, A26, A47, XBOOLE_1:1
.=
0. K
by RLVECT_1:4
;
verum end;
hence
(GE . B) + (GQ . PB) = 0. K
;
verum
end;
set F = In ((Permutations n),(Fin (Permutations n)));
Permutations n in Fin (Permutations n)
by FINSUB_1:def 5;
then A49:
Permutations n = In ((Permutations n),(Fin (Permutations n)))
by SUBSET_1:def 8;
rng PERM = Q
by A12, FUNCT_2:def 3;
then A50:
PERM .: E = Q
by A11, RELAT_1:113;
A51:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A51, A23);
then
S1[ card E]
;
then
( the addF of K $$ (E,(Path_product M))) + ( the addF of K $$ (Q,(Path_product M))) = 0. K
by A14, A19, A50;
hence
Det M = 0. K
by A4, A18, A49, FVSUM_1:8, SETWOP_2:4; verum