let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K holds
( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n )
let K be Field; :: thesis: for A being Matrix of n,K holds
( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n )
let A be Matrix of n,K; :: thesis: ( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n )
per cases
( n > 0 or n = 0 )
;
suppose A1:
n > 0
;
:: thesis: ( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n )thus
( ex
B being
Matrix of
n,
K st
B * A = 1. K,
n implies ex
B2 being
Matrix of
n,
K st
A * B2 = 1. K,
n )
by AA4500;
:: thesis: ( ex B2 being Matrix of n,K st A * B2 = 1. K,n implies ex B1 being Matrix of n,K st B1 * A = 1. K,n )thus
( ex
B being
Matrix of
n,
K st
A * B = 1. K,
n implies ex
B2 being
Matrix of
n,
K st
B2 * A = 1. K,
n )
:: thesis: verumproof
assume
ex
B being
Matrix of
n,
K st
A * B = 1. K,
n
;
:: thesis: ex B2 being Matrix of n,K st B2 * A = 1. K,n
then consider B being
Matrix of
n,
K such that B2:
A * B = 1. K,
n
;
B12:
(
len A = n &
width A = n )
by MATRIX_1:25;
B13:
(
len B = n &
width B = n )
by MATRIX_1:25;
(A * B) @ = 1. K,
n
by B2, MATRIX_6:10;
then
(B @ ) * (A @ ) = 1. K,
n
by A1, B12, B13, MATRIX_3:24;
then consider B2 being
Matrix of
n,
K such that B3:
(A @ ) * B2 = 1. K,
n
by AA4500;
B12:
(
len (A @ ) = n &
width (A @ ) = n )
by MATRIX_1:25;
B13:
(
len B2 = n &
width B2 = n )
by MATRIX_1:25;
((A @ ) * B2) @ = 1. K,
n
by B3, MATRIX_6:10;
then
(B2 @ ) * ((A @ ) @ ) = 1. K,
n
by A1, B12, B13, MATRIX_3:24;
then
(B2 @ ) * A = 1. K,
n
by MATRIXR2:29;
hence
ex
B2 being
Matrix of
n,
K st
B2 * A = 1. K,
n
;
:: thesis: verum
end; end;