let K be Field; for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for M being Matrix of len b1, len b2,K holds AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
let V1, V2 be finite-dimensional VectSp of K; for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for M being Matrix of len b1, len b2,K holds AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
let b1 be OrdBasis of V1; for b2 being OrdBasis of V2
for M being Matrix of len b1, len b2,K holds AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
let b2 be OrdBasis of V2; for M being Matrix of len b1, len b2,K holds AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
let M be Matrix of len b1, len b2,K; AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
set MX = Mx2Tran (M,b1,b2);
set A = AutMt ((Mx2Tran (M,b1,b2)),b1,b2);
set ONE = 1. (K,(len b1));
A1:
len M = len b1
by MATRIX_0:25;
A2:
len (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) = len b1
by MATRIX_0:25;
A3:
len (1. (K,(len b1))) = len b1
by MATRIX_0:24;
now for i being Nat st 1 <= i & i <= len M holds
M . i = (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) . ilet i be
Nat;
( 1 <= i & i <= len M implies M . i = (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) . i )assume A4:
( 1
<= i &
i <= len M )
;
M . i = (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) . iA5:
i in Seg (len b1)
by A1, A4;
A6:
i in dom (1. (K,(len b1)))
by A1, A3, A4, FINSEQ_3:25;
reconsider Ai =
(AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) /. i as
FinSequence of
K by FINSEQ_1:def 11;
A7:
i in dom b1
by A1, A4, FINSEQ_3:25;
then
(AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) /. i = ((Mx2Tran (M,b1,b2)) . (b1 /. i)) |-- b2
by MATRLIN:def 8;
then LineVec2Mx Ai =
(LineVec2Mx ((b1 /. i) |-- b1)) * M
by A1, A4, Th32
.=
(LineVec2Mx (Line ((1. (K,(len b1))),i))) * M
by A7, Th19
.=
LineVec2Mx (Line (((1. (K,(len b1))) * M),i))
by A1, A6, Th35, MATRIX_0:24
.=
LineVec2Mx (Line (M,i))
by A1, MATRIXR2:68
;
then A8:
Ai =
Line (
(LineVec2Mx (Line (M,i))),1)
by MATRIX15:25
.=
Line (
M,
i)
by MATRIX15:25
.=
M . i
by A5, MATRIX_0:52
;
i in dom (AutMt ((Mx2Tran (M,b1,b2)),b1,b2))
by A1, A2, A4, FINSEQ_3:25;
hence
M . i = (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) . i
by A8, PARTFUN1:def 6;
verum end;
hence
AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
by A2, FINSEQ_1:14, MATRIX_0:25; verum