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