let r be Real; for i, j, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
(@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))
let i, j, n be Nat; for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
(@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))
let p be Point of (TOP-REAL n); ( 1 <= i & i < j & j <= n implies (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r)) )
assume that
A1:
1 <= i
and
A2:
i < j
and
A3:
j <= n
; (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))
set O = Rotation (i,j,n,r);
set C = Col ((Rotation (i,j,n,r)),j);
set S = Seg n;
1 <= j
by A1, A2, XXREAL_0:2;
then A4:
j in Seg n
by A3;
A5:
len (Rotation (i,j,n,r)) = n
by MATRIX_0:25;
then A6:
dom (Rotation (i,j,n,r)) = Seg n
by FINSEQ_1:def 3;
then A7:
(Col ((Rotation (i,j,n,r)),j)) . j = (Rotation (i,j,n,r)) * (j,j)
by A4, MATRIX_0:def 8;
A8:
i <= n
by A2, A3, XXREAL_0:2;
then A9:
i in Seg n
by A1;
then A10:
(Col ((Rotation (i,j,n,r)),j)) . i = (Rotation (i,j,n,r)) * (i,j)
by A6, MATRIX_0:def 8;
( len p = n & len (Col ((Rotation (i,j,n,r)),j)) = n )
by A5, CARD_1:def 7;
then
len (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = n
by MATRIX_3:6;
then A11:
dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = Seg n
by FINSEQ_1:def 3;
then A12:
i in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j))))
by A1, A8;
A13:
Indices (Rotation (i,j,n,r)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
for k being Nat st k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) & k <> i & k <> j holds
(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real
proof
let k be
Nat;
( k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) & k <> i & k <> j implies (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real )
assume that A14:
k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j))))
and A15:
k <> i
and A16:
k <> j
;
(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real
not
k in {i,j}
by A15, A16, TARSKI:def 2;
then A17:
{k,j} <> {i,j}
by TARSKI:def 2;
reconsider pk =
(@ p) . k as
Element of
F_Real by XREAL_0:def 1;
A18:
[k,j] in Indices (Rotation (i,j,n,r))
by A4, A11, A13, A14, ZFMISC_1:87;
(Col ((Rotation (i,j,n,r)),j)) . k = (Rotation (i,j,n,r)) * (
k,
j)
by A6, A11, A14, MATRIX_0:def 8;
hence (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k =
pk * ((Rotation (i,j,n,r)) * (k,j))
by A14, FVSUM_1:60
.=
pk * (0. F_Real)
by A1, A2, A3, A16, A17, A18, Def3
.=
0. F_Real
;
verum
end;
then A19:
Sum (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = ((mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. i) + ((mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. j)
by A2, A4, A9, A11, MATRIX15:7;
reconsider pii = (@ p) . i, pj = (@ p) . j as Element of F_Real by XREAL_0:def 1;
A20: (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. i =
(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . i
by A9, A11, PARTFUN1:def 6
.=
pii * ((Rotation (i,j,n,r)) * (i,j))
by A10, A12, FVSUM_1:60
.=
(p . i) * (sin r)
by A1, A2, A3, Def3
;
(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. j =
(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . j
by A4, A11, PARTFUN1:def 6
.=
pj * ((Rotation (i,j,n,r)) * (j,j))
by A4, A7, A11, FVSUM_1:60
.=
(p . j) * (cos r)
by A1, A2, A3, Def3
;
hence
(@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))
by A19, A20; verum