reconsider s1 = <*1,2*>, s2 = <*2,1*> as Permutation of (Seg 2) by Th2;
let K be Field; for M being Matrix of 2,K holds Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))
let M be Matrix of 2,K; Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))
set D0 = {s1,s2};
reconsider l0 = <*> {s1,s2} as FinSequence of (Group_of_Perm 2) by Th3, MATRIX_1:def 13;
set X = Permutations 2;
reconsider p1 = s1, p2 = s2 as Element of Permutations 2 by MATRIX_1:def 12;
set Y = the carrier of K;
set f = Path_product M;
set F = the addF of K;
set di = the multF of K $$ (Path_matrix (p1,M));
set B = In ((Permutations 2),(Fin (Permutations 2)));
Permutations 2 in Fin (Permutations 2)
by FINSUB_1:def 5;
then A3:
In ((Permutations 2),(Fin (Permutations 2))) = Permutations 2
by SUBSET_1:def 8;
Det M = the addF of K $$ ((In ((Permutations 2),(Fin (Permutations 2)))),(Path_product M))
by MATRIX_3:def 9;
then consider G being Function of (Fin (Permutations 2)), the carrier of K such that
A4:
Det M = G . (In ((Permutations 2),(Fin (Permutations 2))))
and
for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G . {} = e
and
A5:
for x being Element of Permutations 2 holds G . {x} = (Path_product M) . x
and
A6:
for B9 being Element of Fin (Permutations 2) st B9 c= In ((Permutations 2),(Fin (Permutations 2))) & B9 <> {} holds
for x being Element of Permutations 2 st x in (In ((Permutations 2),(Fin (Permutations 2)))) \ B9 holds
G . (B9 \/ {x}) = the addF of K . ((G . B9),((Path_product M) . x))
by A3, SETWISEO:def 3;
A7:
G . {p1} = (Path_product M) . p1
by A5;
A8:
G . (In ((Permutations 2),(Fin (Permutations 2)))) = the addF of K . (((Path_product M) . p1),((Path_product M) . p2))
proof
reconsider B9 =
{.p1.} as
Element of
Fin (Permutations 2) ;
A9:
B9 c= In (
(Permutations 2),
(Fin (Permutations 2)))
(In ((Permutations 2),(Fin (Permutations 2)))) \ B9 = {s2}
by A1, A3, Th3, ZFMISC_1:17;
then
s2 in (In ((Permutations 2),(Fin (Permutations 2)))) \ B9
by TARSKI:def 1;
then
G . (B9 \/ {p2}) = the
addF of
K . (
(G . B9),
((Path_product M) . p2))
by A6, A9;
hence
G . (In ((Permutations 2),(Fin (Permutations 2)))) = the
addF of
K . (
((Path_product M) . p1),
((Path_product M) . p2))
by A3, A7, Th3, ENUMSET1:1;
verum
end;
set dj = the multF of K $$ (Path_matrix (p2,M));
A10:
p1 . 2 = 2
by FINSEQ_1:44;
A11:
p2 . 2 = 1
by FINSEQ_1:44;
A12:
len (Path_matrix (p1,M)) = 2
by MATRIX_3:def 7;
then consider f3 being sequence of the carrier of K such that
A13:
f3 . 1 = (Path_matrix (p1,M)) . 1
and
A14:
for n being Nat st 0 <> n & n < 2 holds
f3 . (n + 1) = the multF of K . ((f3 . n),((Path_matrix (p1,M)) . (n + 1)))
and
A15:
the multF of K $$ (Path_matrix (p1,M)) = f3 . 2
by FINSOP_1:def 1;
A16:
1 in Seg 2
;
then A17:
1 in dom (Path_matrix (p1,M))
by A12, FINSEQ_1:def 3;
A18:
2 in Seg 2
;
then
2 in dom (Path_matrix (p1,M))
by A12, FINSEQ_1:def 3;
then A19:
( p1 . 1 = 1 & (Path_matrix (p1,M)) . 2 = M * (2,2) )
by A10, FINSEQ_1:44, MATRIX_3:def 7;
A20:
len (Path_matrix (p2,M)) = 2
by MATRIX_3:def 7;
then consider f4 being sequence of the carrier of K such that
A21:
f4 . 1 = (Path_matrix (p2,M)) . 1
and
A22:
for n being Nat st 0 <> n & n < 2 holds
f4 . (n + 1) = the multF of K . ((f4 . n),((Path_matrix (p2,M)) . (n + 1)))
and
A23:
the multF of K $$ (Path_matrix (p2,M)) = f4 . 2
by FINSOP_1:def 1;
A24:
1 in dom (Path_matrix (p2,M))
by A20, A16, FINSEQ_1:def 3;
2 in dom (Path_matrix (p2,M))
by A20, A18, FINSEQ_1:def 3;
then A25:
( p2 . 1 = 2 & (Path_matrix (p2,M)) . 2 = M * (2,1) )
by A11, FINSEQ_1:44, MATRIX_3:def 7;
A26: f4 . (1 + 1) =
the multF of K . ((f4 . 1),((Path_matrix (p2,M)) . (1 + 1)))
by A22
.=
(M * (1,2)) * (M * (2,1))
by A24, A25, A21, MATRIX_3:def 7
;
A27:
len (Permutations 2) = 2
by MATRIX_1:9;
for l being FinSequence of (Group_of_Perm 2) holds
( not (len l) mod 2 = 0 or not s2 = Product l or ex i being Nat st
( i in dom l & ( for q being Element of Permutations 2 holds
( not l . i = q or not q is being_transposition ) ) ) )
by Lm1, Th11;
then
( (Path_product M) . p2 = - (( the multF of K "**" (Path_matrix (p2,M))),p2) & p2 is odd )
by A27, MATRIX_3:def 8;
then A28:
(Path_product M) . p2 = - ( the multF of K $$ (Path_matrix (p2,M)))
by MATRIX_1:def 16;
A29: Product l0 =
Product (<*> the carrier of (Group_of_Perm 2))
.=
1_ (Group_of_Perm 2)
by GROUP_4:8
.=
p1
by FINSEQ_2:52, MATRIX_1:15
;
A30:
0 mod 2 = 0
by NAT_D:26;
ex l being FinSequence of (Group_of_Perm 2) st
( (len l) mod 2 = 0 & s1 = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 2 st
( l . i = q & q is being_transposition ) ) )
then A31:
( (Path_product M) . p1 = - (( the multF of K "**" (Path_matrix (p1,M))),p1) & p1 is even )
by A27, MATRIX_3:def 8;
f3 . (1 + 1) =
the multF of K . ((f3 . 1),((Path_matrix (p1,M)) . (1 + 1)))
by A14
.=
(M * (1,1)) * (M * (2,2))
by A17, A19, A13, MATRIX_3:def 7
;
hence
Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))
by A4, A8, A15, A23, A26, A31, A28, MATRIX_1:def 16; verum