let K be Field; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: (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 :: thesis: 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; :: thesis: ( [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))) ; :: thesis: (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 :: thesis: 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) . j
A19: 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; :: thesis: ( 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)) ; :: thesis: (Col ((AutMt (f,b1,b2)),j)) . k = (((f * b1) /. k) |-- b2) . j
A22: ( 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum