let i, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st i in Seg n holds
(@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = - (p . i)
let p be Point of (TOP-REAL n); :: thesis: ( i in Seg n implies (@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = - (p . i) )
set S = Seg n;
assume A1: i in Seg n ; :: thesis: (@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = - (p . i)
reconsider pI = (@ p) . i as Element of F_Real by XREAL_0:def 1;
set A = AxialSymmetry (i,n);
set C = Col ((AxialSymmetry (i,n)),i);
A2: len (AxialSymmetry (i,n)) = n by MATRIX_0:25;
then A3: dom (AxialSymmetry (i,n)) = Seg n by FINSEQ_1:def 3;
then A4: (Col ((AxialSymmetry (i,n)),i)) . i = (AxialSymmetry (i,n)) * (i,i) by A1, MATRIX_0:def 8;
( len p = n & len (Col ((AxialSymmetry (i,n)),i)) = n ) by A2, CARD_1:def 7;
then len (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) = n by MATRIX_3:6;
then A5: dom (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) = Seg n by FINSEQ_1:def 3;
A6: Indices (AxialSymmetry (i,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A7: for k being Nat st k in dom (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) & k <> i holds
(mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . k = 0. F_Real thus (@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . i by A1, A5, A7, MATRIX_3:12
.= pI * ((AxialSymmetry (i,n)) * (i,i)) by A1, A4, A5, FVSUM_1:60
.= pI * (- (1. F_Real)) by A1, Def2
.= pI * (- 1)
.= - (p . i) ; :: thesis: verum