let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K st A is invertible holds
( A @ is invertible & (A @ ) ~ = (A ~ ) @ )
let K be Field; :: thesis: for A being Matrix of n,K st A is invertible holds
( A @ is invertible & (A @ ) ~ = (A ~ ) @ )
let A be Matrix of n,K; :: thesis: ( A is invertible implies ( A @ is invertible & (A @ ) ~ = (A ~ ) @ ) )
assume A is invertible ; :: thesis: ( A @ is invertible & (A @ ) ~ = (A ~ ) @ )
then consider B being Matrix of n,K such that
A2: ( B * A = 1. K,n & A * B = 1. K,n ) by AA4145;
(A * B) @ = (B @ ) * (A @ ) by AA44;
then A3: (B @ ) * (A @ ) = 1. K,n by A2, MATRIX_6:10;
(B * A) @ = (A @ ) * (B @ ) by AA44;
then A4: (A @ ) * (B @ ) = 1. K,n by A2, MATRIX_6:10;
B = A ~ by AA4140, A2;
hence ( A @ is invertible & (A @ ) ~ = (A ~ ) @ ) by AA4140, A3, A4; :: thesis: verum