let n be Element of NAT ; 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; 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; ( 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
; 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 ;
( 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
;
((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;
verum
end;
A13:
for i being Element of NAT st 1 < i & i <= n holds
((P0 @) * A) * (i,1) = 0. K
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; verum