let X be set ; for k, n being Nat
for p being Point of (TOP-REAL n) st k in X & k in Seg n holds
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds
(f . p) . i = 0 ) )
let k, n be Nat; for p being Point of (TOP-REAL n) st k in X & k in Seg n holds
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds
(f . p) . i = 0 ) )
let p be Point of (TOP-REAL n); ( k in X & k in Seg n implies ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds
(f . p) . i = 0 ) ) )
assume that
A1:
k in X
and
A2:
k in Seg n
; ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds
(f . p) . i = 0 ) )
set TR = TOP-REAL n;
defpred S1[ Nat] means ( $1 <= n implies ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( f is (X /\ (Seg $1)) \/ {k} -support-yielding & ( card ((X /\ (Seg $1)) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg $1) & i <> k holds
(f . p) . i = 0 ) ) );
A3:
for z being Nat st S1[z] holds
S1[z + 1]
proof
let z be
Nat;
( S1[z] implies S1[z + 1] )
set z1 =
z + 1;
assume A4:
S1[
z]
;
S1[z + 1]
A5:
Seg (z + 1) = (Seg z) \/ {(z + 1)}
by FINSEQ_1:9;
A6:
Seg (z + 1) = (Seg z) \/ {(z + 1)}
by FINSEQ_1:9;
A7:
(
z + 1
in X implies
((X /\ (Seg z)) \/ {k}) \/ {(z + 1),k} = (X /\ (Seg (z + 1))) \/ {k} )
assume A9:
z + 1
<= n
;
ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( f is (X /\ (Seg (z + 1))) \/ {k} -support-yielding & ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 ) )
then consider f being
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) such that A10:
f is
(X /\ (Seg z)) \/ {k} -support-yielding
and A11:
(
card ((X /\ (Seg z)) \/ {k}) > 1 implies
(f . p) . k >= 0 )
and A12:
for
m being
Nat st
m in X /\ (Seg z) &
m <> k holds
(f . p) . m = 0
by A4, NAT_1:13;
set z1 =
z + 1;
per cases
( z + 1 = k or not z + 1 in X or ( z + 1 < k & z + 1 in X ) or ( z + 1 > k & z + 1 in X ) )
by XXREAL_0:1;
suppose A13:
z + 1
= k
;
ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( f is (X /\ (Seg (z + 1))) \/ {k} -support-yielding & ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 ) )take
f
;
( f is (X /\ (Seg (z + 1))) \/ {k} -support-yielding & ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 ) )(Seg (z + 1)) \/ {(z + 1)} =
(Seg z) \/ ({(z + 1)} \/ {(z + 1)})
by A5, XBOOLE_1:4
.=
(Seg z) \/ {(z + 1)}
;
then A14:
(X /\ (Seg (z + 1))) \/ {k} =
(X \/ {k}) /\ ((Seg z) \/ {k})
by A13, XBOOLE_1:24
.=
(X /\ (Seg z)) \/ {k}
by XBOOLE_1:24
;
hence
f is
(X /\ (Seg (z + 1))) \/ {k} -support-yielding
by A10;
( ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 ) )thus
(
card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies
(f . p) . k >= 0 )
by A11, A14;
for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 let m be
Nat;
( m in X /\ (Seg (z + 1)) & m <> k implies (f . p) . m = 0 )assume that A15:
m in X /\ (Seg (z + 1))
and A16:
m <> k
;
(f . p) . m = 0 A17:
m in Seg (z + 1)
by A15, XBOOLE_0:def 4;
A18:
m in X
by A15, XBOOLE_0:def 4;
not
m in {(z + 1)}
by A13, A16, TARSKI:def 1;
then
m in Seg z
by A5, A17, XBOOLE_0:def 3;
then
m in X /\ (Seg z)
by A18, XBOOLE_0:def 4;
hence
(f . p) . m = 0
by A12, A16;
verum end; suppose A19:
not
z + 1
in X
;
ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( f is (X /\ (Seg (z + 1))) \/ {k} -support-yielding & ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 ) )take
f
;
( f is (X /\ (Seg (z + 1))) \/ {k} -support-yielding & ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 ) )A20:
{(z + 1)} misses X
by A19, ZFMISC_1:50;
A21:
X /\ (Seg (z + 1)) =
(X /\ (Seg z)) \/ (X /\ {(z + 1)})
by A5, XBOOLE_1:23
.=
(X /\ (Seg z)) \/ {}
by A20, XBOOLE_0:def 7
.=
X /\ (Seg z)
;
hence
f is
(X /\ (Seg (z + 1))) \/ {k} -support-yielding
by A10;
( ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 ) )thus
(
card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies
(f . p) . k >= 0 )
by A11, A21;
for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 let m be
Nat;
( m in X /\ (Seg (z + 1)) & m <> k implies (f . p) . m = 0 )assume that A22:
m in X /\ (Seg (z + 1))
and A23:
m <> k
;
(f . p) . m = 0 A24:
m in Seg (z + 1)
by A22, XBOOLE_0:def 4;
A25:
m in X
by A22, XBOOLE_0:def 4;
then
not
m in {(z + 1)}
by A19, TARSKI:def 1;
then
m in Seg z
by A5, A24, XBOOLE_0:def 3;
then
m in X /\ (Seg z)
by A25, XBOOLE_0:def 4;
hence
(f . p) . m = 0
by A12, A23;
verum end; suppose A26:
(
z + 1
< k &
z + 1
in X )
;
ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( f is (X /\ (Seg (z + 1))) \/ {k} -support-yielding & ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 ) )set fp =
f . p;
set S =
(((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2);
A27:
(
z + 1
>= 1 &
k <= n )
by A2, FINSEQ_1:1, NAT_1:11;
A28:
(
((f . p) . k) ^2 >= 0 &
((f . p) . (z + 1)) ^2 >= 0 )
by XREAL_1:63;
then A29:
(sqrt ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2))) ^2 = (((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2)
by SQUARE_1:def 2;
then consider r being
Real such that A30:
((Mx2Tran (Rotation ((z + 1),k,n,r))) . (f . p)) . k = sqrt ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2))
by A26, A27, Th25;
reconsider M =
Mx2Tran (Rotation ((z + 1),k,n,r)) as
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) by A26, A27, Th28;
take Mf =
M * f;
( Mf is (X /\ (Seg (z + 1))) \/ {k} -support-yielding & ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (Mf . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(Mf . p) . i = 0 ) )A31:
M is
{(z + 1),k} -support-yielding
by A26, A27, Th26;
hence
Mf is
(X /\ (Seg (z + 1))) \/ {k} -support-yielding
by A7, A10, A26;
( ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (Mf . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(Mf . p) . i = 0 ) )A32:
dom Mf = the
carrier of
(TOP-REAL n)
by FUNCT_2:52;
then A33:
f . p in dom M
by FUNCT_1:11;
A34:
Mf . p = M . (f . p)
by A32, FUNCT_1:12;
hence
(
card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies
(Mf . p) . k >= 0 )
by A28, A30, SQUARE_1:def 2;
for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(Mf . p) . i = 0 let i be
Nat;
( i in X /\ (Seg (z + 1)) & i <> k implies (Mf . p) . i = 0 )assume that A35:
i in X /\ (Seg (z + 1))
and A36:
i <> k
;
(Mf . p) . i = 0 A37:
i in X
by A35, XBOOLE_0:def 4;
i in Seg (z + 1)
by A35, XBOOLE_0:def 4;
then A38:
(
i in Seg z or
i in {(z + 1)} )
by A5, XBOOLE_0:def 3;
end; suppose A42:
(
z + 1
> k &
z + 1
in X )
;
ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( f is (X /\ (Seg (z + 1))) \/ {k} -support-yielding & ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(f . p) . i = 0 ) )set fp =
f . p;
set S =
(((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2);
A43:
1
<= k
by A2, FINSEQ_1:1;
A44:
(
((f . p) . k) ^2 >= 0 &
((f . p) . (z + 1)) ^2 >= 0 )
by XREAL_1:63;
then A45:
(sqrt ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2))) ^2 = (((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2)
by SQUARE_1:def 2;
then consider r being
Real such that A46:
((Mx2Tran (Rotation (k,(z + 1),n,r))) . (f . p)) . k = sqrt ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2))
by A9, A42, A43, Th24;
reconsider M =
Mx2Tran (Rotation (k,(z + 1),n,r)) as
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) by A9, A42, A43, Th28;
take Mf =
M * f;
( Mf is (X /\ (Seg (z + 1))) \/ {k} -support-yielding & ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (Mf . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(Mf . p) . i = 0 ) )A47:
M is
{k,(z + 1)} -support-yielding
by A9, A42, A43, Th26;
hence
Mf is
(X /\ (Seg (z + 1))) \/ {k} -support-yielding
by A7, A10, A42;
( ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (Mf . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(Mf . p) . i = 0 ) )A48:
dom Mf = the
carrier of
(TOP-REAL n)
by FUNCT_2:52;
then A49:
Mf . p = M . (f . p)
by FUNCT_1:12;
hence
(
card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies
(Mf . p) . k >= 0 )
by A44, A46, SQUARE_1:def 2;
for i being Nat st i in X /\ (Seg (z + 1)) & i <> k holds
(Mf . p) . i = 0 let i be
Nat;
( i in X /\ (Seg (z + 1)) & i <> k implies (Mf . p) . i = 0 )assume that A50:
i in X /\ (Seg (z + 1))
and A51:
i <> k
;
(Mf . p) . i = 0 A52:
i in X
by A50, XBOOLE_0:def 4;
i in Seg (z + 1)
by A50, XBOOLE_0:def 4;
then A53:
(
i in Seg z or
i in {(z + 1)} )
by A5, XBOOLE_0:def 3;
end; end;
end;
A58:
S1[ 0 ]
for z being Nat holds S1[z]
from NAT_1:sch 2(A58, A3);
then consider f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) such that
A60:
( f is (X /\ (Seg n)) \/ {k} -support-yielding & ( card ((X /\ (Seg n)) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds
(f . p) . i = 0 ) )
;
take
f
; ( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds
(f . p) . i = 0 ) )
A61:
X /\ (Seg n) c= X
by XBOOLE_1:17;
( {k} c= X & {k} c= Seg n )
by A1, A2, ZFMISC_1:31;
then
(X /\ (Seg n)) \/ {k} = X /\ (Seg n)
by XBOOLE_1:12, XBOOLE_1:19;
hence
( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds
(f . p) . i = 0 ) )
by A60, A61; verum