let p be FinSequence of REAL ; for MR, MR1 being Matrix of REAL st len p = len MR holds
( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j)) ) ) )
let MR, MR1 be Matrix of REAL; ( len p = len MR implies ( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j)) ) ) ) )
set MM = Vec2DiagMx p;
A1:
len (Vec2DiagMx p) = len p
by Th25;
A2:
width (Vec2DiagMx p) = len p
by Th25;
assume A3:
len p = len MR
; ( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j)) ) ) )
then A4:
dom p = dom MR
by FINSEQ_3:29;
hereby ( len MR1 = len p & width MR1 = width MR & ( for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j)) ) implies MR1 = (Vec2DiagMx p) * MR )
assume A5:
MR1 = (Vec2DiagMx p) * MR
;
( len MR1 = len p & width MR1 = width MR & ( for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j)) ) )hence
(
len MR1 = len p &
width MR1 = width MR )
by A3, A1, A2, MATRPROB:39;
for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j))A6:
len MR1 = len (Vec2DiagMx p)
by A3, A2, A5, MATRPROB:39;
then A7:
dom MR1 = dom (Vec2DiagMx p)
by FINSEQ_3:29;
A8:
dom MR1 = dom p
by A1, A6, FINSEQ_3:29;
thus
for
i,
j being
Nat st
[i,j] in Indices MR1 holds
MR1 * (
i,
j)
= (p . i) * (MR * (i,j))
verumproof
let i,
j be
Nat;
( [i,j] in Indices MR1 implies MR1 * (i,j) = (p . i) * (MR * (i,j)) )
assume A9:
[i,j] in Indices MR1
;
MR1 * (i,j) = (p . i) * (MR * (i,j))
i in Seg (len MR1)
by A9, MATRPROB:12;
then A10:
i in dom MR1
by FINSEQ_1:def 3;
then A11:
(Line ((Vec2DiagMx p),i)) . i = p . i
by A7, Th25;
set q =
mlt (
(Line ((Vec2DiagMx p),i)),
(Col (MR,j)));
A12:
len (Line ((Vec2DiagMx p),i)) = width (Vec2DiagMx p)
by MATRIX_0:def 7;
A13:
len (Col (MR,j)) = len MR
by MATRIX_0:def 8;
A14:
Line (
(Vec2DiagMx p),
i)
has_onlyone_value_in i
by A7, A10, Th25;
then A15:
(mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j)))) . i = ((Line ((Vec2DiagMx p),i)) . i) * ((Col (MR,j)) . i)
by A3, A2, A12, A13, Th12;
thus MR1 * (
i,
j) =
(Line ((Vec2DiagMx p),i)) "*" (Col (MR,j))
by A3, A2, A5, A9, MATRPROB:39
.=
Sum (mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j))))
by RVSUM_1:def 16
.=
(p . i) * ((Col (MR,j)) . i)
by A3, A2, A14, A11, A12, A13, A15, Th12, Th13
.=
(p . i) * (MR * (i,j))
by A4, A8, A10, MATRIX_0:def 8
;
verum
end;
end;
assume that
A16:
len MR1 = len p
and
A17:
width MR1 = width MR
and
A18:
for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j))
; MR1 = (Vec2DiagMx p) * MR
A19:
dom MR1 = dom (Vec2DiagMx p)
by A1, A16, FINSEQ_3:29;
A20:
dom MR = dom MR1
by A3, A16, FINSEQ_3:29;
for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (Line ((Vec2DiagMx p),i)) "*" (Col (MR,j))
proof
let i,
j be
Nat;
( [i,j] in Indices MR1 implies MR1 * (i,j) = (Line ((Vec2DiagMx p),i)) "*" (Col (MR,j)) )
assume A21:
[i,j] in Indices MR1
;
MR1 * (i,j) = (Line ((Vec2DiagMx p),i)) "*" (Col (MR,j))
i in Seg (len MR1)
by A21, MATRPROB:12;
then A22:
i in dom MR1
by FINSEQ_1:def 3;
then A23:
(Line ((Vec2DiagMx p),i)) . i = p . i
by A19, Th25;
set q =
mlt (
(Line ((Vec2DiagMx p),i)),
(Col (MR,j)));
A24:
len (Line ((Vec2DiagMx p),i)) = width (Vec2DiagMx p)
by MATRIX_0:def 7;
A25:
len (Col (MR,j)) = len MR
by MATRIX_0:def 8;
A26:
Line (
(Vec2DiagMx p),
i)
has_onlyone_value_in i
by A19, A22, Th25;
then A27:
(mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j)))) . i = ((Line ((Vec2DiagMx p),i)) . i) * ((Col (MR,j)) . i)
by A3, A2, A24, A25, Th12;
thus MR1 * (
i,
j) =
(p . i) * (MR * (i,j))
by A18, A21
.=
(p . i) * ((Col (MR,j)) . i)
by A20, A22, MATRIX_0:def 8
.=
Sum (mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j))))
by A3, A2, A26, A23, A24, A25, A27, Th12, Th13
.=
(Line ((Vec2DiagMx p),i)) "*" (Col (MR,j))
by RVSUM_1:def 16
;
verum
end;
hence
MR1 = (Vec2DiagMx p) * MR
by A3, A1, A2, A16, A17, MATRPROB:39; verum