let x be FinSequence of REAL ; 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; ( len x > 0 implies ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) ) )
consider n being Nat such that
A1:
for x being object st x in rng M holds
ex s2 being FinSequence st
( s2 = x & len s2 = n )
by MATRIX_0:def 1;
assume A2:
len x > 0
; ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )
thus
( M = ColVec2Mx x implies ( Col (M,1) = x & width M = 1 ) )
( Col (M,1) = x & width M = 1 implies M = ColVec2Mx x )proof
assume A3:
M = ColVec2Mx x
;
( Col (M,1) = x & width M = 1 )
then A4:
width M = 1
by A2, Def9;
A5:
len M = len x
by A2, A3, Def9;
then A6:
dom M = dom x
by FINSEQ_3:29;
for
j being
Nat st
j in dom M holds
x . j = M * (
j,1)
proof
let j be
Nat;
( j in dom M implies x . j = M * (j,1) )
reconsider xj =
x . j as
Element of
REAL by XREAL_0:def 1;
assume A7:
j in dom M
;
x . j = M * (j,1)
then reconsider j =
j as
Element of
NAT ;
A8:
M . j = <*xj*>
by A2, A3, A6, A7, Def9;
then reconsider q =
M . j as
FinSequence of
REAL ;
A9:
q . 1
= xj
by A8, FINSEQ_1:40;
1
in Seg (width M)
by A4, FINSEQ_1:1;
then
[j,1] in Indices M
by A7, ZFMISC_1:87;
hence
x . j = M * (
j,1)
by A9, MATRIX_0:def 5;
verum
end;
hence
(
Col (
M,1)
= x &
width M = 1 )
by A2, A3, A5, Def9, MATRIX_0:def 8;
verum
end;
assume that
A10:
Col (M,1) = x
and
A11:
width M = 1
; M = ColVec2Mx x
A12:
len x = len M
by A10, MATRIX_0:def 8;
then consider s being FinSequence such that
A13:
s in rng M
and
A14:
len s = 1
by A2, A11, MATRIX_0:def 3;
A15:
dom x = dom M
by A12, FINSEQ_3:29;
A16:
ex s2 being FinSequence st
( s2 = s & len s2 = n )
by A13, A1;
for j being Nat st j in dom x holds
M . j = <*(x . j)*>
proof
let j be
Nat;
( j in dom x implies M . j = <*(x . j)*> )
assume A17:
j in dom x
;
M . j = <*(x . j)*>
then
M . j in rng M
by A15, FUNCT_1:def 3;
then A18:
ex
s3 being
FinSequence st
(
s3 = M . j &
len s3 = 1 )
by A14, A1, A16;
1
in Seg (width M)
by A11, FINSEQ_1:1;
then
[j,1] in Indices M
by A15, A17, ZFMISC_1:87;
then A19:
ex
p being
FinSequence of
REAL st
(
p = M . j &
M * (
j,1)
= p . 1 )
by MATRIX_0:def 5;
x . j = M * (
j,1)
by A10, A15, A17, MATRIX_0:def 8;
hence
M . j = <*(x . j)*>
by A19, A18, FINSEQ_1:40;
verum
end;
hence
M = ColVec2Mx x
by A2, A11, A12, Def9; verum