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
A1: B * A = 1. K,n and
A2: A * B = 1. K,n by Th19;
(A * B) @ = (B @ ) * (A @ ) by Th30;
then A3: (B @ ) * (A @ ) = 1. K,n by A2, MATRIX_6:10;
(B * A) @ = (A @ ) * (B @ ) by Th30;
then A4: (A @ ) * (B @ ) = 1. K,n by A1, MATRIX_6:10;
B = A ~ by A1, A2, Th18;
hence ( A @ is invertible & (A @ ) ~ = (A ~ ) @ ) by A3, A4, Th18; :: thesis: verum