let n be Nat; for p, q being Point of (TOP-REAL n) st n <> 1 & |.p.| = |.q.| holds
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q )
let p, q be Point of (TOP-REAL n); ( n <> 1 & |.p.| = |.q.| implies ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q ) )
set TR = TOP-REAL n;
assume A1:
n <> 1
; ( not |.p.| = |.q.| or ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q ) )
assume A2:
|.p.| = |.q.|
; ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q )
per cases
( p = q or p <> q )
;
suppose A4:
p <> q
;
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q )A5:
n <> 0
then A7:
n >= 1
by NAT_1:14;
defpred S1[
Nat]
means ( $1
+ 1
<= n implies ex
f being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) ex
X being
set st
(
card X = $1 &
X c= Seg n & ( for
k being
Nat st
k in X holds
(f . p) . k = q . k ) ) );
A8:
Sum (sqr q) >= 0
by RVSUM_1:86;
A9:
card (Seg n) = n
by FINSEQ_1:57;
A10:
for
m being
Nat st
S1[
m] holds
S1[
m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A11:
S1[
m]
;
S1[m + 1]
set m1 =
m + 1;
assume A12:
(m + 1) + 1
<= n
;
ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) ex X being set st
( card X = m + 1 & X c= Seg n & ( for k being Nat st k in X holds
(f . p) . k = q . k ) )
then consider f being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n),
Xm being
set such that A13:
card Xm = m
and A14:
Xm c= Seg n
and A15:
for
k being
Nat st
k in Xm holds
(f . p) . k = q . k
by A11, NAT_1:13;
set fp =
f . p;
set sfp =
sqr (f . p);
set sq =
sqr q;
A16:
m + 1
< n
by A12, NAT_1:13;
per cases
( ex k being Nat st
( k in (Seg n) \ Xm & (sqr (f . p)) . k >= (sqr q) . k ) or for k being Nat st k in (Seg n) \ Xm holds
(sqr (f . p)) . k < (sqr q) . k )
;
suppose
ex
k being
Nat st
(
k in (Seg n) \ Xm &
(sqr (f . p)) . k >= (sqr q) . k )
;
ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) ex X being set st
( card X = m + 1 & X c= Seg n & ( for k being Nat st k in X holds
(f . p) . k = q . k ) )then consider k being
Nat such that A17:
k in (Seg n) \ Xm
and A18:
(sqr (f . p)) . k >= (sqr q) . k
;
A19:
k in Seg n
by A17, XBOOLE_0:def 5;
then A20:
1
<= k
by FINSEQ_1:1;
set Xmk =
Xm \/ {k};
A21:
(
(sqr (f . p)) . k = ((f . p) . k) ^2 &
(sqr q) . k = (q . k) ^2 )
by VALUED_1:11;
A22:
{k} c= Seg n
by A19, ZFMISC_1:31;
then A23:
Xm \/ {k} c= Seg n
by A14, XBOOLE_1:8;
A24:
not
k in Xm
by A17, XBOOLE_0:def 5;
then
card (Xm \/ {k}) = m + 1
by A13, A14, CARD_2:41;
then
Xm \/ {k} c< Seg n
by A9, A16, A23, XBOOLE_0:def 8;
then consider z being
object such that A25:
z in Seg n
and A26:
not
z in Xm \/ {k}
by XBOOLE_0:6;
reconsider z =
z as
Nat by A25;
A27:
1
<= z
by A25, FINSEQ_1:1;
((f . p) . z) ^2 >= 0
by XREAL_1:63;
then A28:
0 + ((q . k) ^2) <= (((f . p) . z) ^2) + (((f . p) . k) ^2)
by A18, A21, XREAL_1:7;
A29:
z <= n
by A25, FINSEQ_1:1;
A30:
k <= n
by A19, FINSEQ_1:1;
not
z in {k}
by A26, XBOOLE_0:def 3;
then A31:
z <> k
by TARSKI:def 1;
now ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k )per cases
( z < k or z > k )
by A31, XXREAL_0:1;
suppose A32:
z < k
;
ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k )then consider r being
Real such that A33:
((Mx2Tran (Rotation (z,k,n,r))) . (f . p)) . k = q . k
by A27, A28, A30, Th25;
(
Mx2Tran (Rotation (z,k,n,r)) is
{k,z} -support-yielding &
Mx2Tran (Rotation (z,k,n,r)) is
base_rotation )
by A27, A30, A32, Th28, Th26;
hence
ex
g being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) st
(
g is
{k,z} -support-yielding &
(g . (f . p)) . k = q . k )
by A33;
verum end; suppose A34:
z > k
;
ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k )then consider r being
Real such that A35:
((Mx2Tran (Rotation (k,z,n,r))) . (f . p)) . k = q . k
by A20, A28, A29, Th24;
(
Mx2Tran (Rotation (k,z,n,r)) is
{z,k} -support-yielding &
Mx2Tran (Rotation (k,z,n,r)) is
base_rotation )
by A20, A29, A34, Th28, Th26;
hence
ex
g being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) st
(
g is
{k,z} -support-yielding &
(g . (f . p)) . k = q . k )
by A35;
verum end; end; end; then consider g being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) such that A36:
g is
{k,z} -support-yielding
and A37:
(g . (f . p)) . k = q . k
;
take gf =
g * f;
ex X being set st
( card X = m + 1 & X c= Seg n & ( for k being Nat st k in X holds
(gf . p) . k = q . k ) )take
Xm \/ {k}
;
( card (Xm \/ {k}) = m + 1 & Xm \/ {k} c= Seg n & ( for k being Nat st k in Xm \/ {k} holds
(gf . p) . k = q . k ) )thus
(
card (Xm \/ {k}) = m + 1 &
Xm \/ {k} c= Seg n )
by A13, A14, A22, A24, CARD_2:41, XBOOLE_1:8;
for k being Nat st k in Xm \/ {k} holds
(gf . p) . k = q . klet m be
Nat;
( m in Xm \/ {k} implies (gf . p) . m = q . m )A38:
dom gf = the
carrier of
(TOP-REAL n)
by FUNCT_2:52;
A39:
dom g = the
carrier of
(TOP-REAL n)
by FUNCT_2:52;
assume A40:
m in Xm \/ {k}
;
(gf . p) . m = q . mthen A41:
(
m in Xm or
m in {k} )
by XBOOLE_0:def 3;
end; suppose A43:
for
k being
Nat st
k in (Seg n) \ Xm holds
(sqr (f . p)) . k < (sqr q) . k
;
ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) ex X being set st
( card X = m + 1 & X c= Seg n & ( for k being Nat st k in X holds
(f . p) . k = q . k ) )A44:
Sum (sqr (f . p)) >= 0
by RVSUM_1:86;
(
Sum (sqr q) >= 0 &
|.p.| = |.(f . p).| )
by Def4, RVSUM_1:86;
then A45:
Sum (sqr (f . p)) = Sum (sqr q)
by A2, A44, SQUARE_1:28;
A46:
len (sqr (f . p)) = len (f . p)
by RVSUM_1:143;
A47:
len (sqr q) = len q
by RVSUM_1:143;
(
len (f . p) = n &
len q = n )
by CARD_1:def 7;
then reconsider sfp =
sqr (f . p),
sq =
sqr q as
Element of
n -tuples_on REAL by A46, A47, FINSEQ_2:92;
m < n
by A16, NAT_1:13;
then
Xm <> Seg n
by A13, FINSEQ_1:57;
then
Xm c< Seg n
by A14, XBOOLE_0:def 8;
then consider z being
object such that A48:
z in Seg n
and A49:
not
z in Xm
by XBOOLE_0:6;
reconsider z =
z as
Nat by A48;
A50:
z in (Seg n) \ Xm
by A48, A49, XBOOLE_0:def 5;
for
k being
Nat st
k in Seg n holds
sfp . k <= sq . k
then
sfp . z >= sq . z
by A45, A48, RVSUM_1:83;
hence
ex
f being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) ex
X being
set st
(
card X = m + 1 &
X c= Seg n & ( for
k being
Nat st
k in X holds
(f . p) . k = q . k ) )
by A43, A50;
verum end; end;
end; reconsider n1 =
n - 1 as
Nat by A5;
A52:
n1 + 1
= n
;
A53:
S1[
0 ]
for
m being
Nat holds
S1[
m]
from NAT_1:sch 2(A53, A10);
then consider f being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n),
X being
set such that A54:
(
card X = n1 &
X c= Seg n )
and A55:
for
k being
Nat st
k in X holds
(f . p) . k = q . k
by A52;
card ((Seg n) \ X) = n - n1
by A9, A54, CARD_2:44;
then consider z being
object such that A56:
{z} = (Seg n) \ X
by CARD_2:42;
set fp =
f . p;
(
Sum (sqr (f . p)) >= 0 &
|.p.| = |.(f . p).| )
by Def4, RVSUM_1:86;
then A57:
Sum (sqr q) = Sum (sqr (f . p))
by A2, A8, SQUARE_1:28;
A58:
z in {z}
by TARSKI:def 1;
then A59:
z in Seg n
by A56, XBOOLE_0:def 5;
reconsider z =
z as
Nat by A56, A58;
set fpz =
(f . p) +* (
z,
(q . z));
A60:
len (f . p) = n
by CARD_1:def 7;
then A61:
dom (f . p) = Seg n
by FINSEQ_1:def 3;
A62:
for
k being
Nat st 1
<= k &
k <= n holds
((f . p) +* (z,(q . z))) . k = q . k
proof
let k be
Nat;
( 1 <= k & k <= n implies ((f . p) +* (z,(q . z))) . k = q . k )
assume
( 1
<= k &
k <= n )
;
((f . p) +* (z,(q . z))) . k = q . k
then A63:
k in Seg n
;
end; A66:
(
len ((f . p) +* (z,(q . z))) = len (f . p) &
len q = n )
by CARD_1:def 7, FUNCT_7:97;
then A67:
(f . p) +* (
z,
(q . z))
= q
by A60, A62;
then A68:
Sum (sqr q) = ((Sum (sqr (f . p))) - (((f . p) . z) ^2)) + ((q . z) ^2)
by A59, A61, Th3;
per cases
( (f . p) . z = q . z or (f . p) . z = - (q . z) )
by A68, A57, SQUARE_1:40;
suppose A69:
(f . p) . z = - (q . z)
;
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q )
1
< n
by A1, A7, XXREAL_0:1;
then
1
+ 1
<= n
by NAT_1:13;
then consider h being
additive homogeneous Function of
(TOP-REAL n),
(TOP-REAL n) such that A70:
h is
base_rotation
and A71:
h . (f . p) = (f . p) +* (
z,
(- ((f . p) . z)))
by A59, Th34;
dom (h * f) = the
carrier of
(TOP-REAL n)
by FUNCT_2:52;
then (h * f) . p =
(f . p) +* (
z,
(- ((f . p) . z)))
by A71, FUNCT_1:12
.=
q
by A60, A62, A66, A69
;
hence
ex
f being
additive homogeneous Function of
(TOP-REAL n),
(TOP-REAL n) st
(
f is
base_rotation &
f . p = q )
by A70;
verum end; end; end; end;