let x be FinSequence of REAL ; :: thesis: for M being Matrix of REAL st len x > 0 holds
( M = ColVec2Mx x iff ( Col M,1 = x & width M = 1 ) )
let M be Matrix of REAL ; :: thesis: ( len x > 0 implies ( M = ColVec2Mx x iff ( Col M,1 = x & width M = 1 ) ) )
assume A1:
len x > 0
; :: thesis: ( M = ColVec2Mx x iff ( Col M,1 = x & width M = 1 ) )
thus
( M = ColVec2Mx x implies ( Col M,1 = x & width M = 1 ) )
:: thesis: ( Col M,1 = x & width M = 1 implies M = ColVec2Mx x )proof
assume A2:
M = ColVec2Mx x
;
:: thesis: ( Col M,1 = x & width M = 1 )
then A3:
(
len M = len x &
width M = 1 )
by A1, Def9;
then A4:
dom M = dom x
by FINSEQ_3:31;
for
j being
Nat st
j in dom M holds
x . j = M * j,1
proof
let j be
Nat;
:: thesis: ( j in dom M implies x . j = M * j,1 )
assume A5:
j in dom M
;
:: thesis: x . j = M * j,1
then reconsider j =
j as
Element of
NAT ;
A6:
M . j = <*(x . j)*>
by A1, A2, A4, A5, Def9;
then reconsider q =
M . j as
FinSequence of
REAL ;
A7:
q . 1
= x . j
by A6, FINSEQ_1:57;
1
in Seg (width M)
by A3, FINSEQ_1:3;
then
[j,1] in Indices M
by A5, ZFMISC_1:106;
hence
x . j = M * j,1
by A7, MATRIX_1:def 6;
:: thesis: verum
end;
hence
(
Col M,1
= x &
width M = 1 )
by A3, MATRIX_1:def 9;
:: thesis: verum
end;
assume A8:
( Col M,1 = x & width M = 1 )
; :: thesis: M = ColVec2Mx x
then A9:
( len x = len M & ( for j being Nat st j in dom M holds
x . j = M * j,1 ) )
by MATRIX_1:def 9;
then A10:
dom x = dom M
by FINSEQ_3:31;
consider s being FinSequence such that
A11:
( s in rng M & len s = 1 )
by A1, A8, A9, MATRIX_1:def 4;
consider n being Nat such that
A12:
for x being set st x in rng M holds
ex s2 being FinSequence st
( s2 = x & len s2 = n )
by MATRIX_1:def 1;
consider s2 being FinSequence such that
A13:
( s2 = s & len s2 = n )
by A11, A12;
for j being Nat st j in dom x holds
M . j = <*(x . j)*>
proof
let j be
Nat;
:: thesis: ( j in dom x implies M . j = <*(x . j)*> )
assume A14:
j in dom x
;
:: thesis: M . j = <*(x . j)*>
then A15:
x . j = M * j,1
by A8, A10, MATRIX_1:def 9;
1
in Seg (width M)
by A8, FINSEQ_1:3;
then
[j,1] in Indices M
by A10, A14, ZFMISC_1:106;
then consider p being
FinSequence of
REAL such that A16:
(
p = M . j &
M * j,1
= p . 1 )
by MATRIX_1:def 6;
M . j in rng M
by A10, A14, FUNCT_1:def 5;
then
ex
s3 being
FinSequence st
(
s3 = M . j &
len s3 = 1 )
by A11, A12, A13;
hence
M . j = <*(x . j)*>
by A15, A16, FINSEQ_1:57;
:: thesis: verum
end;
hence
M = ColVec2Mx x
by A1, A8, A9, Def9; :: thesis: verum