let i, n be Nat; for p being Point of (TOP-REAL n) st i in Seg n & n >= 2 holds
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) )
let p be Point of (TOP-REAL n); ( i in Seg n & n >= 2 implies ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) ) )
set TR = TOP-REAL n;
assume that
A1:
i in Seg n
and
A2:
n >= 2
; ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) )
A3:
{i} c= Seg n
by A1, ZFMISC_1:31;
A4:
1 <= i
by A1, FINSEQ_1:1;
( card (Seg n) = n & card {i} = 1 )
by CARD_2:42, FINSEQ_1:57;
then
{i} <> Seg n
by A2;
then
{i} c< Seg n
by A3, XBOOLE_0:def 8;
then consider j being object such that
A5:
j in Seg n
and
A6:
not j in {i}
by XBOOLE_0:6;
reconsider j = j as Nat by A5;
A7:
j <> i
by A6, TARSKI:def 1;
A8:
1 <= j
by A5, FINSEQ_1:1;
set p0 = p +* (i,(- (p . i)));
A9:
len (p +* (i,(- (p . i)))) = len p
by FUNCT_7:97;
A10:
len p = n
by CARD_1:def 7;
then A11:
dom p = Seg n
by FINSEQ_1:def 3;
A12:
i <= n
by A1, FINSEQ_1:1;
( (p . i) * (p . i) >= 0 & (p . j) * (p . j) >= 0 )
by XREAL_1:63;
then A13:
( 0 ^2 = 0* 0 & 0 <= ((p . i) ^2) + ((p . j) ^2) )
;
A14:
j <= n
by A5, FINSEQ_1:1;
per cases
( i < j or j < i )
by A7, XXREAL_0:1;
suppose A15:
i < j
;
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) )then consider r being
Real such that A16:
((Mx2Tran (Rotation (i,j,n,r))) . p) . i = 0
by A4, A13, A14, Th24;
set s =
sin r;
set c =
cos r;
A17:
0 = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))
by A4, A14, A15, A16, Th21;
reconsider M =
Mx2Tran (Rotation (i,j,n,(r + r))) as
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) by A4, A14, A15, Th28;
set Mp =
M . p;
A18:
(
cos (r + r) = ((cos r) * (cos r)) - ((sin r) * (sin r)) &
sin (r + r) = ((sin r) * (cos r)) + ((sin r) * (cos r)) )
by SIN_COS:75;
A19:
M is
{i,j} -support-yielding
by A4, A14, A15, Th26;
A20:
for
k being
Nat st 1
<= k &
k <= n holds
(p +* (i,(- (p . i)))) . k = (M . p) . k
proof
let k be
Nat;
( 1 <= k & k <= n implies (p +* (i,(- (p . i)))) . k = (M . p) . k )
assume
( 1
<= k &
k <= n )
;
(p +* (i,(- (p . i)))) . k = (M . p) . k
then A21:
k in Seg n
;
end; take
M
;
( M is base_rotation & M . p = p +* (i,(- (p . i))) )
len (M . p) = n
by CARD_1:def 7;
hence
(
M is
base_rotation &
M . p = p +* (
i,
(- (p . i))) )
by A9, A10, A20;
verum end; suppose A26:
j < i
;
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) )then consider r being
Real such that A27:
((Mx2Tran (Rotation (j,i,n,r))) . p) . i = 0
by A8, A12, A13, Th25;
set s =
sin r;
set c =
cos r;
A28:
0 = ((p . j) * (sin r)) + ((p . i) * (cos r))
by A8, A12, A26, A27, Th22;
reconsider M =
Mx2Tran (Rotation (j,i,n,(r + r))) as
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) by A8, A12, A26, Th28;
set Mp =
M . p;
A29:
(
cos (r + r) = ((cos r) * (cos r)) - ((sin r) * (sin r)) &
sin (r + r) = ((sin r) * (cos r)) + ((sin r) * (cos r)) )
by SIN_COS:75;
A30:
M is
{i,j} -support-yielding
by A8, A12, A26, Th26;
A31:
for
k being
Nat st 1
<= k &
k <= n holds
(p +* (i,(- (p . i)))) . k = (M . p) . k
proof
let k be
Nat;
( 1 <= k & k <= n implies (p +* (i,(- (p . i)))) . k = (M . p) . k )
assume
( 1
<= k &
k <= n )
;
(p +* (i,(- (p . i)))) . k = (M . p) . k
then A32:
k in Seg n
;
end; take
M
;
( M is base_rotation & M . p = p +* (i,(- (p . i))) )
len (M . p) = n
by CARD_1:def 7;
hence
(
M is
base_rotation &
M . p = p +* (
i,
(- (p . i))) )
by A9, A10, A31;
verum end;