let i, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st i in Seg n holds
(Mx2Tran (AxialSymmetry (i,n))) . p = p +* (i,(- (p . i)))
let p be Point of (TOP-REAL n); :: thesis: ( i in Seg n implies (Mx2Tran (AxialSymmetry (i,n))) . p = p +* (i,(- (p . i))) )
set S = Seg n;
set Mp = (Mx2Tran (AxialSymmetry (i,n))) . p;
set p0 = p +* (i,(- (p . i)));
A1: len p = n by CARD_1:def 7;
assume A2: i in Seg n ; :: thesis: (Mx2Tran (AxialSymmetry (i,n))) . p = p +* (i,(- (p . i)))
A3: for j being Nat st 1 <= j & j <= n holds
((Mx2Tran (AxialSymmetry (i,n))) . p) . j = (p +* (i,(- (p . i)))) . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= n implies ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = (p +* (i,(- (p . i)))) . j )
assume A4: ( 1 <= j & j <= n ) ; :: thesis: ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = (p +* (i,(- (p . i)))) . j
A5: j in Seg n by A4;
A6: j in dom p by A1, A4, FINSEQ_3:25;
per cases ( j <> i or j = i ) ;
suppose A7: j <> i ; :: thesis: ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = (p +* (i,(- (p . i)))) . j
then (p +* (i,(- (p . i)))) . j = p . j by FUNCT_7:32;
hence ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = (p +* (i,(- (p . i)))) . j by A2, A7, Th8; :: thesis: verum
end;
suppose A8: j = i ; :: thesis: ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = (p +* (i,(- (p . i)))) . j
then (p +* (i,(- (p . i)))) . j = - (p . i) by A6, FUNCT_7:31;
hence ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = (p +* (i,(- (p . i)))) . j by A5, A8, Th9; :: thesis: verum
end;
end;
end;
( len (p +* (i,(- (p . i)))) = len p & len ((Mx2Tran (AxialSymmetry (i,n))) . p) = n ) by CARD_1:def 7, FUNCT_7:97;
hence (Mx2Tran (AxialSymmetry (i,n))) . p = p +* (i,(- (p . i))) by A1, A3; :: thesis: verum