let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1, b19 being OrdBasis of V1 holds
( AutEqMt ((id V1),b1,b19) is invertible & AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ )
let V1 be finite-dimensional VectSp of K; :: thesis: for b1, b19 being OrdBasis of V1 holds
( AutEqMt ((id V1),b1,b19) is invertible & AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ )
let b1, b19 be OrdBasis of V1; :: thesis: ( AutEqMt ((id V1),b1,b19) is invertible & AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ )
set A = AutEqMt ((id V1),b1,b19);
A1: 1_ K <> 0. K ;
A2: len b1 = dim V1 by Th21
.= len b19 by Th21 ;
then reconsider A9 = AutEqMt ((id V1),b19,b1) as Matrix of len b1, len b1,K ;
A3: ( AutEqMt ((id V1),b1,b19) = AutMt ((id V1),b1,b19) & A9 = AutMt ((id V1),b19,b1) ) by A2, Def2;
per cases ( len b1 = 0 or (len b1) + 0 > 0 ) ;
suppose len b1 = 0 ; :: thesis: ( AutEqMt ((id V1),b1,b19) is invertible & AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ )
then ( Det (AutEqMt ((id V1),b1,b19)) = 1_ K & A9 = (AutEqMt ((id V1),b1,b19)) ~ ) by MATRIXR2:41, MATRIX_0:45;
hence ( AutEqMt ((id V1),b1,b19) is invertible & AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ ) by A1, LAPLACE:34; :: thesis: verum
end;
suppose A4: (len b1) + 0 > 0 ; :: thesis: ( AutEqMt ((id V1),b1,b19) is invertible & AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ )
dom (id V1) = the carrier of V1 ;
then A5: (id V1) * (id V1) = id V1 by RELAT_1:52;
len b1 = dim V1 by Th21;
then len b1 = len b19 by Th21;
then A6: (AutEqMt ((id V1),b1,b19)) * A9 = AutMt (((id V1) * (id V1)),b1,b1) by A3, A4, MATRLIN:41
.= 1. (K,(len b1)) by A5, Th28 ;
len b1 >= 1 by A4, NAT_1:19;
then 1_ K = Det ((AutEqMt ((id V1),b1,b19)) * A9) by A6, MATRIX_7:16
.= (Det (AutEqMt ((id V1),b1,b19))) * (Det A9) by A4, MATRIX11:62 ;
then Det (AutEqMt ((id V1),b1,b19)) <> 0. K ;
then A7: AutEqMt ((id V1),b1,b19) is invertible by LAPLACE:34;
then (AutEqMt ((id V1),b1,b19)) ~ is_reverse_of AutEqMt ((id V1),b1,b19) by MATRIX_6:def 4;
then (AutEqMt ((id V1),b1,b19)) * ((AutEqMt ((id V1),b1,b19)) ~) = 1. (K,(len b1)) by MATRIX_6:def 2;
hence ( AutEqMt ((id V1),b1,b19) is invertible & AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ ) by A6, A7, MATRIX_8:19; :: thesis: verum
end;
end;