let K be Field; for a, b, c, d being Element of K
for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*>
let a, b, c, d be Element of K; for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*>
let p be Element of Permutations 2; ( p = idseq 2 implies Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*> )
assume A1:
p = idseq 2
; Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*>
A2:
len (Path_matrix (p,((a,b) ][ (c,d)))) = 2
by MATRIX_3:def 7;
then A3:
dom (Path_matrix (p,((a,b) ][ (c,d)))) = Seg 2
by FINSEQ_1:def 3;
then A4:
2 in dom (Path_matrix (p,((a,b) ][ (c,d))))
;
then
2 = p . 2
by A1, A3, FUNCT_1:18;
then A5: (Path_matrix (p,((a,b) ][ (c,d)))) . 2 =
((a,b) ][ (c,d)) * (2,2)
by A4, MATRIX_3:def 7
.=
d
by MATRIX_0:50
;
A6:
1 in dom (Path_matrix (p,((a,b) ][ (c,d))))
by A3;
then
1 = p . 1
by A1, A3, FUNCT_1:18;
then (Path_matrix (p,((a,b) ][ (c,d)))) . 1 =
((a,b) ][ (c,d)) * (1,1)
by A6, MATRIX_3:def 7
.=
a
by MATRIX_0:50
;
hence
Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*>
by A2, A5, FINSEQ_1:44; verum