let i, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st i in Seg n & n >= 2 holds
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) )
let p be Point of (TOP-REAL n); :: thesis: ( i in Seg n & n >= 2 implies ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) ) )
set TR = TOP-REAL n;
assume that
A1: i in Seg n and
A2: n >= 2 ; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) )
A3: {i} c= Seg n by A1, ZFMISC_1:31;
A4: 1 <= i by A1, FINSEQ_1:1;
( card (Seg n) = n & card {i} = 1 ) by CARD_2:42, FINSEQ_1:57;
then {i} <> Seg n by A2;
then {i} c< Seg n by A3, XBOOLE_0:def 8;
then consider j being object such that
A5: j in Seg n and
A6: not j in {i} by XBOOLE_0:6;
reconsider j = j as Nat by A5;
A7: j <> i by A6, TARSKI:def 1;
A8: 1 <= j by A5, FINSEQ_1:1;
set p0 = p +* (i,(- (p . i)));
A9: len (p +* (i,(- (p . i)))) = len p by FUNCT_7:97;
A10: len p = n by CARD_1:def 7;
then A11: dom p = Seg n by FINSEQ_1:def 3;
A12: i <= n by A1, FINSEQ_1:1;
( (p . i) * (p . i) >= 0 & (p . j) * (p . j) >= 0 ) by XREAL_1:63;
then A13: ( 0 ^2 = 0* 0 & 0 <= ((p . i) ^2) + ((p . j) ^2) ) ;
A14: j <= n by A5, FINSEQ_1:1;
per cases ( i < j or j < i ) by A7, XXREAL_0:1;
suppose A15: i < j ; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) )
then consider r being Real such that
A16: ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = 0 by A4, A13, A14, Th24;
set s = sin r;
set c = cos r;
A17: 0 = ((p . i) * (cos r)) + ((p . j) * (- (sin r))) by A4, A14, A15, A16, Th21;
reconsider M = Mx2Tran (Rotation (i,j,n,(r + r))) as base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A4, A14, A15, Th28;
set Mp = M . p;
A18: ( cos (r + r) = ((cos r) * (cos r)) - ((sin r) * (sin r)) & sin (r + r) = ((sin r) * (cos r)) + ((sin r) * (cos r)) ) by SIN_COS:75;
A19: M is {i,j} -support-yielding by A4, A14, A15, Th26;
A20: for k being Nat st 1 <= k & k <= n holds
(p +* (i,(- (p . i)))) . k = (M . p) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= n implies (p +* (i,(- (p . i)))) . k = (M . p) . k )
assume ( 1 <= k & k <= n ) ; :: thesis: (p +* (i,(- (p . i)))) . k = (M . p) . k
then A21: k in Seg n ;
per cases ( i = k or j = k or ( i <> k & j <> k ) ) ;
suppose A22: i = k ; :: thesis: (p +* (i,(- (p . i)))) . k = (M . p) . k
hence (p +* (i,(- (p . i)))) . k = - ((p . i) * 1) by A11, A21, FUNCT_7:31
.= - ((p . i) * (((sin r) * (sin r)) + ((cos r) * (cos r)))) by SIN_COS:29
.= (((p . i) * (((cos r) * (cos r)) - ((sin r) * (sin r)))) - (((p . i) * (cos r)) * (cos r))) - (((p . i) * (cos r)) * (cos r))
.= (((p . i) * (((cos r) * (cos r)) - ((sin r) * (sin r)))) - (((p . j) * (sin r)) * (cos r))) - (((p . j) * (sin r)) * (cos r)) by A17
.= ((p . i) * (((cos r) * (cos r)) - ((sin r) * (sin r)))) + ((p . j) * (- (((sin r) * (cos r)) + ((sin r) * (cos r)))))
.= (M . p) . k by A4, A14, A15, A18, A22, Th21 ;
:: thesis: verum
end;
suppose A23: j = k ; :: thesis: (p +* (i,(- (p . i)))) . k = (M . p) . k
hence (p +* (i,(- (p . i)))) . k = (p . j) * 1 by A15, FUNCT_7:32
.= (p . j) * (((sin r) * (sin r)) + ((cos r) * (cos r))) by SIN_COS:29
.= ((((p . j) * (sin r)) * (sin r)) + (((p . j) * (sin r)) * (sin r))) + ((p . j) * (((cos r) * (cos r)) - ((sin r) * (sin r))))
.= ((((p . i) * (cos r)) * (sin r)) + (((p . i) * (cos r)) * (sin r))) + ((p . j) * (((cos r) * (cos r)) - ((sin r) * (sin r)))) by A17
.= ((p . i) * (((sin r) * (cos r)) + ((sin r) * (cos r)))) + ((p . j) * (((cos r) * (cos r)) - ((sin r) * (sin r))))
.= (M . p) . k by A4, A14, A15, A18, A23, Th22 ;
:: thesis: verum
end;
suppose A24: ( i <> k & j <> k ) ; :: thesis: (p +* (i,(- (p . i)))) . k = (M . p) . k
A25: dom M = the carrier of (TOP-REAL n) by FUNCT_2:52;
( (p +* (i,(- (p . i)))) . k = p . k & not k in {i,j} ) by A24, FUNCT_7:32, TARSKI:def 2;
hence (p +* (i,(- (p . i)))) . k = (M . p) . k by A19, A25; :: thesis: verum
end;
end;
end;
take M ; :: thesis: ( M is base_rotation & M . p = p +* (i,(- (p . i))) )
len (M . p) = n by CARD_1:def 7;
hence ( M is base_rotation & M . p = p +* (i,(- (p . i))) ) by A9, A10, A20; :: thesis: verum
end;
suppose A26: j < i ; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) )
then consider r being Real such that
A27: ((Mx2Tran (Rotation (j,i,n,r))) . p) . i = 0 by A8, A12, A13, Th25;
set s = sin r;
set c = cos r;
A28: 0 = ((p . j) * (sin r)) + ((p . i) * (cos r)) by A8, A12, A26, A27, Th22;
reconsider M = Mx2Tran (Rotation (j,i,n,(r + r))) as base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A8, A12, A26, Th28;
set Mp = M . p;
A29: ( cos (r + r) = ((cos r) * (cos r)) - ((sin r) * (sin r)) & sin (r + r) = ((sin r) * (cos r)) + ((sin r) * (cos r)) ) by SIN_COS:75;
A30: M is {i,j} -support-yielding by A8, A12, A26, Th26;
A31: for k being Nat st 1 <= k & k <= n holds
(p +* (i,(- (p . i)))) . k = (M . p) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= n implies (p +* (i,(- (p . i)))) . k = (M . p) . k )
assume ( 1 <= k & k <= n ) ; :: thesis: (p +* (i,(- (p . i)))) . k = (M . p) . k
then A32: k in Seg n ;
per cases ( i = k or j = k or ( i <> k & j <> k ) ) ;
suppose A33: i = k ; :: thesis: (p +* (i,(- (p . i)))) . k = (M . p) . k
hence (p +* (i,(- (p . i)))) . k = - ((p . i) * 1) by A11, A32, FUNCT_7:31
.= - ((p . i) * (((sin r) * (sin r)) + ((cos r) * (cos r)))) by SIN_COS:29
.= ((- (((p . i) * (cos r)) * (cos r))) + ((- ((p . i) * (cos r))) * (cos r))) + ((p . i) * (((cos r) * (cos r)) - ((sin r) * (sin r))))
.= ((((p . j) * (sin r)) * (cos r)) + (((p . j) * (sin r)) * (cos r))) + ((p . i) * (((cos r) * (cos r)) - ((sin r) * (sin r)))) by A28
.= ((p . j) * (((sin r) * (cos r)) + ((sin r) * (cos r)))) + ((p . i) * (((cos r) * (cos r)) - ((sin r) * (sin r))))
.= (M . p) . k by A8, A12, A26, A29, A33, Th22 ;
:: thesis: verum
end;
suppose A34: j = k ; :: thesis: (p +* (i,(- (p . i)))) . k = (M . p) . k
hence (p +* (i,(- (p . i)))) . k = (p . j) * 1 by A26, FUNCT_7:32
.= (p . j) * (((sin r) * (sin r)) + ((cos r) * (cos r))) by SIN_COS:29
.= (((p . j) * (((cos r) * (cos r)) - ((sin r) * (sin r)))) + (((p . j) * (sin r)) * (sin r))) + (((p . j) * (sin r)) * (sin r))
.= (((p . j) * (((cos r) * (cos r)) - ((sin r) * (sin r)))) + ((- ((p . i) * (cos r))) * (sin r))) + ((- ((p . i) * (cos r))) * (sin r)) by A28
.= ((p . j) * (((cos r) * (cos r)) - ((sin r) * (sin r)))) + ((p . i) * (- (((sin r) * (cos r)) + ((sin r) * (cos r)))))
.= (M . p) . k by A8, A12, A26, A29, A34, Th21 ;
:: thesis: verum
end;
suppose A35: ( i <> k & j <> k ) ; :: thesis: (p +* (i,(- (p . i)))) . k = (M . p) . k
A36: dom M = the carrier of (TOP-REAL n) by FUNCT_2:52;
( (p +* (i,(- (p . i)))) . k = p . k & not k in {i,j} ) by A35, FUNCT_7:32, TARSKI:def 2;
hence (p +* (i,(- (p . i)))) . k = (M . p) . k by A30, A36; :: thesis: verum
end;
end;
end;
take M ; :: thesis: ( M is base_rotation & M . p = p +* (i,(- (p . i))) )
len (M . p) = n by CARD_1:def 7;
hence ( M is base_rotation & M . p = p +* (i,(- (p . i))) ) by A9, A10, A31; :: thesis: verum
end;
end;