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

proof

let k be Nat; :: thesis: ( k in dom (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) & k <> i implies (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . k = 0. F_Real )
assume that
A8: k in dom (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) and
A9: k <> i ; :: thesis: (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . k = 0. F_Real
(@ p) . k in REAL by XREAL_0:def 1;
then reconsider pk = (@ p) . k as Element of F_Real ;
A10: [k,i] in Indices (AxialSymmetry (i,n)) by A1, A5, A6, A8, ZFMISC_1:87;
(Col ((AxialSymmetry (i,n)),i)) . k = (AxialSymmetry (i,n)) * (k,i) by A3, A5, A8, MATRIX_0:def 8;
hence (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . k = pk * ((AxialSymmetry (i,n)) * (k,i)) by A8, FVSUM_1:60
.= pk * (0. F_Real) by A1, A9, A10, Def2
.= 0. F_Real ;
:: thesis: verum

end;

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