let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds
ex P being Matrix of n,K st
( P is invertible & (P * A) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds
(P * A) * (1,j) = 0. K ) )
let K be Field; :: thesis: for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds
ex P being Matrix of n,K st
( P is invertible & (P * A) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds
(P * A) * (1,j) = 0. K ) )
let A be Matrix of n,K; :: thesis: ( n > 0 & A * (1,1) <> 0. K implies ex P being Matrix of n,K st
( P is invertible & (P * A) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds
(P * A) * (1,j) = 0. K ) ) )
assume that
A1: n > 0 and
A2: A * (1,1) <> 0. K ; :: thesis: ex P being Matrix of n,K st
( P is invertible & (P * A) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds
(P * A) * (1,j) = 0. K ) )
set B = A @ ;
A3: 0 + 1 <= n by A1, NAT_1:13;
then [1,1] in Indices A by MATRIX_0:31;
then (A @) * (1,1) = A * (1,1) by MATRIX_0:def 6;
then consider P0 being Matrix of n,K such that
A4: P0 is invertible and
A5: ((A @) * P0) * (1,1) = 1. K and
A6: for i being Element of NAT st 1 < i & i <= n holds
((A @) * P0) * (1,i) = 0. K and
A7: for j being Element of NAT st 1 < j & j <= n & (A @) * (j,1) = 0. K holds
((A @) * P0) * (j,1) = 0. K by A1, A2, Th39;
A8: [1,1] in Indices ((A @) * P0) by A3, MATRIX_0:31;
A9: for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds
((P0 @) * A) * (1,j) = 0. K
proof
let j be Element of NAT ; :: thesis: ( 1 < j & j <= n & A * (1,j) = 0. K implies ((P0 @) * A) * (1,j) = 0. K )
assume that
A10: ( 1 < j & j <= n ) and
A11: A * (1,j) = 0. K ; :: thesis: ((P0 @) * A) * (1,j) = 0. K
[1,j] in Indices A by A3, A10, MATRIX_0:31;
then (A @) * (j,1) = A * (1,j) by MATRIX_0:def 6;
then A12: ((A @) * P0) * (j,1) = 0. K by A7, A10, A11;
[j,1] in Indices ((A @) * P0) by A3, A10, MATRIX_0:31;
then (((A @) * P0) @) * (1,j) = 0. K by A12, MATRIX_0:def 6;
then ((P0 @) * ((A @) @)) * (1,j) = 0. K by Th30;
hence ((P0 @) * A) * (1,j) = 0. K by MATRIXR2:29; :: thesis: verum
end;
A13: for i being Element of NAT st 1 < i & i <= n holds
((P0 @) * A) * (i,1) = 0. K
proof
let i be Element of NAT ; :: thesis: ( 1 < i & i <= n implies ((P0 @) * A) * (i,1) = 0. K )
assume ( 1 < i & i <= n ) ; :: thesis: ((P0 @) * A) * (i,1) = 0. K
then A14: ( [1,i] in Indices ((A @) * P0) & ((A @) * P0) * (1,i) = 0. K ) by A3, A6, MATRIX_0:31;
((A @) * P0) @ = (P0 @) * ((A @) @) by Th30
.= (P0 @) * A by MATRIXR2:29 ;
hence ((P0 @) * A) * (i,1) = 0. K by A14, MATRIX_0:def 6; :: thesis: verum
end;
A15: P0 @ is invertible by A4;
((P0 @) * A) * (1,1) = ((P0 @) * ((A @) @)) * (1,1) by MATRIXR2:29
.= (((A @) * P0) @) * (1,1) by Th30
.= 1. K by A5, A8, MATRIX_0:def 6 ;
hence ex P being Matrix of n,K st
( P is invertible & (P * A) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
(P * A) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds
(P * A) * (1,j) = 0. K ) ) by A13, A15, A9; :: thesis: verum