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

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