let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for P being Permutation of (Seg n) holds
( Det ((((M * P) @) * P) @) = Det M & ( for i, j being Nat st [i,j] in Indices M holds
((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) ) )
let K be Field; :: thesis: for M being Matrix of n,K
for P being Permutation of (Seg n) holds
( Det ((((M * P) @) * P) @) = Det M & ( for i, j being Nat st [i,j] in Indices M holds
((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) ) )
let M be Matrix of n,K; :: thesis: for P being Permutation of (Seg n) holds
( Det ((((M * P) @) * P) @) = Det M & ( for i, j being Nat st [i,j] in Indices M holds
((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) ) )
let P be Permutation of (Seg n); :: thesis: ( Det ((((M * P) @) * P) @) = Det M & ( for i, j being Nat st [i,j] in Indices M holds
((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) ) )
reconsider p = P as Element of Permutations n by MATRIX_1:def 12;
A1: - (- (Det M)) = Det M by RLVECT_1:17;
A2: ( ( p is even & - ((Det M),p) = Det M ) or ( p is odd & - ((Det M),p) = - (Det M) ) ) by MATRIX_1:def 16;
thus Det ((((M * P) @) * P) @) = Det (((M * P) @) * P) by MATRIXR2:43
.= - ((Det ((M * P) @)),p) by MATRIX11:46
.= - ((Det (M * P)),p) by MATRIXR2:43
.= - ((- ((Det M),p)),p) by MATRIX11:46
.= Det M by A1, A2, MATRIX_1:def 16 ; :: thesis: for i, j being Nat st [i,j] in Indices M holds
((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j))
let i, j be Nat; :: thesis: ( [i,j] in Indices M implies ((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) )
assume A3: [i,j] in Indices M ; :: thesis: ((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j))
Indices M = Indices ((((M * P) @) * P) @) by MATRIX_0:26;
then A4: [j,i] in Indices (((M * P) @) * P) by A3, MATRIX_0:def 6;
then A5: ((((M * P) @) * P) @) * (i,j) = (((M * P) @) * P) * (j,i) by MATRIX_0:def 6;
( Indices M = Indices (((M * P) @) * P) & Indices M = Indices ((M * P) @) ) by MATRIX_0:26;
then A6: ex k being Nat st
( k = P . j & [k,i] in Indices ((M * P) @) & (((M * P) @) * P) * (j,i) = ((M * P) @) * (k,i) ) by A4, MATRIX11:37;
then A7: [i,(P . j)] in Indices (M * P) by MATRIX_0:def 6;
Indices (M * P) = Indices M by MATRIX_0:26;
then (M * P) * (i,(P . j)) = M * ((P . i),(P . j)) by A7, MATRIX11:def 4;
hence ((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) by A5, A6, A7, MATRIX_0:def 6; :: thesis: verum