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