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 A1:
( n > 0 & 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 @ ;
X:
0 + 1 <= n
by A1, NAT_1:13;
[1,1] in Indices A
by X, MATRIX_1:38;
then A5:
(A @ ) * 1,1 = A * 1,1
by MATRIX_1:def 7;
consider P0 being Matrix of n,K such that
A6:
( P0 is invertible & ((A @ ) * P0) * 1,1 = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds
((A @ ) * P0) * 1,i = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & (A @ ) * j,1 = 0. K holds
((A @ ) * P0) * j,1 = 0. K ) )
by AA3020, A5, A1;
A7:
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 B0:
( 1
< i &
i <= n )
;
:: thesis: ((P0 @ ) * A) * i,1 = 0. K
B1:
[1,i] in Indices ((A @ ) * P0)
by B0, X, MATRIX_1:38;
B2:
((A @ ) * P0) * 1,
i = 0. K
by A6, B0;
((A @ ) * P0) @ =
(P0 @ ) * ((A @ ) @ )
by AA44
.=
(P0 @ ) * A
by MATRIXR2:29
;
hence
((P0 @ ) * A) * i,1
= 0. K
by B1, B2, MATRIX_1:def 7;
:: thesis: verum
end;
A8:
P0 @ is invertible
by BB400, A6;
A12:
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 B1:
( 1
< j &
j <= n &
A * 1,
j = 0. K )
;
:: thesis: ((P0 @ ) * A) * 1,j = 0. K
B1b:
[j,1] in Indices ((A @ ) * P0)
by B1, X, MATRIX_1:38;
[1,j] in Indices A
by B1, X, MATRIX_1:38;
then
(A @ ) * j,1
= A * 1,
j
by MATRIX_1:def 7;
then
((A @ ) * P0) * j,1
= 0. K
by A6, B1;
then
(((A @ ) * P0) @ ) * 1,
j = 0. K
by B1b, MATRIX_1:def 7;
then
((P0 @ ) * ((A @ ) @ )) * 1,
j = 0. K
by AA44;
hence
((P0 @ ) * A) * 1,
j = 0. K
by MATRIXR2:29;
:: thesis: verum
end;
A43:
[1,1] in Indices ((A @ ) * P0)
by X, MATRIX_1:38;
((P0 @ ) * A) * 1,1 =
((P0 @ ) * ((A @ ) @ )) * 1,1
by MATRIXR2:29
.=
(((A @ ) * P0) @ ) * 1,1
by AA44
.=
1. K
by A6, A43, MATRIX_1:def 7
;
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 A8, A7, A12; :: thesis: verum