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:24;
len M = n by MATRIX_1:24;
then A4: ((M ~) * M) @ = (M @) * ((M ~) @) by A2, A3, MATRIX_3:22;
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:24;
then (M * (M ~)) @ = ((M ~) @) * (M @) by A2, A3, MATRIX_3:22;
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