:: Some Basic Properties of Some Special Matrices, Part {III}
:: by Xiquan Liang and Tao Wang
::
:: Received October 23, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


begin

Lm1:  for n, i being Nat st i in Seg n holds
(n + 1) - i in Seg n
proofend;

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 )
proofend;

definition
let K be Field;
let n be Nat;
let M be Matrix of n,K;
attrM is subsymmetric  means :Def1: :: MATRIX17:def 1
 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);
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) );

registration
let n be Nat;
let K be Field;
let a be Element of K;
cluster(n,n) --> a ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular subsymmetric for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st b1 is subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M be subsymmetric Matrix of n,K;
cluster - M ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = - M holds
b1 is subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be subsymmetric Matrix of n,K;
clusterM1 + M2 ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M be subsymmetric Matrix of n,K;
clustera * M ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = a * M holds
b1 is subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be subsymmetric Matrix of n,K;
clusterK287(K,M1,M2) ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M be subsymmetric Matrix of n,K;
clusterM @  ->  subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M @ holds
b1 is subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
cluster line_circulant  ->  subsymmetric for Matrix of n,n, the carrier of K;
coherence
 for b1 being Matrix of n,K st b1 is line_circulant holds
b1 is subsymmetric
proofend;
cluster col_circulant  ->  subsymmetric for Matrix of n,n, the carrier of K;
coherence
 for b1 being Matrix of n,K st b1 is col_circulant holds
b1 is subsymmetric
proofend;
end;

definition
let K be Field;
let n be Nat;
let M be Matrix of n,K;
attrM is Anti-subsymmetric  means :Def2: :: MATRIX17:def 2
 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));
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)) );

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular Anti-subsymmetric for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st b1 is Anti-subsymmetric
proofend;
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
proofend;

registration
let n be Nat;
let K be Field;
let M be Anti-subsymmetric Matrix of n,K;
cluster - M ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = - M holds
b1 is Anti-subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be Anti-subsymmetric Matrix of n,K;
clusterM1 + M2 ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is Anti-subsymmetric
proofend;
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;
clustera * M ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = a * M holds
b1 is Anti-subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be Anti-subsymmetric Matrix of n,K;
clusterK287(K,M1,M2) ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is Anti-subsymmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M be Anti-subsymmetric Matrix of n,K;
clusterM @  ->  Anti-subsymmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M @ holds
b1 is Anti-subsymmetric
proofend;
end;

begin

definition
let K be Field;
let n be Nat;
let M be Matrix of n,K;
attrM is central_symmetric  means :Def3: :: MATRIX17:def 3
 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);
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) );

registration
let n be Nat;
let K be Field;
let a be Element of K;
cluster(n,n) --> a ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is central_symmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular central_symmetric for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st b1 is central_symmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M be central_symmetric Matrix of n,K;
cluster - M ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = - M holds
b1 is central_symmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be central_symmetric Matrix of n,K;
clusterM1 + M2 ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is central_symmetric
proofend;
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;
clustera * M ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = a * M holds
b1 is central_symmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be central_symmetric Matrix of n,K;
clusterK287(K,M1,M2) ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is central_symmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
let M be central_symmetric Matrix of n,K;
clusterM @  ->  central_symmetric for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M @ holds
b1 is central_symmetric
proofend;
end;

registration
let n be Nat;
let K be Field;
cluster symmetric subsymmetric  ->  central_symmetric for Matrix of n,n, the carrier of K;
coherence
 for b1 being Matrix of n,K st b1 is symmetric & b1 is subsymmetric holds
b1 is central_symmetric
proofend;
end;

begin

Lm3:  for n, i, j being Nat st i in Seg n &amp; j in Seg n &amp; i + j <> n + 1 holds
((i + j) - 1) mod n in Seg n
proofend;

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

definition
let K be set ;
let M be Matrix of K;
let p be FinSequence;
predM is_symmetry_circulant_about p means :Def4: :: MATRIX17:def 4
( len p = width M &amp; ( for i, j being Nat st [i,j] in Indices M &amp; i + j <> (len p) + 1 holds
M * (i,j) = p . (((i + j) - 1) mod (len p)) ) &amp; ( for i, j being Nat st [i,j] in Indices M &amp; i + j = (len p) + 1 holds
M * (i,j) = p . (len p) ) );
end;

:: deftheorem Def4 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 &amp; ( for i, j being Nat st [i,j] in Indices M &amp; i + j <> (len p) + 1 holds
M * (i,j) = p . (((i + j) - 1) mod (len p)) ) &amp; ( for i, j being Nat st [i,j] in Indices M &amp; i + j = (len p) + 1 holds
M * (i,j) = p . (len p) ) ) );

theorem T1: :: 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
proofend;

theorem T2: :: 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
proofend;

theorem T4: :: 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
proofend;

theorem T3: :: 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 &amp; M2 is_symmetry_circulant_about q holds
M1 + M2 is_symmetry_circulant_about p + q
proofend;

definition
let K be set ;
let M be Matrix of K;
attrM is symmetry_circulant  means :Def5: :: MATRIX17:def 5
 ex p being FinSequence of K st
( len p = width M &amp; M is_symmetry_circulant_about p );
end;

:: 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 &amp; M is_symmetry_circulant_about p ) );

definition
let K be non empty set ;
let p be FinSequence of K;
attrp is first-symmetry-of-circulant  means :Def6: :: MATRIX17:def 6
 ex M being Matrix of len p,K st M is_symmetry_circulant_about p;
end;

:: deftheorem Def6 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 );

definition
let K be non empty set ;
let p be FinSequence of K;
assume A1: p is first-symmetry-of-circulant ;
func SCirc p ->  Matrix of len p,K means :Def7: :: MATRIX17:def 7
it is_symmetry_circulant_about p;
existence
 ex b1 being Matrix of len p,K st b1 is_symmetry_circulant_about p by A1, Def6;
uniqueness
 for b1, b2 being Matrix of len p,K st b1 is_symmetry_circulant_about p &amp; b2 is_symmetry_circulant_about p holds
b1 = b2
proofend;
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 b3 being Matrix of len p,K holds
( b3 = SCirc p iff b3 is_symmetry_circulant_about p );

registration
let n be Nat;
let K be Field;
let a be Element of K;
cluster(n,n) --> a ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is symmetry_circulant
proofend;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular symmetry_circulant for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st b1 is symmetry_circulant
proofend;
end;

theorem T5: :: 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 &amp; A is_symmetry_circulant_about p holds
A @ is_symmetry_circulant_about p
proofend;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M1 be symmetry_circulant Matrix of n,K;
clustera * M1 ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = a * M1 holds
b1 is symmetry_circulant
proofend;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be symmetry_circulant Matrix of n,K;
clusterM1 + M2 ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is symmetry_circulant
proofend;
end;

registration
let n be Nat;
let K be Field;
let M1 be symmetry_circulant Matrix of n,K;
cluster - M1 ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = - M1 holds
b1 is symmetry_circulant
proofend;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be symmetry_circulant Matrix of n,K;
clusterK287(K,M1,M2) ->  symmetry_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is symmetry_circulant
proofend;
end;

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 &amp; n > 0 holds
A @ is symmetry_circulant
proofend;

theorem Th4: :: 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
proofend;

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)
proofend;

theorem Th6: :: MATRIX17:10
for K being Field
for p, q being FinSequence of K st p is first-symmetry-of-circulant &amp; q is first-symmetry-of-circulant &amp; len p = len q holds
p + q is first-symmetry-of-circulant
proofend;

theorem Th7: :: MATRIX17:11
for K being Field
for p, q being FinSequence of K st len p = len q &amp; p is first-symmetry-of-circulant &amp; q is first-symmetry-of-circulant holds
SCirc (p + q) = (SCirc p) + (SCirc q)
proofend;

theorem Th8: :: 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
proofend;

theorem Th9: :: 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)
proofend;

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)
proofend;

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 &amp; q is first-symmetry-of-circulant &amp; len p = len q holds
(a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q))
proofend;

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 &amp; q is first-symmetry-of-circulant &amp; len p = len q holds
(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))
proofend;

theorem Th13: :: 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
proofend;

registration
let n be Nat;
let K be Field;
cluster symmetry_circulant  ->  symmetric for Matrix of n,n, the carrier of K;
coherence
 for b1 being Matrix of n,K st b1 is symmetry_circulant holds
b1 is symmetric
proofend;
end;