let i, j, n be Nat; for p being Point of (TOP-REAL n) st i in Seg n & j in Seg n & i <> j holds
(@ p) "*" (Col ((AxialSymmetry (i,n)),j)) = p . j
let p be Point of (TOP-REAL n); ( i in Seg n & j in Seg n & i <> j implies (@ p) "*" (Col ((AxialSymmetry (i,n)),j)) = p . j )
set S = Seg n;
assume that
A1:
i in Seg n
and
A2:
j in Seg n
and
A3:
i <> j
; (@ p) "*" (Col ((AxialSymmetry (i,n)),j)) = p . j
set A = AxialSymmetry (i,n);
set C = Col ((AxialSymmetry (i,n)),j);
A4:
Indices (AxialSymmetry (i,n)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A5:
[j,j] in Indices (AxialSymmetry (i,n))
by A2, ZFMISC_1:87;
A6:
len (AxialSymmetry (i,n)) = n
by MATRIX_0:25;
then A7:
dom (AxialSymmetry (i,n)) = Seg n
by FINSEQ_1:def 3;
len (Col ((AxialSymmetry (i,n)),j)) = n
by A6, MATRIX_0:def 8;
then A8:
dom (Col ((AxialSymmetry (i,n)),j)) = Seg n
by FINSEQ_1:def 3;
A9:
now for m being Nat st m in dom (Col ((AxialSymmetry (i,n)),j)) & m <> j holds
(Col ((AxialSymmetry (i,n)),j)) . m = 0. F_Reallet m be
Nat;
( m in dom (Col ((AxialSymmetry (i,n)),j)) & m <> j implies (Col ((AxialSymmetry (i,n)),j)) . m = 0. F_Real )assume that A10:
m in dom (Col ((AxialSymmetry (i,n)),j))
and A11:
m <> j
;
(Col ((AxialSymmetry (i,n)),j)) . m = 0. F_RealA12:
[m,j] in Indices (AxialSymmetry (i,n))
by A2, A4, A8, A10, ZFMISC_1:87;
thus (Col ((AxialSymmetry (i,n)),j)) . m =
(AxialSymmetry (i,n)) * (
m,
j)
by A7, A8, A10, MATRIX_0:def 8
.=
0. F_Real
by A1, A11, A12, Def2
;
verum end;
len p = n
by CARD_1:def 7;
then A13:
dom p = Seg n
by FINSEQ_1:def 3;
(Col ((AxialSymmetry (i,n)),j)) . j =
(AxialSymmetry (i,n)) * (j,j)
by A2, A7, MATRIX_0:def 8
.=
1. F_Real
by A1, A3, A5, Def2
;
hence p . j =
Sum (mlt ((Col ((AxialSymmetry (i,n)),j)),(@ p)))
by A2, A8, A9, A13, MATRIX_3:17
.=
(@ p) "*" (Col ((AxialSymmetry (i,n)),j))
by FVSUM_1:64
;
verum