let r be Real; for i, j, k, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j holds
(@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k
let i, j, k, n be Nat; for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j holds
(@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k
let p be Point of (TOP-REAL n); ( 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j implies (@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k )
set S = Seg n;
assume that
A1:
( 1 <= i & i < j & j <= n )
and
A2:
k in Seg n
and
A3:
( k <> i & k <> j )
; (@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k
set O = Rotation (i,j,n,r);
set C = Col ((Rotation (i,j,n,r)),k);
A4:
Indices (Rotation (i,j,n,r)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A5:
[k,k] in Indices (Rotation (i,j,n,r))
by A2, ZFMISC_1:87;
A6:
len (Rotation (i,j,n,r)) = n
by MATRIX_0:25;
then A7:
dom (Rotation (i,j,n,r)) = Seg n
by FINSEQ_1:def 3;
len (Col ((Rotation (i,j,n,r)),k)) = n
by A6, MATRIX_0:def 8;
then A8:
dom (Col ((Rotation (i,j,n,r)),k)) = Seg n
by FINSEQ_1:def 3;
A9:
now for m being Nat st m in dom (Col ((Rotation (i,j,n,r)),k)) & m <> k holds
(Col ((Rotation (i,j,n,r)),k)) . m = 0. F_Reallet m be
Nat;
( m in dom (Col ((Rotation (i,j,n,r)),k)) & m <> k implies (Col ((Rotation (i,j,n,r)),k)) . m = 0. F_Real )assume that A10:
m in dom (Col ((Rotation (i,j,n,r)),k))
and A11:
m <> k
;
(Col ((Rotation (i,j,n,r)),k)) . m = 0. F_RealA12:
[m,k] in Indices (Rotation (i,j,n,r))
by A2, A4, A8, A10, ZFMISC_1:87;
not
k in {i,j}
by A3, TARSKI:def 2;
then A13:
{m,k} <> {i,j}
by TARSKI:def 2;
thus (Col ((Rotation (i,j,n,r)),k)) . m =
(Rotation (i,j,n,r)) * (
m,
k)
by A7, A8, A10, MATRIX_0:def 8
.=
0. F_Real
by A1, A11, A12, A13, Def3
;
verum end;
len p = n
by CARD_1:def 7;
then A14:
dom p = Seg n
by FINSEQ_1:def 3;
(Col ((Rotation (i,j,n,r)),k)) . k =
(Rotation (i,j,n,r)) * (k,k)
by A2, A7, MATRIX_0:def 8
.=
1. F_Real
by A1, A3, A5, Def3
;
hence p . k =
Sum (mlt ((Col ((Rotation (i,j,n,r)),k)),(@ p)))
by A2, A8, A9, A14, MATRIX_3:17
.=
(@ p) "*" (Col ((Rotation (i,j,n,r)),k))
by FVSUM_1:64
;
verum