:: by Xiquan Liang and Tao Wang

::

:: Received October 23, 2011

:: Copyright (c) 2011-2018 Association of Mizar Users

Lm1: for n, i being Nat st i in Seg n holds

(n + 1) - i in Seg n

proof end;

Lm2: for n, i, j being Nat st [i,j] in [:(Seg n),(Seg n):] holds

( (n + 1) - j in Seg n & (n + 1) - i in Seg n )

proof end;

:: deftheorem Def1 defines subsymmetric MATRIX17:def 1 :

for K being Field

for n being Nat

for M being Matrix of n,K holds

( M is subsymmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds

M * (i,j) = M * (k,l) );

for K being Field

for n being Nat

for M being Matrix of n,K holds

( M is subsymmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds

M * (i,j) = M * (k,l) );

registration

let n be Nat;

let K be Field;

let a be Element of K;

coherence

for b_{1} being Matrix of n,K st b_{1} = (n,n) --> a holds

b_{1} is subsymmetric

end;
let K be Field;

let a be Element of K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

ex b_{1} being Matrix of n,K st b_{1} is subsymmetric

end;
let K be Field;

cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding tabular V110( the carrier of K,n,n) subsymmetric for Matrix of ,;

existence ex b

proof end;

registration

let n be Nat;

let K be Field;

let M be subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = - M holds

b_{1} is subsymmetric

end;
let K be Field;

let M be subsymmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let M1, M2 be subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M1 + M2 holds

b_{1} is subsymmetric

end;
let K be Field;

let M1, M2 be subsymmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let a be Element of K;

let M be subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = a * M holds

b_{1} is subsymmetric

end;
let K be Field;

let a be Element of K;

let M be subsymmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let M1, M2 be subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M1 - M2 holds

b_{1} is subsymmetric
;

end;
let K be Field;

let M1, M2 be subsymmetric Matrix of n,K;

coherence

for b

b

registration

let n be Nat;

let K be Field;

let M be subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M @ holds

b_{1} is subsymmetric

end;
let K be Field;

let M be subsymmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

coherence

for b_{1} being Matrix of n,K st b_{1} is line_circulant holds

b_{1} is subsymmetric

for b_{1} being Matrix of n,K st b_{1} is col_circulant holds

b_{1} is subsymmetric

end;
let K be Field;

coherence

for b

b

proof end;

coherence for b

b

proof end;

:: deftheorem Def2 defines Anti-subsymmetric MATRIX17:def 2 :

for K being Field

for n being Nat

for M being Matrix of n,K holds

( M is Anti-subsymmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds

M * (i,j) = - (M * (k,l)) );

for K being Field

for n being Nat

for M being Matrix of n,K holds

( M is Anti-subsymmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds

M * (i,j) = - (M * (k,l)) );

registration

let n be Nat;

let K be Field;

ex b_{1} being Matrix of n,K st b_{1} is Anti-subsymmetric

end;
let K be Field;

cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding tabular V110( the carrier of K,n,n) Anti-subsymmetric for Matrix of ,;

existence ex b

proof end;

theorem :: MATRIX17:1

for K being Fanoian Field

for n, i, j, k, l being Nat

for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds

M1 * (i,j) = 0. K

for n, i, j, k, l being Nat

for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds

M1 * (i,j) = 0. K

proof end;

registration

let n be Nat;

let K be Field;

let M be Anti-subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = - M holds

b_{1} is Anti-subsymmetric

end;
let K be Field;

let M be Anti-subsymmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let M1, M2 be Anti-subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M1 + M2 holds

b_{1} is Anti-subsymmetric

end;
let K be Field;

let M1, M2 be Anti-subsymmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let a be Element of K;

let M be Anti-subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = a * M holds

b_{1} is Anti-subsymmetric

end;
let K be Field;

let a be Element of K;

let M be Anti-subsymmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let M1, M2 be Anti-subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M1 - M2 holds

b_{1} is Anti-subsymmetric
;

end;
let K be Field;

let M1, M2 be Anti-subsymmetric Matrix of n,K;

coherence

for b

b

registration

let n be Nat;

let K be Field;

let M be Anti-subsymmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M @ holds

b_{1} is Anti-subsymmetric

end;
let K be Field;

let M be Anti-subsymmetric Matrix of n,K;

coherence

for b

b

proof end;

:: deftheorem Def3 defines central_symmetric MATRIX17:def 3 :

for K being Field

for n being Nat

for M being Matrix of n,K holds

( M is central_symmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - i & l = (n + 1) - j holds

M * (i,j) = M * (k,l) );

for K being Field

for n being Nat

for M being Matrix of n,K holds

( M is central_symmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - i & l = (n + 1) - j holds

M * (i,j) = M * (k,l) );

registration

let n be Nat;

let K be Field;

let a be Element of K;

coherence

for b_{1} being Matrix of n,K st b_{1} = (n,n) --> a holds

b_{1} is central_symmetric

end;
let K be Field;

let a be Element of K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

ex b_{1} being Matrix of n,K st b_{1} is central_symmetric

end;
let K be Field;

cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding tabular V110( the carrier of K,n,n) central_symmetric for Matrix of ,;

existence ex b

proof end;

registration

let n be Nat;

let K be Field;

let M be central_symmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = - M holds

b_{1} is central_symmetric

end;
let K be Field;

let M be central_symmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let M1, M2 be central_symmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M1 + M2 holds

b_{1} is central_symmetric

end;
let K be Field;

let M1, M2 be central_symmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let a be Element of K;

let M be central_symmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = a * M holds

b_{1} is central_symmetric

end;
let K be Field;

let a be Element of K;

let M be central_symmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let M1, M2 be central_symmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M1 - M2 holds

b_{1} is central_symmetric
;

end;
let K be Field;

let M1, M2 be central_symmetric Matrix of n,K;

coherence

for b

b

registration

let n be Nat;

let K be Field;

let M be central_symmetric Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M @ holds

b_{1} is central_symmetric

end;
let K be Field;

let M be central_symmetric Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

for b_{1} being Matrix of n,K st b_{1} is symmetric & b_{1} is subsymmetric holds

b_{1} is central_symmetric

end;
let K be Field;

cluster tabular V110( the carrier of K,n,n) symmetric subsymmetric -> central_symmetric for Matrix of ,;

coherence for b

b

proof end;

Lm3: for n, i, j being Nat st i in Seg n & j in Seg n & i + j <> n + 1 holds

((i + j) - 1) mod n in Seg n

proof end;

Lm4: for n, i, j being Nat st [i,j] in [:(Seg n),(Seg n):] & i + j <> n + 1 holds

((i + j) - 1) mod n in Seg n

proof end;

:: deftheorem defines is_symmetry_circulant_about MATRIX17:def 4 :

for K being set

for M being Matrix of K

for p being FinSequence holds

( M is_symmetry_circulant_about p iff ( len p = width M & ( for i, j being Nat st [i,j] in Indices M & i + j <> (len p) + 1 holds

M * (i,j) = p . (((i + j) - 1) mod (len p)) ) & ( for i, j being Nat st [i,j] in Indices M & i + j = (len p) + 1 holds

M * (i,j) = p . (len p) ) ) );

for K being set

for M being Matrix of K

for p being FinSequence holds

( M is_symmetry_circulant_about p iff ( len p = width M & ( for i, j being Nat st [i,j] in Indices M & i + j <> (len p) + 1 holds

M * (i,j) = p . (((i + j) - 1) mod (len p)) ) & ( for i, j being Nat st [i,j] in Indices M & i + j = (len p) + 1 holds

M * (i,j) = p . (len p) ) ) );

theorem Th2: :: MATRIX17:2

for n being Nat

for K being Field

for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a

for K being Field

for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a

proof end;

theorem Th3: :: MATRIX17:3

for n being Nat

for K being Field

for a being Element of K

for p being FinSequence of K

for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds

a * M1 is_symmetry_circulant_about a * p

for K being Field

for a being Element of K

for p being FinSequence of K

for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds

a * M1 is_symmetry_circulant_about a * p

proof end;

theorem Th4: :: MATRIX17:4

for n being Nat

for K being Field

for p being FinSequence of K

for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds

- M1 is_symmetry_circulant_about - p

for K being Field

for p being FinSequence of K

for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds

- M1 is_symmetry_circulant_about - p

proof end;

theorem Th5: :: MATRIX17:5

for n being Nat

for K being Field

for p, q being FinSequence of K

for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds

M1 + M2 is_symmetry_circulant_about p + q

for K being Field

for p, q being FinSequence of K

for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds

M1 + M2 is_symmetry_circulant_about p + q

proof end;

definition

let K be set ;

let M be Matrix of K;

end;
let M be Matrix of K;

attr M is symmetry_circulant means :Def5: :: MATRIX17:def 5

ex p being FinSequence of K st

( len p = width M & M is_symmetry_circulant_about p );

ex p being FinSequence of K st

( len p = width M & M is_symmetry_circulant_about p );

:: deftheorem Def5 defines symmetry_circulant MATRIX17:def 5 :

for K being set

for M being Matrix of K holds

( M is symmetry_circulant iff ex p being FinSequence of K st

( len p = width M & M is_symmetry_circulant_about p ) );

for K being set

for M being Matrix of K holds

( M is symmetry_circulant iff ex p being FinSequence of K st

( len p = width M & M is_symmetry_circulant_about p ) );

definition

let K be non empty set ;

let p be FinSequence of K;

end;
let p be FinSequence of K;

attr p is first-symmetry-of-circulant means :: MATRIX17:def 6

ex M being Matrix of len p,K st M is_symmetry_circulant_about p;

ex M being Matrix of len p,K st M is_symmetry_circulant_about p;

:: deftheorem defines first-symmetry-of-circulant MATRIX17:def 6 :

for K being non empty set

for p being FinSequence of K holds

( p is first-symmetry-of-circulant iff ex M being Matrix of len p,K st M is_symmetry_circulant_about p );

for K being non empty set

for p being FinSequence of K holds

( p is first-symmetry-of-circulant iff ex M being Matrix of len p,K st M is_symmetry_circulant_about p );

definition

let K be non empty set ;

let p be FinSequence of K;

assume A1: p is first-symmetry-of-circulant ;

existence

ex b_{1} being Matrix of len p,K st b_{1} is_symmetry_circulant_about p
by A1;

uniqueness

for b_{1}, b_{2} being Matrix of len p,K st b_{1} is_symmetry_circulant_about p & b_{2} is_symmetry_circulant_about p holds

b_{1} = b_{2}

end;
let p be FinSequence of K;

assume A1: p is first-symmetry-of-circulant ;

existence

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def7 defines SCirc MATRIX17:def 7 :

for K being non empty set

for p being FinSequence of K st p is first-symmetry-of-circulant holds

for b_{3} being Matrix of len p,K holds

( b_{3} = SCirc p iff b_{3} is_symmetry_circulant_about p );

for K being non empty set

for p being FinSequence of K st p is first-symmetry-of-circulant holds

for b

( b

registration

let n be Nat;

let K be Field;

let a be Element of K;

coherence

for b_{1} being Matrix of n,K st b_{1} = (n,n) --> a holds

b_{1} is symmetry_circulant

end;
let K be Field;

let a be Element of K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

ex b_{1} being Matrix of n,K st b_{1} is symmetry_circulant

end;
let K be Field;

cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding tabular V110( the carrier of K,n,n) symmetry_circulant for Matrix of ,;

existence ex b

proof end;

theorem Th6: :: MATRIX17:6

for n being Nat

for D being non empty set

for A being Matrix of n,D

for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds

A @ is_symmetry_circulant_about p

for D being non empty set

for A being Matrix of n,D

for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds

A @ is_symmetry_circulant_about p

proof end;

registration

let n be Nat;

let K be Field;

let a be Element of K;

let M1 be symmetry_circulant Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = a * M1 holds

b_{1} is symmetry_circulant

end;
let K be Field;

let a be Element of K;

let M1 be symmetry_circulant Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let M1, M2 be symmetry_circulant Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M1 + M2 holds

b_{1} is symmetry_circulant

end;
let K be Field;

let M1, M2 be symmetry_circulant Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let M1 be symmetry_circulant Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = - M1 holds

b_{1} is symmetry_circulant

end;
let K be Field;

let M1 be symmetry_circulant Matrix of n,K;

coherence

for b

b

proof end;

registration

let n be Nat;

let K be Field;

let M1, M2 be symmetry_circulant Matrix of n,K;

coherence

for b_{1} being Matrix of n,K st b_{1} = M1 - M2 holds

b_{1} is symmetry_circulant
;

end;
let K be Field;

let M1, M2 be symmetry_circulant Matrix of n,K;

coherence

for b

b

theorem :: MATRIX17:7

for n being Nat

for D being non empty set

for A being Matrix of n,D st A is symmetry_circulant & n > 0 holds

A @ is symmetry_circulant

for D being non empty set

for A being Matrix of n,D st A is symmetry_circulant & n > 0 holds

A @ is symmetry_circulant

proof end;

theorem Th8: :: MATRIX17:8

for K being Field

for p being FinSequence of K st p is first-symmetry-of-circulant holds

- p is first-symmetry-of-circulant

for p being FinSequence of K st p is first-symmetry-of-circulant holds

- p is first-symmetry-of-circulant

proof end;

theorem :: MATRIX17:9

for K being Field

for p being FinSequence of K st p is first-symmetry-of-circulant holds

SCirc (- p) = - (SCirc p)

for p being FinSequence of K st p is first-symmetry-of-circulant holds

SCirc (- p) = - (SCirc p)

proof end;

theorem Th10: :: MATRIX17:10

for K being Field

for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

p + q is first-symmetry-of-circulant

for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

p + q is first-symmetry-of-circulant

proof end;

theorem Th11: :: MATRIX17:11

for K being Field

for p, q being FinSequence of K st len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant holds

SCirc (p + q) = (SCirc p) + (SCirc q)

for p, q being FinSequence of K st len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant holds

SCirc (p + q) = (SCirc p) + (SCirc q)

proof end;

theorem Th12: :: MATRIX17:12

for K being Field

for a being Element of K

for p being FinSequence of K st p is first-symmetry-of-circulant holds

a * p is first-symmetry-of-circulant

for a being Element of K

for p being FinSequence of K st p is first-symmetry-of-circulant holds

a * p is first-symmetry-of-circulant

proof end;

theorem Th13: :: MATRIX17:13

for K being Field

for a being Element of K

for p being FinSequence of K st p is first-symmetry-of-circulant holds

SCirc (a * p) = a * (SCirc p)

for a being Element of K

for p being FinSequence of K st p is first-symmetry-of-circulant holds

SCirc (a * p) = a * (SCirc p)

proof end;

theorem :: MATRIX17:14

for K being Field

for a, b being Element of K

for p being FinSequence of K st p is first-symmetry-of-circulant holds

(a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p)

for a, b being Element of K

for p being FinSequence of K st p is first-symmetry-of-circulant holds

(a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p)

proof end;

theorem :: MATRIX17:15

for K being Field

for a being Element of K

for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

(a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q))

for a being Element of K

for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

(a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q))

proof end;

theorem :: MATRIX17:16

for K being Field

for a, b being Element of K

for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))

for a, b being Element of K

for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))

proof end;

theorem Th17: :: MATRIX17:17

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is symmetry_circulant holds

M1 @ = M1

for K being Field

for M1 being Matrix of n,K st M1 is symmetry_circulant holds

M1 @ = M1

proof end;

registration

let n be Nat;

let K be Field;

coherence

for b_{1} being Matrix of n,K st b_{1} is symmetry_circulant holds

b_{1} is symmetric
by Th17;

end;
let K be Field;

coherence

for b

b