let n be Nat; :: thesis: for K being Field
for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a
let K be Field; :: thesis: for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a
let a be Element of K; :: thesis: (n,n) --> a is_symmetry_circulant_about n |-> a
set p = n |-> a;
set M = (n,n) --> a;
A1: ( width ((n,n) --> a) = n & len (n |-> a) = n ) by CARD_1:def 7, MATRIX_0:24;
hence len (n |-> a) = width ((n,n) --> a) ; :: according to MATRIX17:def 4 :: thesis: ( ( for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j <> (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) ) & ( for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j = (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a)) ) )
A2: Indices ((n,n) --> a) = [:(Seg n),(Seg n):] by MATRIX_0:24;
thus for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j <> (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) :: thesis: for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j = (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((n,n) --> a) & i + j <> (len (n |-> a)) + 1 implies ((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) )
assume that
A3: [i,j] in Indices ((n,n) --> a) and
A4: i + j <> (len (n |-> a)) + 1 ; :: thesis: ((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a)))
((Seg n) --> a) . (((i + j) - 1) mod (len (n |-> a))) = a by A1, A2, A3, A4, Lm4, FUNCOP_1:7;
hence ((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) by A3, MATRIX_0:46; :: thesis: verum

end;

let i, j be Nat; :: thesis: ( [i,j] in Indices ((n,n) --> a) & i + j = (len (n |-> a)) + 1 implies ((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a)) )
assume that
A5: [i,j] in Indices ((n,n) --> a) and
A6: i + j = (len (n |-> a)) + 1 ; :: thesis: ((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a))
( i in Seg n & j in Seg n ) by A2, A5, ZFMISC_1:87;
then ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then 1 + 1 <= i + j by XREAL_1:7;
then ((len (n |-> a)) + 1) - 1 >= (1 + 1) - 1 by A6, XREAL_1:9;
then A7: len (n |-> a) in Seg (len (n |-> a)) ;
((Seg n) --> a) . (len (n |-> a)) = a by A1, A7, FUNCOP_1:7;
hence ((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a)) by A5, MATRIX_0:46; :: thesis: verum