let n be Nat; for f1 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation holds
ex f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding )
let f1 be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); ( f1 is rotation implies ex f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding ) )
set TR = TOP-REAL n;
assume A1:
f1 is rotation
; ex f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding )
set cTR = the carrier of (TOP-REAL n);
set f = f1;
A2:
dom f1 = the carrier of (TOP-REAL n)
by FUNCT_2:52;
A3:
rng f1 c= the carrier of (TOP-REAL n)
by RELAT_1:def 19;
per cases
( n = 0 or n > 0 )
;
suppose
n > 0
;
ex f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding )then reconsider n1 =
n - 1 as
Nat ;
defpred S1[
Nat]
means ( $1
<= n - 1 implies for
S being
Subset of
(TOP-REAL n) st
S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= $1 ) } holds
ex
g being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) st
(g * f1) | S = id S );
set S =
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n1 ) } ;
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n1 ) } c= the
carrier of
(TOP-REAL n)
then reconsider S =
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n1 ) } as
Subset of
(TOP-REAL n) ;
A9:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let z be
Nat;
( S1[z] implies S1[z + 1] )
assume A10:
S1[
z]
;
S1[z + 1]
set z1 =
z + 1;
set SS =
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z ) } ;
assume A11:
z + 1
<= n - 1
;
for S being Subset of (TOP-REAL n) st S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z + 1 ) } holds
ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S
then reconsider n1 =
n - 1 as
Element of
NAT by INT_1:3;
A12:
n1 < n1 + 1
by NAT_1:13;
then A13:
z + 1
< n
by A11, XXREAL_0:2;
set B =
Base_FinSeq (
n,
(z + 1));
set X =
{ i where i is Element of NAT : ( z + 1 <= i & i <= n ) } ;
let S be
Subset of
(TOP-REAL n);
( S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z + 1 ) } implies ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S )
assume A14:
S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z + 1 ) }
;
ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z ) } c= S
then reconsider SS =
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z ) } as
Subset of
(TOP-REAL n) by XBOOLE_1:1;
z < n1
by A11, NAT_1:13;
then consider g being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) such that A17:
(g * f1) | SS = id SS
by A10;
n in NAT
by ORDINAL1:def 12;
then A18:
n in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) }
by A13;
n >= 1
by A12, NAT_1:14;
then
n in Seg n
;
then A19:
n in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n)
by A18, XBOOLE_0:def 4;
A20:
card {(z + 1),n} = 2
by A11, A12, CARD_2:57;
A21:
1
<= z + 1
by NAT_1:11;
then A22:
z + 1
in Seg n
by A13;
Base_FinSeq (
n,
(z + 1))
in S
by A14, A21;
then reconsider B =
Base_FinSeq (
n,
(z + 1)) as
Point of
(TOP-REAL n) ;
set gfB =
(g * f1) . B;
A23:
z + 1
in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) }
by A13;
then consider h being
additive homogeneous Function of
(TOP-REAL n),
(TOP-REAL n) such that A24:
(
h is
{ i where i is Element of NAT : ( z + 1 <= i & i <= n ) } -support-yielding &
h is
base_rotation )
and A25:
(
card ( { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n)) > 1 implies
(h . ((g * f1) . B)) . (z + 1) >= 0 )
and A26:
for
i being
Nat st
i in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) &
i <> z + 1 holds
(h . ((g * f1) . B)) . i = 0
by A22, Th30;
reconsider hg =
h * g as
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) by A24;
A27:
dom (hg * f1) = the
carrier of
(TOP-REAL n)
by FUNCT_2:52;
A28:
for
x being
set st
x in SS holds
(
((h * g) * f1) . x = x &
h . x = x )
proof
let x be
set ;
( x in SS implies ( ((h * g) * f1) . x = x & h . x = x ) )
assume A29:
x in SS
;
( ((h * g) * f1) . x = x & h . x = x )
reconsider B =
x as
Point of
(TOP-REAL n) by A29;
((g * f1) | SS) . x = (g * f1) . x
by A29, FUNCT_1:49;
then A30:
(g * f1) . x = x
by A17, A29, FUNCT_1:17;
A31:
ex
i being
Element of
NAT st
(
x = Base_FinSeq (
n,
i) & 1
<= i &
i <= z )
by A29;
A32:
for
j being
Nat st
j in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) holds
B . j = 0
A35:
hg * f1 = h * (g * f1)
by RELAT_1:36;
then
(h * (g * f1)) . x = h . ((g * f1) . x)
by A27, A29, FUNCT_1:12;
hence
(
((h * g) * f1) . x = x &
h . x = x )
by A24, A30, A32, A35, Th33;
verum
end;
z + 1
in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n)
by A22, A23, XBOOLE_0:def 4;
then
{(z + 1),n} c= { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n)
by A19, ZFMISC_1:32;
then A36:
1
+ 1
<= card ( { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n))
by A20, NAT_1:43;
A37:
for
x being
object st
x in S holds
((hg * f1) | S) . x = (id S) . x
proof
let x be
object ;
( x in S implies ((hg * f1) | S) . x = (id S) . x )
assume A38:
x in S
;
((hg * f1) | S) . x = (id S) . x
A39:
(id S) . x = x
by A38, FUNCT_1:17;
A40:
hg * f1 = h * (g * f1)
by RELAT_1:36;
A41:
((hg * f1) | S) . x = (hg * f1) . x
by A38, FUNCT_1:49;
consider i being
Element of
NAT such that A42:
x = Base_FinSeq (
n,
i)
and A43:
1
<= i
and A44:
i <= z + 1
by A14, A38;
per cases
( i <= z or i = z + 1 )
by A44, NAT_1:8;
suppose A45:
i = z + 1
;
((hg * f1) | S) . x = (id S) . xset H =
h . ((g * f1) . B);
A46:
(h * (g * f1)) . x = h . ((g * f1) . B)
by A27, A40, A42, A45, FUNCT_1:12;
A47:
len (h . ((g * f1) . B)) = n
by CARD_1:def 7;
A48:
for
j being
Nat st
j in Seg n &
j < z + 1 holds
(h . ((g * f1) . B)) . j = 0
proof
let j be
Nat;
( j in Seg n & j < z + 1 implies (h . ((g * f1) . B)) . j = 0 )
assume that A49:
j in Seg n
and A50:
j < z + 1
;
(h . ((g * f1) . B)) . j = 0
A51:
1
<= j
by A49, FINSEQ_1:1;
j <= z
by A50, NAT_1:13;
then A52:
Base_FinSeq (
n,
j)
in SS
by A49, A51;
then reconsider Bnj =
Base_FinSeq (
n,
j) as
Point of
(TOP-REAL n) ;
((h * g) * f1) . Bnj = Bnj
by A28, A52;
then A53:
Bnj + (h . ((g * f1) . B)) = ((h * g) * f1) . (Bnj + B)
by A40, A42, A45, A46, VECTSP_1:def 20;
A54:
len Bnj = n
by CARD_1:def 7;
|.(((h * g) * f1) . (Bnj + B)).| = |.(Bnj + B).|
by A1, A24, Def4;
then A55:
|.(Bnj + B).| ^2 = ((|.Bnj.| ^2) + (2 * |((h . ((g * f1) . B)),Bnj)|)) + (|.(h . ((g * f1) . B)).| ^2)
by A47, A53, A54, EUCLID_2:11;
A56:
Bnj = (0* n) +* (
j,1)
by MATRIXR2:def 4;
len B = n
by CARD_1:def 7;
then A57:
|.(Bnj + B).| ^2 = ((|.Bnj.| ^2) + (2 * |(B,Bnj)|)) + (|.B.| ^2)
by A54, EUCLID_2:11;
A58:
j <= n
by A49, FINSEQ_1:1;
|.(h . ((g * f1) . B)).| = |.B.|
by A1, A24, A42, A45, A46, Def4;
then (B . j) * 1 =
|((h . ((g * f1) . B)),Bnj)|
by A55, A56, A57, TOPREALC:16
.=
((h . ((g * f1) . B)) . j) * 1
by A56, TOPREALC:16
;
hence
(h . ((g * f1) . B)) . j = 0
by A50, A51, A58, MATRIXR2:76;
verum
end; set H =
h . ((g * f1) . B);
set 0H =
(0* n) +* (
(z + 1),
((h . ((g * f1) . B)) . (z + 1)));
A59:
len (0* n) = n
by CARD_1:def 7;
A60:
for
j being
Nat st
j in Seg n &
j > z + 1 holds
(h . ((g * f1) . B)) . j = 0
A63:
for
j being
Nat st 1
<= j &
j <= n holds
(h . ((g * f1) . B)) . j = ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j
(
len (h . ((g * f1) . B)) = n &
len ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) = len (0* n) )
by CARD_1:def 7, FUNCT_7:97;
then A68:
(0* n) +* (
(z + 1),
((h . ((g * f1) . B)) . (z + 1)))
= h . ((g * f1) . B)
by A59, A63;
A69:
|.((g * f1) . B).| = |.B.|
by A1, Def4;
A70:
B = (0* n) +* (
(z + 1),1)
by MATRIXR2:def 4;
then A71:
|.B.| =
|.1.|
by A22, TOPREALC:13
.=
1
by ABSVALUE:def 1
;
(
|.(h . ((g * f1) . B)).| = |.((g * f1) . B).| &
|.((h . ((g * f1) . B)) . (z + 1)).| = (h . ((g * f1) . B)) . (z + 1) )
by A24, A25, A36, Def4, ABSVALUE:def 1, NAT_1:13;
then
h . ((g * f1) . B) = B
by A22, A68, A70, A71, A69, TOPREALC:13;
hence
((hg * f1) | S) . x = (id S) . x
by A38, A39, A40, A42, A45, A46, FUNCT_1:49;
verum end; end;
end;
take
hg
;
(hg * f1) | S = id S
(
dom (id S) = S &
dom ((hg * f1) | S) = S )
by A27, RELAT_1:62;
hence
(hg * f1) | S = id S
by A37, FUNCT_1:2;
verum
end; A72:
S1[
0 ]
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A72, A9);
then consider g being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) such that A76:
(g * f1) | S = id S
;
take
g
;
( g is base_rotation & g * f1 is {n} -support-yielding )set gf =
g * f1;
thus
g is
base_rotation
;
g * f1 is {n} -support-yielding let p be
Function;
MATRTOP3:def 1 for x being set st p in dom (g * f1) & ((g * f1) . p) . x <> p . x holds
x in {n}let x be
set ;
( p in dom (g * f1) & ((g * f1) . p) . x <> p . x implies x in {n} )assume that A77:
p in dom (g * f1)
and A78:
((g * f1) . p) . x <> p . x
;
x in {n}reconsider p =
p as
Point of
(TOP-REAL n) by A77, FUNCT_2:52;
len ((g * f1) . p) = n
by CARD_1:def 7;
then
dom ((g * f1) . p) = Seg n
by FINSEQ_1:def 3;
then A79:
( not
x in Seg n implies
((g * f1) . p) . x = {} )
by FUNCT_1:def 2;
len p = n
by CARD_1:def 7;
then
dom p = Seg n
by FINSEQ_1:def 3;
then A80:
x in Seg n
by A78, A79, FUNCT_1:def 2;
assume A81:
not
x in {n}
;
contradictionreconsider x =
x as
Nat by A80;
A82:
x <= n
by A80, FINSEQ_1:1;
x <> n
by A81, TARSKI:def 1;
then
x < n1 + 1
by A82, XXREAL_0:1;
then A83:
x <= n1
by NAT_1:13;
(
x in NAT & 1
<= x )
by A80, FINSEQ_1:1;
then
Base_FinSeq (
n,
x)
in S
by A83;
then
Base_FinSeq (
n,
x)
in Lin S
by RLVECT_3:15;
then
((g * f1) . p) . x = p . x
by A1, A76, A80, Th32;
hence
contradiction
by A78;
verum end; end;