let n be Nat; for x being FinSequence of REAL st len x = n & n > 0 holds
(1_Rmatrix n) * x = x
let x be FinSequence of REAL ; ( len x = n & n > 0 implies (1_Rmatrix n) * x = x )
assume that
A1:
len x = n
and
A2:
n > 0
; (1_Rmatrix n) * x = x
A3:
len (ColVec2Mx x) = len x
by A1, A2, MATRIXR1:def 9;
A4:
len (Col ((ColVec2Mx x),1)) = len (ColVec2Mx x)
by MATRIX_0:def 8;
A5:
for k being Nat st 1 <= k & k <= len (Col ((ColVec2Mx x),1)) holds
(Col ((ColVec2Mx x),1)) . k = x . k
proof
let k be
Nat;
( 1 <= k & k <= len (Col ((ColVec2Mx x),1)) implies (Col ((ColVec2Mx x),1)) . k = x . k )
assume A6:
( 1
<= k &
k <= len (Col ((ColVec2Mx x),1)) )
;
(Col ((ColVec2Mx x),1)) . k = x . k
A7:
k in Seg (len (ColVec2Mx x))
by A4, A6;
then A8:
k in dom (ColVec2Mx x)
by FINSEQ_1:def 3;
then A9:
(Col ((ColVec2Mx x),1)) . k = (ColVec2Mx x) * (
k,1)
by MATRIX_0:def 8;
( 1
in Seg 1 &
Indices (ColVec2Mx x) = [:(dom (ColVec2Mx x)),(Seg 1):] )
by A1, A2, MATRIXR1:def 9;
then
[k,1] in Indices (ColVec2Mx x)
by A8, ZFMISC_1:87;
then consider p being
FinSequence of
REAL such that A10:
p = (ColVec2Mx x) . k
and A11:
(ColVec2Mx x) * (
k,1)
= p . 1
by MATRIX_0:def 5;
k in dom x
by A3, A7, FINSEQ_1:def 3;
then
p = <*(x . k)*>
by A1, A2, A10, MATRIXR1:def 9;
hence
(Col ((ColVec2Mx x),1)) . k = x . k
by A9, A11, FINSEQ_1:40;
verum
end;
(1_Rmatrix n) * x =
Col ((MXF2MXR (MXR2MXF (ColVec2Mx x))),1)
by A1, A3, Th68
.=
x
by A3, A4, A5
;
hence
(1_Rmatrix n) * x = x
; verum