let n be Element of NAT ; 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; 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; ( 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
;
( 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 Th54;
( 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) )
verumproof
assume
ex
B being
Matrix of
n,
K st
A * B = 1. (
K,
n)
;
ex B2 being Matrix of n,K st B2 * A = 1. (K,n)
then consider B being
Matrix of
n,
K such that A2:
A * B = 1. (
K,
n)
;
A3:
(
width A = n &
len B = n )
by MATRIX_0:24;
(
width B = n &
(A * B) @ = 1. (
K,
n) )
by A2, MATRIX_0:24, MATRIX_6:10;
then
(B @) * (A @) = 1. (
K,
n)
by A1, A3, MATRIX_3:22;
then consider B2 being
Matrix of
n,
K such that A4:
(A @) * B2 = 1. (
K,
n)
by Th54;
A5:
(
width (A @) = n &
len B2 = n )
by MATRIX_0:24;
(
width B2 = n &
((A @) * B2) @ = 1. (
K,
n) )
by A4, MATRIX_0:24, MATRIX_6:10;
then
(B2 @) * ((A @) @) = 1. (
K,
n)
by A1, A5, MATRIX_3:22;
then
(B2 @) * A = 1. (
K,
n)
by MATRIXR2:29;
hence
ex
B2 being
Matrix of
n,
K st
B2 * A = 1. (
K,
n)
;
verum
end; end;