let x be FinSequence of REAL ; ( len x > 0 implies ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x ) )
A1:
dom (LineVec2Mx x) = Seg (len (LineVec2Mx x))
by FINSEQ_1:def 3;
A2:
width (LineVec2Mx x) = len x
by Def10;
assume A3:
len x > 0
; ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x )
then A4:
len (ColVec2Mx x) = len x
by Def9;
A5:
len (LineVec2Mx x) = 1
by Def10;
A6:
width (ColVec2Mx x) = 1
by A3, Def9;
A7:
dom (ColVec2Mx x) = Seg (len (ColVec2Mx x))
by FINSEQ_1:def 3;
A8:
for i, j being Nat holds
( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) )
proof
let i,
j be
Nat;
( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) )
(
[i,j] in Indices (ColVec2Mx x) iff (
i in dom (ColVec2Mx x) &
j in Seg (width (ColVec2Mx x)) ) )
by ZFMISC_1:87;
hence
(
[i,j] in Indices (ColVec2Mx x) iff
[j,i] in Indices (LineVec2Mx x) )
by A2, A5, A4, A6, A7, A1, ZFMISC_1:87;
verum
end;
A9:
for i, j being Nat st [j,i] in Indices (LineVec2Mx x) holds
(ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i)
proof
let i,
j be
Nat;
( [j,i] in Indices (LineVec2Mx x) implies (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i) )
assume A10:
[j,i] in Indices (LineVec2Mx x)
;
(ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i)
then
[i,j] in Indices (ColVec2Mx x)
by A8;
then A11:
ex
p being
FinSequence of
REAL st
(
p = (ColVec2Mx x) . i &
(ColVec2Mx x) * (
i,
j)
= p . j )
by MATRIX_0:def 5;
j in Seg 1
by A5, A1, A10, ZFMISC_1:87;
then
( 1
<= j &
j <= 1 )
by FINSEQ_1:1;
then A12:
j = 1
by XXREAL_0:1;
i in Seg (len x)
by A2, A10, ZFMISC_1:87;
then A13:
i in dom x
by FINSEQ_1:def 3;
then
(ColVec2Mx x) . i = <*(x . i)*>
by A3, Def9;
hence (ColVec2Mx x) * (
i,
j) =
x . i
by A12, A11, FINSEQ_1:40
.=
(LineVec2Mx x) * (
j,
i)
by A12, A13, Def10
;
verum
end;
hence
(LineVec2Mx x) @ = ColVec2Mx x
by A2, A4, A8, MATRIX_0:def 6; (ColVec2Mx x) @ = LineVec2Mx x
A14:
for i, j being Nat st [j,i] in Indices (ColVec2Mx x) holds
(LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i)
proof
let i,
j be
Nat;
( [j,i] in Indices (ColVec2Mx x) implies (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) )
assume
[j,i] in Indices (ColVec2Mx x)
;
(LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i)
then
[i,j] in Indices (LineVec2Mx x)
by A8;
hence
(LineVec2Mx x) * (
i,
j)
= (ColVec2Mx x) * (
j,
i)
by A9;
verum
end;
for i, j being Nat holds
( [i,j] in Indices (LineVec2Mx x) iff [j,i] in Indices (ColVec2Mx x) )
by A8;
hence
(ColVec2Mx x) @ = LineVec2Mx x
by A5, A6, A14, MATRIX_0:def 6; verum