let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)
for A being Subset of (TOP-REAL n) st f is rotation & f | A = id A holds
for i being Nat st i in Seg n & Base_FinSeq (n,i) in Lin A holds
(f . p) . i = p . i
let p be Point of (TOP-REAL n); :: thesis: for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)
for A being Subset of (TOP-REAL n) st f is rotation & f | A = id A holds
for i being Nat st i in Seg n & Base_FinSeq (n,i) in Lin A holds
(f . p) . i = p . i
let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: for A being Subset of (TOP-REAL n) st f is rotation & f | A = id A holds
for i being Nat st i in Seg n & Base_FinSeq (n,i) in Lin A holds
(f . p) . i = p . i
set TR = TOP-REAL n;
let A be Subset of (TOP-REAL n); :: thesis: ( f is rotation & f | A = id A implies for i being Nat st i in Seg n & Base_FinSeq (n,i) in Lin A holds
(f . p) . i = p . i )
assume that
A1: f is rotation and
A2: f | A = id A ; :: thesis: for i being Nat st i in Seg n & Base_FinSeq (n,i) in Lin A holds
(f . p) . i = p . i
set L = Lin A;
set n0 = 0* n;
A3: f | (Lin A) = id (Lin A) by A2, Th31;
A4: len (0* n) = n by CARD_1:def 7;
then A5: dom (0* n) = Seg n by FINSEQ_1:def 3;
let k be Nat; :: thesis: ( k in Seg n & Base_FinSeq (n,k) in Lin A implies (f . p) . k = p . k )
assume that
A6: k in Seg n and
A7: Base_FinSeq (n,k) in Lin A ; :: thesis: (f . p) . k = p . k
set n0k = (0* n) +* (k,1);
A8: (0* n) +* (k,1) = Base_FinSeq (n,k) by MATRIXR2:def 4;
set pk = p . k;
the carrier of (Lin A) c= the carrier of (TOP-REAL n) by RLSUB_1:def 2;
then A9: f | (Lin A) = f | the carrier of (Lin A) by TMAP_1:def 3;
dom ((0* n) +* (k,1)) = dom (0* n) by FUNCT_7:30;
then A10: len ((0* n) +* (k,1)) = n by A4, FINSEQ_3:29;
A11: (0* n) +* (k,1) = @ (@ ((0* n) +* (k,1))) ;
then reconsider N0k = (0* n) +* (k,1) as Point of (TOP-REAL n) by A10, TOPREAL3:46;
A12: (0* n) +* (k,1) is Element of n -tuples_on REAL by A10, A11, FINSEQ_2:92;
A13: for p being Point of (TOP-REAL n) st p . k <> 0 holds
(f . p) . k = p . k

proof

let p be Point of (TOP-REAL n); :: thesis: ( p . k <> 0 implies (f . p) . k = p . k )
assume A14: p . k <> 0 ; :: thesis: (f . p) . k = p . k
set fp = f . p;
set pk = p . k;
set pN = (p . k) * N0k;
set ppN = p - ((p . k) * N0k);
A15: (f . (p - ((p . k) * N0k))) + (f . ((p . k) * N0k)) = f . ((p - ((p . k) * N0k)) + ((p . k) * N0k)) by VECTSP_1:def 20;
( len (f . (p - ((p . k) * N0k))) = n & len (f . ((p . k) * N0k)) = n ) by CARD_1:def 7;
then A16: |.(f . ((p - ((p . k) * N0k)) + ((p . k) * N0k))).| ^2 = ((|.(f . (p - ((p . k) * N0k))).| ^2) + (2 * |((f . ((p . k) * N0k)),(f . (p - ((p . k) * N0k))))|)) + (|.(f . ((p . k) * N0k)).| ^2) by A15, EUCLID_2:11;
A17: (n |-> (p . k)) . k = p . k by A6, FINSEQ_2:57;
A18: (p . k) * ((0* n) +* (k,1)) = mlt ((n |-> (p . k)),((0* n) +* (k,1))) by A12, RVSUM_1:63
.= (0* n) +* (k,((p . k) * 1)) by A17, TOPREALC:15
.= (0* n) +* (k,(p . k)) ;
len (f . p) = n by CARD_1:def 7;
then A19: dom (f . p) = Seg n by FINSEQ_1:def 3;
A20: len (p - ((p . k) * N0k)) = n by CARD_1:def 7;
then dom (p - ((p . k) * N0k)) = Seg n by FINSEQ_1:def 3;
then A21: (p - ((p . k) * N0k)) . k = (p . k) - (((p . k) * N0k) . k) by A6, VALUED_1:13;
len ((p . k) * N0k) = n by CARD_1:def 7;
then A22: |.((p - ((p . k) * N0k)) + ((p . k) * N0k)).| ^2 = ((|.(p - ((p . k) * N0k)).| ^2) + (2 * |(((p . k) * N0k),(p - ((p . k) * N0k)))|)) + (|.((p . k) * N0k).| ^2) by A20, EUCLID_2:11;
(p . k) * N0k in Lin A by A7, A8, RLSUB_1:21;
then A23: (p . k) * N0k in the carrier of (Lin A) ;
then A24: (p . k) * N0k = (f | (Lin A)) . ((p . k) * N0k) by A3, FUNCT_1:17
.= f . ((p . k) * N0k) by A9, A23, FUNCT_1:49 ;
( |.((p - ((p . k) * N0k)) + ((p . k) * N0k)).| = |.(f . ((p - ((p . k) * N0k)) + ((p . k) * N0k))).| & |.(p - ((p . k) * N0k)).| = |.(f . (p - ((p . k) * N0k))).| ) by A1;
then |(((p . k) * N0k),(p - ((p . k) * N0k)))| = (p . k) * ((f . (p - ((p . k) * N0k))) . k) by A18, A16, A22, A24, TOPREALC:16;
then A25: (p . k) * ((p - ((p . k) * N0k)) . k) = (p . k) * ((f . (p - ((p . k) * N0k))) . k) by A18, TOPREALC:16;
((p . k) * N0k) . k = p . k by A6, A5, A18, FUNCT_7:31;
then A26: (f . (p - ((p . k) * N0k))) . k = 0 by A14, A21, A25;
(p - ((p . k) * N0k)) + ((p . k) * N0k) = p - (((p . k) * N0k) - ((p . k) * N0k)) by RLVECT_1:29
.= p - (0. (TOP-REAL n)) by RLVECT_1:5
.= p by RLVECT_1:13 ;
then (f . p) . k = ((f . (p - ((p . k) * N0k))) . k) + ((f . ((p . k) * N0k)) . k) by A6, A15, A19, VALUED_1:def 1
.= ((f . (p - ((p . k) * N0k))) . k) + (p . k) by A6, A5, A18, A24, FUNCT_7:31 ;
hence (f . p) . k = p . k by A26; :: thesis: verum

end;

per cases ( p . k <> 0 or p . k = 0 ) ;

suppose p . k <> 0 ; :: thesis: (f . p) . k = p . k

hence (f . p) . k = p . k by A13; :: thesis: verum

end;

suppose p . k = 0 ; :: thesis: (f . p) . k = p . k

len (f . p) = n by CARD_1:def 7;
then A27: |.((f . p) + N0k).| ^2 = ((|.(f . p).| ^2) + (2 * |(N0k,(f . p))|)) + (|.N0k.| ^2) by A10, EUCLID_2:11;
len p = n by CARD_1:def 7;
then A28: |.(p + N0k).| ^2 = ((|.p.| ^2) + (2 * |(N0k,p)|)) + (|.N0k.| ^2) by A10, EUCLID_2:11;
A29: N0k in the carrier of (Lin A) by A7, A8;
then N0k = (f | (Lin A)) . N0k by A3, FUNCT_1:17
.= f . N0k by A9, A29, FUNCT_1:49 ;
then A30: f . (p + N0k) = (f . p) + N0k by VECTSP_1:def 20;
( |.(p + N0k).| = |.(f . (p + N0k)).| & |.(f . p).| = |.p.| ) by A1;
then |(N0k,(f . p))| = 1 * (p . k) by A27, A28, A30, TOPREALC:16;
then p . k = 1 * ((f . p) . k) by TOPREALC:16;
hence (f . p) . k = p . k ; :: thesis: verum

end;

end;