let x be FinSequence of REAL ; for A being Matrix of REAL st len A = len x holds
(LineVec2Mx x) * A = LineVec2Mx (x * A)
let A be Matrix of REAL; ( len A = len x implies (LineVec2Mx x) * A = LineVec2Mx (x * A) )
A1:
len (LineVec2Mx (x * A)) = 1
by MATRIXR1:def 10;
assume A2:
len A = len x
; (LineVec2Mx x) * A = LineVec2Mx (x * A)
then A3:
width (MXR2MXF (LineVec2Mx x)) = len (MXR2MXF A)
by MATRIXR1:def 10;
width (LineVec2Mx (x * A)) = len (x * A)
by MATRIXR1:def 10;
then A4:
width (LineVec2Mx (x * A)) = width A
by A2, MATRIXR1:62;
A5:
len (x * A) = width A
by A2, MATRIXR1:62;
then A6:
width (MXR2MXF (LineVec2Mx (x * A))) = width (MXR2MXF A)
by MATRIXR1:def 10;
A7:
width (LineVec2Mx x) = len x
by MATRIXR1:def 10;
A8:
for i, j being Nat st [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) holds
(MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j))
proof
len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = len (MXR2MXF (LineVec2Mx x))
by A3, MATRIX_3:def 4;
then
len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = 1
by MATRIXR1:def 10;
then A9:
1
in Seg (len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)))
;
let i,
j be
Nat;
( [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) implies (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) )
A10:
width ((LineVec2Mx x) * A) = width A
by A2, A7, MATRIX_3:def 4;
assume A11:
[i,j] in Indices (MXR2MXF (LineVec2Mx (x * A)))
;
(MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j))
then A12:
j in Seg (width A)
by A4, ZFMISC_1:87;
then
j in dom (x * A)
by A5, FINSEQ_1:def 3;
then A13:
(Line (((LineVec2Mx x) * A),1)) . j = (LineVec2Mx (x * A)) * (1,
j)
by MATRIXR1:def 10;
Indices (LineVec2Mx (x * A)) = [:(Seg 1),(Seg (width A)):]
by A1, A4, FINSEQ_1:def 3;
then
i in Seg 1
by A11, ZFMISC_1:87;
then
( 1
<= i &
i <= 1 )
by FINSEQ_1:1;
then A14:
i = 1
by XXREAL_0:1;
width ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = width A
by A3, MATRIX_3:def 4;
then
[1,j] in [:(Seg (len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)))),(Seg (width ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)))):]
by A12, A9, ZFMISC_1:87;
then A15:
[1,j] in Indices ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A))
by FINSEQ_1:def 3;
width (MXR2MXF (LineVec2Mx x)) = len (MXR2MXF A)
by A2, MATRIXR1:def 10;
then
((LineVec2Mx x) * A) * (1,
j)
= (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j))
by A14, A15, MATRIX_3:def 4;
hence
(MXR2MXF (LineVec2Mx (x * A))) * (
i,
j)
= (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j))
by A12, A14, A13, A10, MATRIX_0:def 7;
verum
end;
len (MXR2MXF (LineVec2Mx (x * A))) = len (MXR2MXF (LineVec2Mx x))
by A1, MATRIXR1:def 10;
hence
(LineVec2Mx x) * A = LineVec2Mx (x * A)
by A6, A3, A8, MATRIX_3:def 4; verum