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 being Nat st i in dom M holds
Line (M,i) = (p . i) * q ) ) )
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 being Nat st i in dom M holds
Line (M,i) = (p . i) * q ) ) )
let M be Matrix of REAL; ( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i being Nat st i in dom M holds
Line (M,i) = (p . i) * q ) ) )
set M1 = ColVec2Mx p;
set M2 = LineVec2Mx q;
hereby ( len M = len p & width M = len q & ( for i being Nat st i in dom M holds
Line (M,i) = (p . i) * q ) implies M = (ColVec2Mx p) * (LineVec2Mx q) )
assume A1:
M = (ColVec2Mx p) * (LineVec2Mx q)
;
( len M = len p & width M = len q & ( for i being Nat st i in dom M holds
Line (M,i) = (p . i) * q ) )hence
(
len M = len p &
width M = len q )
by Th21;
for i being Nat st i in dom M holds
Line (M,i) = (p . i) * qthus
for
i being
Nat st
i in dom M holds
Line (
M,
i)
= (p . i) * q
verumproof
let i be
Nat;
( i in dom M implies Line (M,i) = (p . i) * q )
assume
i in dom M
;
Line (M,i) = (p . i) * q
then A2:
i in Seg (len M)
by FINSEQ_1:def 3;
A3:
for
j being
Nat st
j in dom (Line (M,i)) holds
(Line (M,i)) . j = ((p . i) * q) . j
proof
let j be
Nat;
( j in dom (Line (M,i)) implies (Line (M,i)) . j = ((p . i) * q) . j )
assume
j in dom (Line (M,i))
;
(Line (M,i)) . j = ((p . i) * q) . j
then
j in Seg (len (Line (M,i)))
by FINSEQ_1:def 3;
then A4:
j in Seg (width M)
by MATRIX_0:def 7;
then A5:
[i,j] in Indices M
by A2, MATRPROB:12;
thus (Line (M,i)) . j =
M * (
i,
j)
by A4, MATRIX_0:def 7
.=
(p . i) * (q . j)
by A1, A5, Th21
.=
((p . i) * q) . j
by RVSUM_1:44
;
verum
end;
dom (Line (M,i)) =
Seg (len (Line (M,i)))
by FINSEQ_1:def 3
.=
Seg (width M)
by MATRIX_0:def 7
.=
Seg (len q)
by A1, Th21
.=
dom q
by FINSEQ_1:def 3
.=
dom ((p . i) * q)
by VALUED_1:def 5
;
hence
Line (
M,
i)
= (p . i) * q
by A3, FINSEQ_1:13;
verum
end;
end;
assume that
A6:
len M = len p
and
A7:
width M = len q
and
A8:
for i being Nat st i in dom M holds
Line (M,i) = (p . i) * q
; M = (ColVec2Mx p) * (LineVec2Mx q)
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j)
proof
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 dom M
by A9, MATRPROB:13;
j in Seg (width M)
by A9, MATRPROB:12;
hence M * (
i,
j) =
(Line (M,i)) . j
by MATRIX_0:def 7
.=
((p . i) * q) . j
by A8, A10
.=
(p . i) * (q . j)
by RVSUM_1:44
;
verum
end;
hence
M = (ColVec2Mx p) * (LineVec2Mx q)
by A6, A7, Th21; verum