let K be Field; for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1 st len b1 > 0 & f is additive & f is homogeneous holds
(LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2)
let V1, V2 be finite-dimensional VectSp of K; for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1 st len b1 > 0 & f is additive & f is homogeneous holds
(LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2)
let f be Function of V1,V2; for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1 st len b1 > 0 & f is additive & f is homogeneous holds
(LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2)
let b1 be OrdBasis of V1; for b2 being OrdBasis of V2
for v1 being Element of V1 st len b1 > 0 & f is additive & f is homogeneous holds
(LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2)
let b2 be OrdBasis of V2; for v1 being Element of V1 st len b1 > 0 & f is additive & f is homogeneous holds
(LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2)
let v1 be Element of V1; ( len b1 > 0 & f is additive & f is homogeneous implies (LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2) )
assume that
A1:
len b1 > 0
and
A2:
( f is additive & f is homogeneous )
; (LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2)
set A = AutMt (f,b1,b2);
set fb = (f . v1) |-- b2;
set vb = v1 |-- b1;
set L = LineVec2Mx (v1 |-- b1);
set LA = (LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2));
set Lf = LineVec2Mx ((f . v1) |-- b2);
A3:
len (AutMt (f,b1,b2)) = len b1
by MATRLIN:def 8;
len ((f . v1) |-- b2) = len b2
by MATRLIN:def 7;
then A4:
width (LineVec2Mx ((f . v1) |-- b2)) = len b2
by MATRIX_0:23;
A5:
len (v1 |-- b1) = len b1
by MATRLIN:def 7;
then A6:
width (LineVec2Mx (v1 |-- b1)) = len b1
by MATRIX_0:23;
len (LineVec2Mx (v1 |-- b1)) = 1
by MATRIX_0:23;
then A7:
len ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2))) = 1
by A6, A3, MATRIX_3:def 4;
A8:
width (AutMt (f,b1,b2)) = len b2
by A1, MATRLIN:39;
then A9:
width ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2))) = len b2
by A6, A3, MATRIX_3:def 4;
A10:
now for i, j being Nat st [i,j] in Indices ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2))) holds
(LineVec2Mx ((f . v1) |-- b2)) * (i,j) = ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2))) * (i,j)A11:
dom b2 = Seg (len b2)
by FINSEQ_1:def 3;
A12:
dom ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2))) = Seg 1
by A7, FINSEQ_1:def 3;
A13:
len (f * b1) = len b1
by FINSEQ_2:33;
let i,
j be
Nat;
( [i,j] in Indices ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2))) implies (LineVec2Mx ((f . v1) |-- b2)) * (i,j) = ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2))) * (i,j) )assume A14:
[i,j] in Indices ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)))
;
(LineVec2Mx ((f . v1) |-- b2)) * (i,j) = ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2))) * (i,j)A15:
j in Seg (len b2)
by A9, A14, ZFMISC_1:87;
i in dom ((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)))
by A14, ZFMISC_1:87;
then A16:
i = 1
by A12, FINSEQ_1:2, TARSKI:def 1;
A17:
len (Col ((AutMt (f,b1,b2)),j)) = len (AutMt (f,b1,b2))
by CARD_1:def 7;
A18:
now for k being Nat st k in dom (Col ((AutMt (f,b1,b2)),j)) holds
(Col ((AutMt (f,b1,b2)),j)) . k = (((f * b1) /. k) |-- b2) . jA19:
dom (f * b1) = dom b1
by A13, FINSEQ_3:29;
A20:
dom (AutMt (f,b1,b2)) = dom (Col ((AutMt (f,b1,b2)),j))
by A17, FINSEQ_3:29;
let k be
Nat;
( k in dom (Col ((AutMt (f,b1,b2)),j)) implies (Col ((AutMt (f,b1,b2)),j)) . k = (((f * b1) /. k) |-- b2) . j )assume A21:
k in dom (Col ((AutMt (f,b1,b2)),j))
;
(Col ((AutMt (f,b1,b2)),j)) . k = (((f * b1) /. k) |-- b2) . jA22:
(
dom (AutMt (f,b1,b2)) = Seg (len (AutMt (f,b1,b2))) &
(AutMt (f,b1,b2)) . k = (AutMt (f,b1,b2)) /. k )
by A21, A20, FINSEQ_1:def 3, PARTFUN1:def 6;
A23:
dom (AutMt (f,b1,b2)) = dom b1
by A3, FINSEQ_3:29;
then A24:
f . (b1 /. k) =
f . (b1 . k)
by A21, A20, PARTFUN1:def 6
.=
(f * b1) . k
by A21, A20, A23, FUNCT_1:13
.=
(f * b1) /. k
by A21, A20, A23, A19, PARTFUN1:def 6
;
thus (Col ((AutMt (f,b1,b2)),j)) . k =
(AutMt (f,b1,b2)) * (
k,
j)
by A21, A20, MATRIX_0:def 8
.=
(Line ((AutMt (f,b1,b2)),k)) . j
by A8, A15, MATRIX_0:def 7
.=
((AutMt (f,b1,b2)) /. k) . j
by A3, A21, A20, A22, MATRIX_0:52
.=
(((f * b1) /. k) |-- b2) . j
by A21, A20, A23, A24, MATRLIN:def 8
;
verum end; thus (LineVec2Mx ((f . v1) |-- b2)) * (
i,
j) =
(Line ((LineVec2Mx ((f . v1) |-- b2)),i)) . j
by A4, A15, MATRIX_0:def 7
.=
((f . v1) |-- b2) . j
by A16, MATRIX15:25
.=
((f . (Sum (lmlt ((v1 |-- b1),b1)))) |-- b2) . j
by MATRLIN:35
.=
((Sum (lmlt ((v1 |-- b1),(f * b1)))) |-- b2) . j
by A2, A5, MATRLIN:18
.=
(v1 |-- b1) "*" (Col ((AutMt (f,b1,b2)),j))
by A1, A5, A3, A11, A15, A13, A17, A18, Th30
.=
(Line ((LineVec2Mx (v1 |-- b1)),1)) "*" (Col ((AutMt (f,b1,b2)),j))
by MATRIX15:25
.=
((LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2))) * (
i,
j)
by A6, A3, A14, A16, MATRIX_3:def 4
;
verum end;
len (LineVec2Mx ((f . v1) |-- b2)) = 1
by MATRIX_0:23;
hence
(LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2)
by A7, A9, A4, A10, MATRIX_0:21; verum