let i be Nat; for K being Field
for A, B being Matrix of K st i in dom A & width A = len B holds
(LineVec2Mx (Line (A,i))) * B = LineVec2Mx (Line ((A * B),i))
let K be Field; for A, B being Matrix of K st i in dom A & width A = len B holds
(LineVec2Mx (Line (A,i))) * B = LineVec2Mx (Line ((A * B),i))
let A, B be Matrix of K; ( i in dom A & width A = len B implies (LineVec2Mx (Line (A,i))) * B = LineVec2Mx (Line ((A * B),i)) )
assume that
A1:
i in dom A
and
A2:
width A = len B
; (LineVec2Mx (Line (A,i))) * B = LineVec2Mx (Line ((A * B),i))
A3:
width (A * B) = width B
by A2, MATRIX_3:def 4;
set LAB = LineVec2Mx (Line ((A * B),i));
A4:
( width (LineVec2Mx (Line ((A * B),i))) = len (Line ((A * B),i)) & len (Line ((A * B),i)) = width (A * B) )
by CARD_1:def 7, MATRIX_0:23;
set L = LineVec2Mx (Line (A,i));
A5:
( width (LineVec2Mx (Line (A,i))) = len (Line (A,i)) & len (Line (A,i)) = width A )
by CARD_1:def 7, MATRIX_0:23;
then A6:
width ((LineVec2Mx (Line (A,i))) * B) = width B
by A2, MATRIX_3:def 4;
len (LineVec2Mx (Line (A,i))) = 1
by CARD_1:def 7;
then A7:
len ((LineVec2Mx (Line (A,i))) * B) = 1
by A2, A5, MATRIX_3:def 4;
len (A * B) = len A
by A2, MATRIX_3:def 4;
then A8:
dom A = dom (A * B)
by FINSEQ_3:29;
A9:
now for j, k being Nat st [j,k] in Indices ((LineVec2Mx (Line (A,i))) * B) holds
((LineVec2Mx (Line (A,i))) * B) * (j,k) = (LineVec2Mx (Line ((A * B),i))) * (j,k)let j,
k be
Nat;
( [j,k] in Indices ((LineVec2Mx (Line (A,i))) * B) implies ((LineVec2Mx (Line (A,i))) * B) * (j,k) = (LineVec2Mx (Line ((A * B),i))) * (j,k) )assume A10:
[j,k] in Indices ((LineVec2Mx (Line (A,i))) * B)
;
((LineVec2Mx (Line (A,i))) * B) * (j,k) = (LineVec2Mx (Line ((A * B),i))) * (j,k)A11:
k in Seg (width (A * B))
by A3, A6, A10, ZFMISC_1:87;
then A12:
[i,k] in Indices (A * B)
by A1, A8, ZFMISC_1:87;
Indices ((LineVec2Mx (Line (A,i))) * B) = [:(Seg 1),(Seg (width B)):]
by A7, A6, FINSEQ_1:def 3;
then
j in Seg 1
by A10, ZFMISC_1:87;
then A13:
j = 1
by FINSEQ_1:2, TARSKI:def 1;
hence ((LineVec2Mx (Line (A,i))) * B) * (
j,
k) =
(Line ((LineVec2Mx (Line (A,i))),1)) "*" (Col (B,k))
by A2, A5, A10, MATRIX_3:def 4
.=
(Line (A,i)) "*" (Col (B,k))
by MATRIX15:25
.=
(A * B) * (
i,
k)
by A2, A12, MATRIX_3:def 4
.=
(Line ((A * B),i)) . k
by A11, MATRIX_0:def 7
.=
(Line ((LineVec2Mx (Line ((A * B),i))),j)) . k
by A13, MATRIX15:25
.=
(LineVec2Mx (Line ((A * B),i))) * (
j,
k)
by A4, A11, MATRIX_0:def 7
;
verum end;
len (LineVec2Mx (Line ((A * B),i))) = 1
by CARD_1:def 7;
hence
(LineVec2Mx (Line (A,i))) * B = LineVec2Mx (Line ((A * B),i))
by A4, A3, A7, A6, A9, MATRIX_0:21; verum