let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K
for j0 being Element of NAT st 1 <= j0 & j0 <= n holds
( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) ) )
let K be Field; :: thesis: for A being Matrix of n,K
for j0 being Element of NAT st 1 <= j0 & j0 <= n holds
( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) ) )
let A be Matrix of n,K; :: thesis: for j0 being Element of NAT st 1 <= j0 & j0 <= n holds
( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) ) )
let j0 be Element of NAT ; :: thesis: ( 1 <= j0 & j0 <= n implies ( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) ) ) )
assume A1: ( 1 <= j0 & j0 <= n ) ; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) ) )
A2: ((SwapDiagonal (K,n,j0)) * (A @)) @ = ((A @) @) * ((SwapDiagonal (K,n,j0)) @) by Th30
.= A * ((SwapDiagonal (K,n,j0)) @) by MATRIXR2:29
.= A * (SwapDiagonal (K,n,j0)) by A1, Th50 ;
A3: for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) )
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies ( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) ) )
assume A4: ( 1 <= i & i <= n ) ; :: thesis: ( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) )
then A5: 1 <= n by XXREAL_0:2;
then A6: [i,1] in Indices A by A4, MATRIX_0:31;
[j0,i] in Indices ((SwapDiagonal (K,n,j0)) * (A @)) by A1, A4, MATRIX_0:31;
hence (A * (SwapDiagonal (K,n,j0))) * (i,j0) = ((SwapDiagonal (K,n,j0)) * (A @)) * (j0,i) by A2, MATRIX_0:def 6
.= (A @) * (1,i) by A1, A4, Th48
.= A * (i,1) by A6, MATRIX_0:def 6 ;
:: thesis: (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0)
A7: [i,j0] in Indices A by A1, A4, MATRIX_0:31;
[1,i] in Indices ((SwapDiagonal (K,n,j0)) * (A @)) by A4, A5, MATRIX_0:31;
hence (A * (SwapDiagonal (K,n,j0))) * (i,1) = ((SwapDiagonal (K,n,j0)) * (A @)) * (1,i) by A2, MATRIX_0:def 6
.= (A @) * (j0,i) by A1, A4, Th48
.= A * (i,j0) by A7, MATRIX_0:def 6 ;
:: thesis: verum
end;
for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j)
proof
let i, j be Element of NAT ; :: thesis: ( j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n implies (A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) )
assume that
A8: ( j <> 1 & j <> j0 ) and
A9: ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: (A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j)
A10: [i,j] in Indices A by A9, MATRIX_0:31;
[j,i] in Indices ((SwapDiagonal (K,n,j0)) * (A @)) by A9, MATRIX_0:31;
hence (A * (SwapDiagonal (K,n,j0))) * (i,j) = ((SwapDiagonal (K,n,j0)) * (A @)) * (j,i) by A2, MATRIX_0:def 6
.= (A @) * (j,i) by A1, A8, A9, Th48
.= A * (i,j) by A10, MATRIX_0:def 6 ;
:: thesis: verum
end;
hence ( ( for i being Element of NAT st 1 <= i & i <= n holds
( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds
(A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) ) ) by A3; :: thesis: verum