let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st M is invertible & n > 0 holds
(M @ ) ~ = (M ~ ) @
let K be Field; :: thesis: for M being Matrix of n,K st M is invertible & n > 0 holds
(M @ ) ~ = (M ~ ) @
let M be Matrix of n,K; :: thesis: ( M is invertible & n > 0 implies (M @ ) ~ = (M ~ ) @ )
assume that
A1: M is invertible and
A2: n > 0 ; :: thesis: (M @ ) ~ = (M ~ ) @
set M1 = M @ ;
set M2 = (M ~ ) @ ;
A3: ( width M = n & width (M ~ ) = n ) by MATRIX_1:25;
len M = n by MATRIX_1:25;
then A4: ((M ~ ) * M) @ = (M @ ) * ((M ~ ) @ ) by A2, A3, MATRIX_3:24;
A5: M ~ is_reverse_of M by A1, Def4;
then (M ~ ) * M = 1. K,n by Def2;
then A6: (M @ ) * ((M ~ ) @ ) = 1. K,n by A4, Th10;
len (M ~ ) = n by MATRIX_1:25;
then (M * (M ~ )) @ = ((M ~ ) @ ) * (M @ ) by A2, A3, MATRIX_3:24;
then (M @ ) * ((M ~ ) @ ) = ((M ~ ) @ ) * (M @ ) by A5, A4, Def2;
then A7: M @ is_reverse_of (M ~ ) @ by A6, Def2;
then M @ is invertible by Def3;
hence (M @ ) ~ = (M ~ ) @ by A7, Def4; :: thesis: verum