let n be Nat; for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)
for A being Subset of (TOP-REAL n) st f | A = id A holds
f | (Lin A) = id (Lin A)
let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); for A being Subset of (TOP-REAL n) st f | A = id A holds
f | (Lin A) = id (Lin A)
set TR = TOP-REAL n;
let A be Subset of (TOP-REAL n); ( f | A = id A implies f | (Lin A) = id (Lin A) )
assume A1:
f | A = id A
; f | (Lin A) = id (Lin A)
defpred S1[ Nat] means for L being Linear_Combination of A st card (Carrier L) <= $1 holds
f . (Sum L) = Sum L;
A2:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A3:
S1[
i]
;
S1[i + 1]
set i1 =
i + 1;
let L be
Linear_Combination of
A;
( card (Carrier L) <= i + 1 implies f . (Sum L) = Sum L )
assume A4:
card (Carrier L) <= i + 1
;
f . (Sum L) = Sum L
per cases
( card (Carrier L) <= i or card (Carrier L) = i + 1 )
by A4, NAT_1:8;
suppose A5:
card (Carrier L) = i + 1
;
f . (Sum L) = Sum Lthen
not
Carrier L is
empty
;
then consider x being
object such that A6:
x in Carrier L
by XBOOLE_0:def 1;
reconsider x =
x as
Point of
(TOP-REAL n) by A6;
reconsider X =
{x} as
Subset of
(TOP-REAL n) by ZFMISC_1:31;
consider K being
Linear_Combination of
X such that A7:
K . x = L . x
by RLVECT_4:37;
L . x <> 0
by A6, RLVECT_2:19;
then
(
Carrier K c= {x} &
x in Carrier K )
by A7, RLVECT_2:19, RLVECT_2:def 6;
then A8:
Carrier K = {x}
by ZFMISC_1:33;
{x} \/ (Carrier L) = Carrier L
by A6, ZFMISC_1:40;
then A9:
Carrier (L - K) c= Carrier L
by A8, RLVECT_2:55;
(L - K) . x =
(L . x) - (K . x)
by RLVECT_2:54
.=
0
by A7
;
then
not
x in Carrier (L - K)
by RLVECT_2:19;
then
Carrier (L - K) c< Carrier L
by A6, A9, XBOOLE_0:def 8;
then
card (Carrier (L - K)) < i + 1
by A5, CARD_2:48;
then A10:
card (Carrier (L - K)) <= i
by NAT_1:13;
ZeroLC (TOP-REAL n) =
(- K) - (- K)
by RLVECT_2:57
.=
(- K) + (- (- K))
by RLVECT_2:def 13
.=
(- K) + K
by RLVECT_2:53
;
then L =
L + ((- K) + K)
by RLVECT_2:41
.=
(L + (- K)) + K
by RLVECT_2:40
.=
(L - K) + K
by RLVECT_2:def 13
;
then A11:
Sum L = (Sum (L - K)) + (Sum K)
by RLVECT_3:1;
A12:
Carrier L c= A
by RLVECT_2:def 6;
then
(f | A) . x = f . x
by A6, FUNCT_1:49;
then A13:
f . x = x
by A1, A6, A12, FUNCT_1:17;
Carrier (L - K) c= A
by A9, A12;
then
L - K is
Linear_Combination of
A
by RLVECT_2:def 6;
then A14:
f . (Sum (L - K)) = Sum (L - K)
by A3, A10;
Sum K = (L . x) * x
by A7, RLVECT_2:32;
then
f . (Sum K) = Sum K
by A13, TOPREAL9:def 4;
hence
f . (Sum L) = Sum L
by A11, A14, VECTSP_1:def 20;
verum end;
end;
set L = Lin A;
set cL = the carrier of (Lin A);
the carrier of (Lin A) c= the carrier of (TOP-REAL n)
by RLSUB_1:def 2;
then A15:
f | (Lin A) = f | the carrier of (Lin A)
by TMAP_1:def 3;
A16:
S1[ 0 ]
A18:
for i being Nat holds S1[i]
from NAT_1:sch 2(A16, A2);
A19:
for x being object st x in the carrier of (Lin A) holds
(f | (Lin A)) . x = (id (Lin A)) . x
( dom (f | (Lin A)) = the carrier of (Lin A) & dom (id (Lin A)) = the carrier of (Lin A) )
by FUNCT_2:def 1;
hence
f | (Lin A) = id (Lin A)
by A19, FUNCT_1:2; verum