let p be non empty FinSequence of REAL ; for q being FinSequence of REAL
for M being Matrix of REAL holds
( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j) ) ) )
let q be FinSequence of REAL ; for M being Matrix of REAL holds
( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j) ) ) )
let M be Matrix of REAL; ( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j) ) ) )
set M1 = ColVec2Mx p;
set M2 = LineVec2Mx q;
A1:
len (ColVec2Mx p) = len p
by MATRIXR1:def 9;
A2:
len (LineVec2Mx q) = 1
by MATRIXR1:def 10;
A3:
len p > 0
;
then A4:
width (ColVec2Mx p) = 1
by MATRIXR1:def 9;
A5:
width (LineVec2Mx q) = len q
by MATRIXR1:def 10;
hereby ( len M = len p & width M = len q & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j) ) implies M = (ColVec2Mx p) * (LineVec2Mx q) )
assume A6:
M = (ColVec2Mx p) * (LineVec2Mx q)
;
( len M = len p & width M = len q & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j) ) )then A7:
len M = len (ColVec2Mx p)
by A4, A2, MATRPROB:39;
thus
(
len M = len p &
width M = len q )
by A1, A4, A2, A5, A6, MATRPROB:39;
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j)A8:
width M = width (LineVec2Mx q)
by A4, A2, A6, MATRPROB:39;
thus
for
i,
j being
Nat st
[i,j] in Indices M holds
M * (
i,
j)
= (p . i) * (q . j)
verumproof
let i,
j be
Nat;
( [i,j] in Indices M implies M * (i,j) = (p . i) * (q . j) )
assume A9:
[i,j] in Indices M
;
M * (i,j) = (p . i) * (q . j)
A10:
i in Seg (len M)
by A9, MATRPROB:12;
then A11:
i in dom p
by A1, A7, FINSEQ_1:def 3;
j in Seg (width M)
by A9, MATRPROB:12;
then A12:
j in dom q
by A5, A8, FINSEQ_1:def 3;
i in dom (ColVec2Mx p)
by A7, A10, FINSEQ_1:def 3;
then A13:
Line (
(ColVec2Mx p),
i) =
(ColVec2Mx p) . i
by MATRIX_0:60
.=
<*(p . i)*>
by A3, A11, MATRIXR1:def 9
;
thus M * (
i,
j) =
(Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j))
by A4, A2, A6, A9, MATRPROB:39
.=
<*(p . i)*> "*" <*(q . j)*>
by A12, A13, Th20
.=
Sum (mlt (<*(p . i)*>,<*(q . j)*>))
by RVSUM_1:def 16
.=
Sum <*((p . i) * (q . j))*>
by RVSUM_1:62
.=
(p . i) * (q . j)
by RVSUM_1:73
;
verum
end;
end;
assume that
A14:
len M = len p
and
A15:
width M = len q
and
A16:
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j)
; M = (ColVec2Mx p) * (LineVec2Mx q)
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j))
proof
let i,
j be
Nat;
( [i,j] in Indices M implies M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j)) )
assume A17:
[i,j] in Indices M
;
M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j))
j in Seg (width M)
by A17, MATRPROB:12;
then A18:
j in dom q
by A15, FINSEQ_1:def 3;
A19:
i in Seg (len M)
by A17, MATRPROB:12;
then A20:
i in dom (ColVec2Mx p)
by A1, A14, FINSEQ_1:def 3;
i in dom p
by A14, A19, FINSEQ_1:def 3;
then A21:
<*(p . i)*> =
(ColVec2Mx p) . i
by A3, MATRIXR1:def 9
.=
Line (
(ColVec2Mx p),
i)
by A20, MATRIX_0:60
;
thus M * (
i,
j) =
(p . i) * (q . j)
by A16, A17
.=
Sum <*((p . i) * (q . j))*>
by RVSUM_1:73
.=
Sum (mlt (<*(p . i)*>,<*(q . j)*>))
by RVSUM_1:62
.=
<*(p . i)*> "*" <*(q . j)*>
by RVSUM_1:def 16
.=
(Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j))
by A18, A21, Th20
;
verum
end;
hence
M = (ColVec2Mx p) * (LineVec2Mx q)
by A1, A4, A2, A5, A14, A15, MATRPROB:39; verum