let K be Ring; for a being Element of K holds Det <*<*a*>*> = a
let a be Element of K; Det <*<*a*>*> = a
set M = <*<*a*>*>;
A1:
(Path_product <*<*a*>*>) . (idseq 1) = a
proof
reconsider p =
idseq 1 as
Element of
Permutations 1
by MATRIX_1:def 12;
A2:
- (
a,
p)
= a
A3:
len (Path_matrix (p,<*<*a*>*>)) = 1
by Def7;
then A4:
dom (Path_matrix (p,<*<*a*>*>)) = Seg 1
by FINSEQ_1:def 3;
then A5:
1
in dom (Path_matrix (p,<*<*a*>*>))
by FINSEQ_1:2, TARSKI:def 1;
then
1
= p . 1
by A4, FUNCT_1:18;
then
(Path_matrix (p,<*<*a*>*>)) . 1
= <*<*a*>*> * (1,1)
by A5, Def7;
then
(Path_matrix (p,<*<*a*>*>)) . 1
= a
by MATRIX_0:49;
then A6:
Path_matrix (
p,
<*<*a*>*>)
= <*a*>
by A3, FINSEQ_1:40;
(
(Path_product <*<*a*>*>) . p = - (
( the multF of K $$ (Path_matrix (p,<*<*a*>*>))),
p) &
<*a*> = 1
|-> a )
by Def8, FINSEQ_2:59;
hence
(Path_product <*<*a*>*>) . (idseq 1) = a
by A6, A2, FINSOP_1:16;
verum
end;
Permutations 1 in Fin (Permutations 1)
by FINSUB_1:def 5;
then
In ((Permutations 1),(Fin (Permutations 1))) = Permutations 1
by SUBSET_1:def 8;
then
( In ((Permutations 1),(Fin (Permutations 1))) = {(idseq 1)} & idseq 1 in Permutations 1 )
by MATRIX_1:10, TARSKI:def 1;
hence
Det <*<*a*>*> = a
by A1, SETWISEO:17; verum