:: MATRIX16 semantic presentation
begin
Lm1: for n being Element of NAT
for k being Nat st k <= n & k >= 1 holds
(k - 1) mod n = k - 1
proof
let n be Element of NAT ; ::_thesis: for k being Nat st k <= n & k >= 1 holds
(k - 1) mod n = k - 1
let k be Nat; ::_thesis: ( k <= n & k >= 1 implies (k - 1) mod n = k - 1 )
assume that
A1: k <= n and
A2: k >= 1 ; ::_thesis: (k - 1) mod n = k - 1
A3: k - 1 >= 1 - 1 by A2, XREAL_1:9;
A4: n - 1 < n by XREAL_1:44;
k - 1 <= n - 1 by A1, XREAL_1:9;
then k - 1 < n by A4, XXREAL_0:2;
hence (k - 1) mod n = k - 1 by A3, NAT_D:63; ::_thesis: verum
end;
Lm2: for n, i, j being Nat st i in Seg n & j in Seg n holds
((j - i) mod n) + 1 in Seg n
proof
let n, i, j be Nat; ::_thesis: ( i in Seg n & j in Seg n implies ((j - i) mod n) + 1 in Seg n )
assume that
A1: i in Seg n and
A2: j in Seg n ; ::_thesis: ((j - i) mod n) + 1 in Seg n
( i <= n & 1 <= j ) by A1, A2, FINSEQ_1:1;
then A3: 1 - n <= j - i by XREAL_1:13;
( 1 <= i & j <= n ) by A1, A2, FINSEQ_1:1;
then A4: j - i <= n - 1 by XREAL_1:13;
- n <= (- n) + 1 by XREAL_1:29;
then A5: - n <= j - i by A3, XXREAL_0:2;
n - 1 < n by XREAL_1:44;
then A6: j - i < n by A4, XXREAL_0:2;
(j - i) mod n <= n - 1
proof
percases ( 0 <= j - i or 0 > j - i ) ;
suppose 0 <= j - i ; ::_thesis: (j - i) mod n <= n - 1
hence (j - i) mod n <= n - 1 by A4, A6, NAT_D:63; ::_thesis: verum
end;
supposeA7: 0 > j - i ; ::_thesis: (j - i) mod n <= n - 1
then j - i <= - 1 by INT_1:8;
then n + (j - i) <= n + (- 1) by XREAL_1:6;
hence (j - i) mod n <= n - 1 by A5, A7, NAT_D:63; ::_thesis: verum
end;
end;
end;
then A8: ((j - i) mod n) + 1 <= (n - 1) + 1 by XREAL_1:6;
n in NAT by ORDINAL1:def_12;
then n > 0 by A1, FINTOPO5:2;
then (j - i) mod n >= 0 by NAT_D:62;
then ( ((j - i) mod n) + 1 >= 0 + 1 & ((j - i) mod n) + 1 in NAT ) by INT_1:3, XREAL_1:6;
hence ((j - i) mod n) + 1 in Seg n by A8; ::_thesis: verum
end;
Lm3: for n, i, j being Nat st ( [i,j] in [:(Seg n),(Seg n):] or [j,i] in [:(Seg n),(Seg n):] ) holds
((j - i) mod n) + 1 in Seg n
proof
let n, i, j be Nat; ::_thesis: ( ( [i,j] in [:(Seg n),(Seg n):] or [j,i] in [:(Seg n),(Seg n):] ) implies ((j - i) mod n) + 1 in Seg n )
assume ( [i,j] in [:(Seg n),(Seg n):] or [j,i] in [:(Seg n),(Seg n):] ) ; ::_thesis: ((j - i) mod n) + 1 in Seg n
then ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
hence ((j - i) mod n) + 1 in Seg n by Lm2; ::_thesis: verum
end;
theorem :: MATRIX16:1
for K being Field
for p being FinSequence of K holds (1_ K) * p = p
proof
let K be Field; ::_thesis: for p being FinSequence of K holds (1_ K) * p = p
let p be FinSequence of K; ::_thesis: (1_ K) * p = p
A1: dom p = Seg (len p) by FINSEQ_1:def_3;
A2: ( Seg (len ((1_ K) * p)) = Seg (len p) & dom ((1_ K) * p) = Seg (len ((1_ K) * p)) ) by FINSEQ_1:def_3, MATRIXR1:16;
for i being Nat st i in dom p holds
((1_ K) * p) . i = p . i
proof
let i be Nat; ::_thesis: ( i in dom p implies ((1_ K) * p) . i = p . i )
A3: rng p c= the carrier of K by FINSEQ_1:def_4;
assume A4: i in dom p ; ::_thesis: ((1_ K) * p) . i = p . i
then A5: p . i in dom ( the multF of K [;] ((1_ K),(id the carrier of K))) by A2, A1, FUNCT_1:11;
p . i in rng p by A4, FUNCT_1:3;
then reconsider b = p . i as Element of K by A3;
((1_ K) * p) . i = ((1_ K) multfield) . (p . i) by A4, FUNCT_1:13
.= the multF of K . ((1_ K),((id the carrier of K) . (p . i))) by A5, FUNCOP_1:32
.= (1_ K) * b by FUNCT_1:18
.= p . i by VECTSP_1:def_8 ;
hence ((1_ K) * p) . i = p . i ; ::_thesis: verum
end;
hence (1_ K) * p = p by A2, A1, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: MATRIX16:2
for K being Field
for p being FinSequence of K holds (- (1_ K)) * p = - p
proof
let K be Field; ::_thesis: for p being FinSequence of K holds (- (1_ K)) * p = - p
let p be FinSequence of K; ::_thesis: (- (1_ K)) * p = - p
A1: ( Seg (len ((- (1_ K)) * p)) = Seg (len p) & dom ((- (1_ K)) * p) = Seg (len ((- (1_ K)) * p)) ) by FINSEQ_1:def_3, MATRIXR1:16;
A2: dom p = Seg (len p) by FINSEQ_1:def_3;
A3: for i being Nat st i in dom p holds
((- (1_ K)) * p) . i = (- p) . i
proof
let i be Nat; ::_thesis: ( i in dom p implies ((- (1_ K)) * p) . i = (- p) . i )
A4: rng p c= the carrier of K by FINSEQ_1:def_4;
assume A5: i in dom p ; ::_thesis: ((- (1_ K)) * p) . i = (- p) . i
then A6: p . i in dom ( the multF of K [;] ((- (1_ K)),(id the carrier of K))) by A1, A2, FUNCT_1:11;
p . i in rng p by A5, FUNCT_1:3;
then reconsider b = p . i as Element of K by A4;
((- (1_ K)) * b) + b = ((- (1_ K)) * b) + ((1_ K) * b) by VECTSP_1:def_8
.= ((- (1_ K)) + (1_ K)) * b by VECTSP_1:def_7
.= (0. K) * b by RLVECT_1:5
.= 0. K by VECTSP_1:7 ;
then ((- (1_ K)) * b) + (b + (- b)) = (0. K) + (- b) by RLVECT_1:def_3;
then (0. K) + (- b) = ((- (1_ K)) * b) + (0. K) by RLVECT_1:5
.= (- (1_ K)) * b by RLVECT_1:4 ;
then A7: (- (1_ K)) * b = - b by RLVECT_1:4;
((- (1_ K)) * p) . i = ((- (1_ K)) multfield) . (p . i) by A5, FUNCT_1:13
.= the multF of K . ((- (1_ K)),((id the carrier of K) . (p . i))) by A6, FUNCOP_1:32
.= the multF of K . ((- (1_ K)),b) by FUNCT_1:18
.= (comp K) . b by A7, VECTSP_1:def_13
.= (- p) . i by A5, FUNCT_1:13 ;
hence ((- (1_ K)) * p) . i = (- p) . i ; ::_thesis: verum
end;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A8: len (- p) = len p by CARD_1:def_7;
( dom (- p) = Seg (len (- p)) & dom p = Seg (len p) ) by FINSEQ_1:def_3;
hence (- (1_ K)) * p = - p by A1, A3, A8, FINSEQ_1:13; ::_thesis: verum
end;
definition
let K be set ;
let M be Matrix of K;
let p be FinSequence;
predM is_line_circulant_about p means :Def1: :: MATRIX16:def 1
( len p = width M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((j - i) mod (len p)) + 1) ) );
end;
:: deftheorem Def1 defines is_line_circulant_about MATRIX16:def_1_:_
for K being set
for M being Matrix of K
for p being FinSequence holds
( M is_line_circulant_about p iff ( len p = width M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((j - i) mod (len p)) + 1) ) ) );
definition
let K be set ;
let M be Matrix of K;
attrM is line_circulant means :Def2: :: MATRIX16:def 2
ex p being FinSequence of K st
( len p = width M & M is_line_circulant_about p );
end;
:: deftheorem Def2 defines line_circulant MATRIX16:def_2_:_
for K being set
for M being Matrix of K holds
( M is line_circulant iff ex p being FinSequence of K st
( len p = width M & M is_line_circulant_about p ) );
definition
let K be non empty set ;
let p be FinSequence of K;
attrp is first-line-of-circulant means :Def3: :: MATRIX16:def 3
ex M being Matrix of len p,K st M is_line_circulant_about p;
end;
:: deftheorem Def3 defines first-line-of-circulant MATRIX16:def_3_:_
for K being non empty set
for p being FinSequence of K holds
( p is first-line-of-circulant iff ex M being Matrix of len p,K st M is_line_circulant_about p );
definition
let K be set ;
let M be Matrix of K;
let p be FinSequence;
predM is_col_circulant_about p means :Def4: :: MATRIX16:def 4
( len p = len M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((i - j) mod (len p)) + 1) ) );
end;
:: deftheorem Def4 defines is_col_circulant_about MATRIX16:def_4_:_
for K being set
for M being Matrix of K
for p being FinSequence holds
( M is_col_circulant_about p iff ( len p = len M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((i - j) mod (len p)) + 1) ) ) );
definition
let K be set ;
let M be Matrix of K;
attrM is col_circulant means :Def5: :: MATRIX16:def 5
ex p being FinSequence of K st
( len p = len M & M is_col_circulant_about p );
end;
:: deftheorem Def5 defines col_circulant MATRIX16:def_5_:_
for K being set
for M being Matrix of K holds
( M is col_circulant iff ex p being FinSequence of K st
( len p = len M & M is_col_circulant_about p ) );
definition
let K be non empty set ;
let p be FinSequence of K;
attrp is first-col-of-circulant means :Def6: :: MATRIX16:def 6
ex M being Matrix of len p,K st M is_col_circulant_about p;
end;
:: deftheorem Def6 defines first-col-of-circulant MATRIX16:def_6_:_
for K being non empty set
for p being FinSequence of K holds
( p is first-col-of-circulant iff ex M being Matrix of len p,K st M is_col_circulant_about p );
definition
let K be non empty set ;
let p be FinSequence of K;
assume A1: p is first-line-of-circulant ;
func LCirc p -> Matrix of len p,K means :Def7: :: MATRIX16:def 7
it is_line_circulant_about p;
existence
ex b1 being Matrix of len p,K st b1 is_line_circulant_about p by A1, Def3;
uniqueness
for b1, b2 being Matrix of len p,K st b1 is_line_circulant_about p & b2 is_line_circulant_about p holds
b1 = b2
proof
let M1, M2 be Matrix of len p,K; ::_thesis: ( M1 is_line_circulant_about p & M2 is_line_circulant_about p implies M1 = M2 )
assume that
A2: M1 is_line_circulant_about p and
A3: M2 is_line_circulant_about p ; ::_thesis: M1 = M2
A4: Indices M1 = Indices M2 by MATRIX_1:26;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A5: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then M1 * (i,j) = p . (((j - i) mod (len p)) + 1) by A2, Def1;
hence M1 * (i,j) = M2 * (i,j) by A3, A4, A5, Def1; ::_thesis: verum
end;
hence M1 = M2 by MATRIX_1:27; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines LCirc MATRIX16:def_7_:_
for K being non empty set
for p being FinSequence of K st p is first-line-of-circulant holds
for b3 being Matrix of len p,K holds
( b3 = LCirc p iff b3 is_line_circulant_about p );
definition
let K be non empty set ;
let p be FinSequence of K;
assume A1: p is first-col-of-circulant ;
func CCirc p -> Matrix of len p,K means :Def8: :: MATRIX16:def 8
it is_col_circulant_about p;
existence
ex b1 being Matrix of len p,K st b1 is_col_circulant_about p by A1, Def6;
uniqueness
for b1, b2 being Matrix of len p,K st b1 is_col_circulant_about p & b2 is_col_circulant_about p holds
b1 = b2
proof
let M1, M2 be Matrix of len p,K; ::_thesis: ( M1 is_col_circulant_about p & M2 is_col_circulant_about p implies M1 = M2 )
assume that
A2: M1 is_col_circulant_about p and
A3: M2 is_col_circulant_about p ; ::_thesis: M1 = M2
A4: Indices M1 = Indices M2 by MATRIX_1:26;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A5: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then M1 * (i,j) = p . (((i - j) mod (len p)) + 1) by A2, Def4;
hence M1 * (i,j) = M2 * (i,j) by A3, A4, A5, Def4; ::_thesis: verum
end;
hence M1 = M2 by MATRIX_1:27; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines CCirc MATRIX16:def_8_:_
for K being non empty set
for p being FinSequence of K st p is first-col-of-circulant holds
for b3 being Matrix of len p,K holds
( b3 = CCirc p iff b3 is_col_circulant_about p );
registration
let K be Field;
cluster Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like first-line-of-circulant first-col-of-circulant for FinSequence of the carrier of K;
existence
ex b1 being FinSequence of K st
( b1 is first-line-of-circulant & b1 is first-col-of-circulant )
proof
A1: 0. (K,1,1) = 1 |-> (1 |-> (0. K)) ;
set M1 = 0. (K,1);
take p = 1 |-> (0. K); ::_thesis: ( p is first-line-of-circulant & p is first-col-of-circulant )
A2: len (1 |-> (0. K)) = 1 by CARD_1:def_7;
A3: Indices (0. (K,1)) = [:(Seg 1),(Seg 1):] by MATRIX_1:24;
A4: for i, j being Nat st [i,j] in Indices (0. (K,1)) holds
(0. (K,1)) * (i,j) = p . (((i - j) mod (len p)) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (0. (K,1)) implies (0. (K,1)) * (i,j) = p . (((i - j) mod (len p)) + 1) )
assume A5: [i,j] in Indices (0. (K,1)) ; ::_thesis: (0. (K,1)) * (i,j) = p . (((i - j) mod (len p)) + 1)
then ((i - j) mod 1) + 1 in Seg 1 by A3, Lm3;
then ((Seg 1) --> (0. K)) . (((i - j) mod 1) + 1) = 0. K by FUNCOP_1:7;
hence (0. (K,1)) * (i,j) = p . (((i - j) mod (len p)) + 1) by A2, A1, A5, MATRIX_3:1; ::_thesis: verum
end;
A6: for i, j being Nat st [i,j] in Indices (0. (K,1)) holds
(0. (K,1)) * (i,j) = p . (((j - i) mod (len p)) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (0. (K,1)) implies (0. (K,1)) * (i,j) = p . (((j - i) mod (len p)) + 1) )
assume A7: [i,j] in Indices (0. (K,1)) ; ::_thesis: (0. (K,1)) * (i,j) = p . (((j - i) mod (len p)) + 1)
then ((j - i) mod 1) + 1 in Seg 1 by A3, Lm3;
then ((Seg 1) --> (0. K)) . (((j - i) mod 1) + 1) = 0. K by FUNCOP_1:7;
hence (0. (K,1)) * (i,j) = p . (((j - i) mod (len p)) + 1) by A2, A1, A7, MATRIX_3:1; ::_thesis: verum
end;
width (0. (K,1)) = 1 by MATRIX_1:24;
then 0. (K,1) is_line_circulant_about p by A2, A6, Def1;
hence p is first-line-of-circulant by A2, Def3; ::_thesis: p is first-col-of-circulant
len (0. (K,1)) = 1 by MATRIX_1:24;
then 0. (K,1) is_col_circulant_about p by A2, A4, Def4;
hence p is first-col-of-circulant by A2, Def6; ::_thesis: verum
end;
end;
registration
let K be Field;
let n be Element of NAT ;
cluster 0. (K,n) -> line_circulant col_circulant ;
coherence
( 0. (K,n) is line_circulant & 0. (K,n) is col_circulant )
proof
set p = n |-> (0. K);
A1: len (0. (K,n)) = n by MATRIX_1:24;
A2: 0. (K,n,n) = n |-> (n |-> (0. K)) ;
set M1 = 0. (K,n);
A3: len (n |-> (0. K)) = n by CARD_1:def_7;
A4: Indices (0. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (0. (K,n)) implies (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) )
assume A5: [i,j] in Indices (0. (K,n)) ; ::_thesis: (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1)
then ((i - j) mod n) + 1 in Seg n by A4, Lm3;
then ((i - j) mod (len (n |-> (0. K)))) + 1 in Seg n by CARD_1:def_7;
then ((Seg n) --> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) = 0. K by FUNCOP_1:7;
hence (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) by A2, A5, MATRIX_3:1; ::_thesis: verum
end;
then A6: 0. (K,n) is_col_circulant_about n |-> (0. K) by A1, A3, Def4;
A7: width (0. (K,n)) = n by MATRIX_1:24;
thus 0. (K,n) is line_circulant ::_thesis: 0. (K,n) is col_circulant
proof
for i, j being Nat st [i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (0. (K,n)) implies (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) )
assume A8: [i,j] in Indices (0. (K,n)) ; ::_thesis: (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)
then ((j - i) mod n) + 1 in Seg n by A4, Lm3;
then ((Seg n) --> (0. K)) . (((j - i) mod n) + 1) = 0. K by FUNCOP_1:7;
hence (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) by A3, A2, A8, MATRIX_3:1; ::_thesis: verum
end;
then 0. (K,n) is_line_circulant_about n |-> (0. K) by A7, A3, Def1;
then consider p being FinSequence of K such that
A9: ( len p = width (0. (K,n)) & 0. (K,n) is_line_circulant_about p ) by A7, A3;
take p ; :: according to MATRIX16:def_2 ::_thesis: ( len p = width (0. (K,n)) & 0. (K,n) is_line_circulant_about p )
thus ( len p = width (0. (K,n)) & 0. (K,n) is_line_circulant_about p ) by A9; ::_thesis: verum
end;
consider p being FinSequence of K such that
A10: ( len p = len (0. (K,n)) & 0. (K,n) is_col_circulant_about p ) by A1, A3, A6;
take p ; :: according to MATRIX16:def_5 ::_thesis: ( len p = len (0. (K,n)) & 0. (K,n) is_col_circulant_about p )
thus ( len p = len (0. (K,n)) & 0. (K,n) is_col_circulant_about p ) by A10; ::_thesis: verum
end;
end;
registration
let K be Field;
let n be Element of NAT ;
let a be Element of K;
cluster(n,n) --> a -> line_circulant for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is line_circulant
proof
set p = n |-> a;
A1: ( width ((n,n) --> a) = n & len (n |-> a) = n ) by CARD_1:def_7, MATRIX_1:24;
A2: Indices ((n,n) --> a) = [:(Seg n),(Seg n):] by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices ((n,n) --> a) holds
((n,n) --> a) * (i,j) = (n |-> a) . (((j - i) mod (len (n |-> a))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((n,n) --> a) implies ((n,n) --> a) * (i,j) = (n |-> a) . (((j - i) mod (len (n |-> a))) + 1) )
assume A3: [i,j] in Indices ((n,n) --> a) ; ::_thesis: ((n,n) --> a) * (i,j) = (n |-> a) . (((j - i) mod (len (n |-> a))) + 1)
then ((j - i) mod n) + 1 in Seg n by A2, Lm3;
then ((j - i) mod (len (n |-> a))) + 1 in Seg n by CARD_1:def_7;
then ((Seg n) --> a) . (((j - i) mod (len (n |-> a))) + 1) = a by FUNCOP_1:7;
hence ((n,n) --> a) * (i,j) = (n |-> a) . (((j - i) mod (len (n |-> a))) + 1) by A3, MATRIX_2:1; ::_thesis: verum
end;
then (n,n) --> a is_line_circulant_about n |-> a by A1, Def1;
hence for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is line_circulant by A1, Def2; ::_thesis: verum
end;
cluster(n,n) --> a -> col_circulant for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is col_circulant
proof
set M1 = (n,n) --> a;
set p = n |-> a;
A4: ( len ((n,n) --> a) = n & len (n |-> a) = n ) by CARD_1:def_7, MATRIX_1:24;
A5: Indices ((n,n) --> a) = [:(Seg n),(Seg n):] by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices ((n,n) --> a) holds
((n,n) --> a) * (i,j) = (n |-> a) . (((i - j) mod (len (n |-> a))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((n,n) --> a) implies ((n,n) --> a) * (i,j) = (n |-> a) . (((i - j) mod (len (n |-> a))) + 1) )
assume A6: [i,j] in Indices ((n,n) --> a) ; ::_thesis: ((n,n) --> a) * (i,j) = (n |-> a) . (((i - j) mod (len (n |-> a))) + 1)
then ((i - j) mod n) + 1 in Seg n by A5, Lm3;
then ((i - j) mod (len (n |-> a))) + 1 in Seg n by CARD_1:def_7;
then ((Seg n) --> a) . (((i - j) mod (len (n |-> a))) + 1) = a by FUNCOP_1:7;
hence ((n,n) --> a) * (i,j) = (n |-> a) . (((i - j) mod (len (n |-> a))) + 1) by A6, MATRIX_2:1; ::_thesis: verum
end;
then (n,n) --> a is_col_circulant_about n |-> a by A4, Def4;
hence for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is col_circulant by A4, Def5; ::_thesis: verum
end;
end;
registration
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular line_circulant col_circulant for FinSequence of the carrier of K * ;
existence
ex b1 being Matrix of K st
( b1 is line_circulant & b1 is col_circulant )
proof
take (1,1) --> (0. K) ; ::_thesis: ( (1,1) --> (0. K) is line_circulant & (1,1) --> (0. K) is col_circulant )
thus ( (1,1) --> (0. K) is line_circulant & (1,1) --> (0. K) is col_circulant ) ; ::_thesis: verum
end;
end;
theorem :: MATRIX16:3
for n being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is line_circulant & n > 0 holds
A @ is col_circulant
proof
let n be Element of NAT ; ::_thesis: for D being non empty set
for A being Matrix of n,D st A is line_circulant & n > 0 holds
A @ is col_circulant
let D be non empty set ; ::_thesis: for A being Matrix of n,D st A is line_circulant & n > 0 holds
A @ is col_circulant
let A be Matrix of n,D; ::_thesis: ( A is line_circulant & n > 0 implies A @ is col_circulant )
assume that
A1: A is line_circulant and
A2: n > 0 ; ::_thesis: A @ is col_circulant
consider p being FinSequence of D such that
A3: len p = width A and
A4: A is_line_circulant_about p by A1, Def2;
width A = n by MATRIX_1:24;
then A5: len (A @) = len p by A2, A3, MATRIX_2:10;
for i, j being Nat st [i,j] in Indices (A @) holds
(A @) * (i,j) = p . (((i - j) mod (len p)) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A @) implies (A @) * (i,j) = p . (((i - j) mod (len p)) + 1) )
A6: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume [i,j] in Indices (A @) ; ::_thesis: (A @) * (i,j) = p . (((i - j) mod (len p)) + 1)
then [i,j] in Indices A by MATRIX_1:26;
then ( i in Seg n & j in Seg n ) by A6, ZFMISC_1:87;
then A7: [j,i] in Indices A by A6, ZFMISC_1:87;
then (A @) * (i,j) = A * (j,i) by MATRIX_1:def_6;
hence (A @) * (i,j) = p . (((i - j) mod (len p)) + 1) by A4, A7, Def1; ::_thesis: verum
end;
then A @ is_col_circulant_about p by A5, Def4;
then consider p being FinSequence of D such that
A8: ( len p = len (A @) & A @ is_col_circulant_about p ) by A5;
take p ; :: according to MATRIX16:def_5 ::_thesis: ( len p = len (A @) & A @ is_col_circulant_about p )
thus ( len p = len (A @) & A @ is_col_circulant_about p ) by A8; ::_thesis: verum
end;
theorem :: MATRIX16:4
for n being Element of NAT
for D being non empty set
for t being FinSequence of D
for A being Matrix of n,D st A is_line_circulant_about t & n > 0 holds
t = Line (A,1)
proof
let n be Element of NAT ; ::_thesis: for D being non empty set
for t being FinSequence of D
for A being Matrix of n,D st A is_line_circulant_about t & n > 0 holds
t = Line (A,1)
let D be non empty set ; ::_thesis: for t being FinSequence of D
for A being Matrix of n,D st A is_line_circulant_about t & n > 0 holds
t = Line (A,1)
let t be FinSequence of D; ::_thesis: for A being Matrix of n,D st A is_line_circulant_about t & n > 0 holds
t = Line (A,1)
let A be Matrix of n,D; ::_thesis: ( A is_line_circulant_about t & n > 0 implies t = Line (A,1) )
assume that
A1: A is_line_circulant_about t and
A2: n > 0 ; ::_thesis: t = Line (A,1)
A3: width A = n by MATRIX_1:24;
then A4: ( dom t = Seg (len t) & len t = n ) by A1, Def1, FINSEQ_1:def_3;
A5: for k being Nat st k in dom t holds
t . k = (Line (A,1)) . k
proof
let k be Nat; ::_thesis: ( k in dom t implies t . k = (Line (A,1)) . k )
assume A6: k in dom t ; ::_thesis: t . k = (Line (A,1)) . k
then A7: ( 1 <= k & k <= n ) by A4, FINSEQ_1:1;
n >= 0 + 1 by A2, INT_1:7;
then 1 in Seg n ;
then [1,k] in [:(Seg n),(Seg n):] by A4, A6, ZFMISC_1:def_2;
then A8: [1,k] in Indices A by MATRIX_1:24;
(Line (A,1)) . k = A * (1,k) by A3, A4, A6, MATRIX_1:def_7
.= t . (((k - 1) mod (len t)) + 1) by A1, A8, Def1
.= t . (((k - 1) mod n) + 1) by A1, A3, Def1
.= t . ((k - 1) + 1) by A7, Lm1 ;
hence t . k = (Line (A,1)) . k ; ::_thesis: verum
end;
len (Line (A,1)) = n by A3, MATRIX_1:def_7;
then dom (Line (A,1)) = dom t by A4, FINSEQ_1:def_3;
hence t = Line (A,1) by A5, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: MATRIX16:5
for i, j, n, k, l being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is line_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
proof
let i, j, n, k, l be Element of NAT ; ::_thesis: for D being non empty set
for A being Matrix of n,D st A is line_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
let D be non empty set ; ::_thesis: for A being Matrix of n,D st A is line_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
let A be Matrix of n,D; ::_thesis: ( A is line_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies A * (i,j) = A * (k,l) )
assume that
A1: A is line_circulant and
A2: [i,j] in [:(Seg n),(Seg n):] and
A3: k = i + 1 and
A4: l = j + 1 and
A5: i < n and
A6: j < n ; ::_thesis: A * (i,j) = A * (k,l)
consider p being FinSequence of D such that
len p = width A and
A7: A is_line_circulant_about p by A1, Def2;
A8: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
j in Seg n by A2, ZFMISC_1:87;
then 1 <= j by FINSEQ_1:1;
then 1 + 1 <= j + 1 by XREAL_1:6;
then A9: 1 <= j + 1 by XXREAL_0:2;
j + 1 <= n by A6, INT_1:7;
then A10: l in Seg n by A4, A9;
i in Seg n by A2, ZFMISC_1:87;
then 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A11: 1 <= i + 1 by XXREAL_0:2;
i + 1 <= n by A5, INT_1:7;
then k in Seg n by A3, A11;
then [k,l] in Indices A by A8, A10, ZFMISC_1:87;
then A * (k,l) = p . (((l - k) mod (len p)) + 1) by A7, Def1
.= p . (((j - i) mod (len p)) + 1) by A3, A4
.= A * (i,j) by A2, A7, A8, Def1 ;
hence A * (i,j) = A * (k,l) ; ::_thesis: verum
end;
theorem Th6: :: MATRIX16:6
for n being Element of NAT
for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is line_circulant holds
a * M1 is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is line_circulant holds
a * M1 is line_circulant
let K be Field; ::_thesis: for a being Element of K
for M1 being Matrix of n,K st M1 is line_circulant holds
a * M1 is line_circulant
let a be Element of K; ::_thesis: for M1 being Matrix of n,K st M1 is line_circulant holds
a * M1 is line_circulant
let M1 be Matrix of n,K; ::_thesis: ( M1 is line_circulant implies a * M1 is line_circulant )
A1: Indices (a * M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume M1 is line_circulant ; ::_thesis: a * M1 is line_circulant
then consider p being FinSequence of K such that
A2: len p = width M1 and
A3: M1 is_line_circulant_about p by Def2;
A4: width M1 = n by MATRIX_1:24;
then A5: dom p = Seg n by A2, FINSEQ_1:def_3;
A6: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
A7: for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) )
assume A8: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
then A9: ((j - i) mod n) + 1 in Seg n by A1, Lm3;
then A10: ((j - i) mod (len p)) + 1 in dom (a * p) by A2, A4, A6, MATRIXR1:16;
A11: [i,j] in Indices M1 by A1, A8, MATRIX_1:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (((j - i) mod (len p)) + 1)) by A3, A11, Def1
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by A2, A4, A5, A9, PARTFUN1:def_6
.= a * (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * p) /. (((j - i) mod (len p)) + 1) by A2, A4, A5, A9, POLYNOM1:def_1
.= (a * p) . (((j - i) mod (len p)) + 1) by A10, PARTFUN1:def_6 ;
hence (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; ::_thesis: verum
end;
A12: ( width (a * M1) = n & len (a * p) = len p ) by MATRIXR1:16, MATRIX_1:24;
len p = n by A2, MATRIX_1:24;
then a * M1 is_line_circulant_about a * p by A12, A7, Def1;
then consider q being FinSequence of K such that
A13: ( len q = width (a * M1) & a * M1 is_line_circulant_about q ) by A2, A12, MATRIX_1:24;
take q ; :: according to MATRIX16:def_2 ::_thesis: ( len q = width (a * M1) & a * M1 is_line_circulant_about q )
thus ( len q = width (a * M1) & a * M1 is_line_circulant_about q ) by A13; ::_thesis: verum
end;
theorem Th7: :: MATRIX16:7
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 + M2 is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 + M2 is line_circulant
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 + M2 is line_circulant
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is line_circulant & M2 is line_circulant implies M1 + M2 is line_circulant )
assume that
A1: M1 is line_circulant and
A2: M2 is line_circulant ; ::_thesis: M1 + M2 is line_circulant
consider p being FinSequence of K such that
A3: len p = width M1 and
A4: M1 is_line_circulant_about p by A1, Def2;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A7: width M1 = n by MATRIX_1:24;
then A8: dom p = Seg n by A3, FINSEQ_1:def_3;
consider q being FinSequence of K such that
A9: len q = width M2 and
A10: M2 is_line_circulant_about q by A2, Def2;
A11: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A12: width M2 = n by MATRIX_1:24;
then dom q = Seg n by A9, FINSEQ_1:def_3;
then A13: dom (p + q) = dom p by A8, POLYNOM1:1;
then A14: len (p + q) = n by A8, FINSEQ_1:def_3;
A15: width (M1 + M2) = n by MATRIX_1:24;
A16: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) )
assume A17: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
then A18: ((j - i) mod (len (p + q))) + 1 in dom (p + q) by A6, A8, A16, A13, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A11, A6, A17, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),(q . (((j - i) mod (len q)) + 1))) by A10, A5, A6, A17, Def1
.= the addF of K . ((p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1))) by A3, A4, A9, A11, A7, A12, A6, A14, A17, Def1
.= (p + q) . (((j - i) mod (len (p + q))) + 1) by A18, FUNCOP_1:22 ;
hence (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) ; ::_thesis: verum
end;
then M1 + M2 is_line_circulant_about p + q by A15, A14, Def1;
then consider r being FinSequence of K such that
A19: ( len r = width (M1 + M2) & M1 + M2 is_line_circulant_about r ) by A15, A14;
take r ; :: according to MATRIX16:def_2 ::_thesis: ( len r = width (M1 + M2) & M1 + M2 is_line_circulant_about r )
thus ( len r = width (M1 + M2) & M1 + M2 is_line_circulant_about r ) by A19; ::_thesis: verum
end;
theorem Th8: :: MATRIX16:8
for n being Element of NAT
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
(M1 + M2) + M3 is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
(M1 + M2) + M3 is line_circulant
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
(M1 + M2) + M3 is line_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies (M1 + M2) + M3 is line_circulant )
assume that
A1: ( M1 is line_circulant & M2 is line_circulant ) and
A2: M3 is line_circulant ; ::_thesis: (M1 + M2) + M3 is line_circulant
M1 + M2 is line_circulant by A1, Th7;
hence (M1 + M2) + M3 is line_circulant by A2, Th7; ::_thesis: verum
end;
theorem :: MATRIX16:9
for n being Element of NAT
for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) + (b * M2) is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) + (b * M2) is line_circulant
let K be Field; ::_thesis: for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) + (b * M2) is line_circulant
let a, b be Element of K; ::_thesis: for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) + (b * M2) is line_circulant
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is line_circulant & M2 is line_circulant implies (a * M1) + (b * M2) is line_circulant )
assume ( M1 is line_circulant & M2 is line_circulant ) ; ::_thesis: (a * M1) + (b * M2) is line_circulant
then ( a * M1 is line_circulant & b * M2 is line_circulant ) by Th6;
hence (a * M1) + (b * M2) is line_circulant by Th7; ::_thesis: verum
end;
theorem :: MATRIX16:10
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) + (c * M3) is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) + (c * M3) is line_circulant
let K be Field; ::_thesis: for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) + (c * M3) is line_circulant
let a, b, c be Element of K; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) + (c * M3) is line_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies ((a * M1) + (b * M2)) + (c * M3) is line_circulant )
assume that
A1: ( M1 is line_circulant & M2 is line_circulant ) and
A2: M3 is line_circulant ; ::_thesis: ((a * M1) + (b * M2)) + (c * M3) is line_circulant
A3: c * M3 is line_circulant by A2, Th6;
( a * M1 is line_circulant & b * M2 is line_circulant ) by A1, Th6;
hence ((a * M1) + (b * M2)) + (c * M3) is line_circulant by A3, Th8; ::_thesis: verum
end;
theorem Th11: :: MATRIX16:11
for n being Element of NAT
for K being Field
for M1 being Matrix of n,K st M1 is line_circulant holds
- M1 is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is line_circulant holds
- M1 is line_circulant
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is line_circulant holds
- M1 is line_circulant
let M1 be Matrix of n,K; ::_thesis: ( M1 is line_circulant implies - M1 is line_circulant )
A1: width M1 = n by MATRIX_1:24;
A2: Indices (- M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume M1 is line_circulant ; ::_thesis: - M1 is line_circulant
then consider p being FinSequence of K such that
A3: len p = width M1 and
A4: M1 is_line_circulant_about p by Def2;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then A5: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A6: ( width (- M1) = n & len (- p) = len p ) by CARD_1:def_7, MATRIX_1:24;
A7: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices (- M1) holds
(- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) implies (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) )
assume A8: [i,j] in Indices (- M1) ; ::_thesis: (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
then ((j - i) mod n) + 1 in Seg n by A2, Lm3;
then A9: ((j - i) mod (len p)) + 1 in dom p by A3, A1, FINSEQ_1:def_3;
(- M1) * (i,j) = - (M1 * (i,j)) by A7, A2, A8, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A4, A7, A2, A8, Def1
.= (- p) . (((j - i) mod (len p)) + 1) by A9, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) by A5, CARD_1:def_7; ::_thesis: verum
end;
then - M1 is_line_circulant_about - p by A3, A1, A6, Def1;
then consider r being FinSequence of K such that
A10: ( len r = width (- M1) & - M1 is_line_circulant_about r ) by A3, A6, MATRIX_1:24;
take r ; :: according to MATRIX16:def_2 ::_thesis: ( len r = width (- M1) & - M1 is_line_circulant_about r )
thus ( len r = width (- M1) & - M1 is_line_circulant_about r ) by A10; ::_thesis: verum
end;
theorem :: MATRIX16:12
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 - M2 is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 - M2 is line_circulant
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 - M2 is line_circulant
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is line_circulant & M2 is line_circulant implies M1 - M2 is line_circulant )
assume that
A1: M1 is line_circulant and
A2: M2 is line_circulant ; ::_thesis: M1 - M2 is line_circulant
- M2 is line_circulant by A2, Th11;
hence M1 - M2 is line_circulant by A1, Th7; ::_thesis: verum
end;
theorem Th13: :: MATRIX16:13
for n being Element of NAT
for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) - (b * M2) is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) - (b * M2) is line_circulant
let K be Field; ::_thesis: for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) - (b * M2) is line_circulant
let a, b be Element of K; ::_thesis: for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) - (b * M2) is line_circulant
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is line_circulant & M2 is line_circulant implies (a * M1) - (b * M2) is line_circulant )
assume that
A1: M1 is line_circulant and
A2: M2 is line_circulant ; ::_thesis: (a * M1) - (b * M2) is line_circulant
b * M2 is line_circulant by A2, Th6;
then A3: - (b * M2) is line_circulant by Th11;
a * M1 is line_circulant by A1, Th6;
hence (a * M1) - (b * M2) is line_circulant by A3, Th7; ::_thesis: verum
end;
theorem :: MATRIX16:14
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) - (c * M3) is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) - (c * M3) is line_circulant
let K be Field; ::_thesis: for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) - (c * M3) is line_circulant
let a, b, c be Element of K; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) - (c * M3) is line_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies ((a * M1) + (b * M2)) - (c * M3) is line_circulant )
assume that
A1: ( M1 is line_circulant & M2 is line_circulant ) and
A2: M3 is line_circulant ; ::_thesis: ((a * M1) + (b * M2)) - (c * M3) is line_circulant
c * M3 is line_circulant by A2, Th6;
then A3: - (c * M3) is line_circulant by Th11;
( a * M1 is line_circulant & b * M2 is line_circulant ) by A1, Th6;
then (a * M1) + (b * M2) is line_circulant by Th7;
hence ((a * M1) + (b * M2)) - (c * M3) is line_circulant by A3, Th7; ::_thesis: verum
end;
theorem :: MATRIX16:15
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) - (c * M3) is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) - (c * M3) is line_circulant
let K be Field; ::_thesis: for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) - (c * M3) is line_circulant
let a, b, c be Element of K; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) - (c * M3) is line_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies ((a * M1) - (b * M2)) - (c * M3) is line_circulant )
assume that
A1: ( M1 is line_circulant & M2 is line_circulant ) and
A2: M3 is line_circulant ; ::_thesis: ((a * M1) - (b * M2)) - (c * M3) is line_circulant
c * M3 is line_circulant by A2, Th6;
then A3: - (c * M3) is line_circulant by Th11;
(a * M1) - (b * M2) is line_circulant by A1, Th13;
hence ((a * M1) - (b * M2)) - (c * M3) is line_circulant by A3, Th7; ::_thesis: verum
end;
theorem :: MATRIX16:16
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) + (c * M3) is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) + (c * M3) is line_circulant
let K be Field; ::_thesis: for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) + (c * M3) is line_circulant
let a, b, c be Element of K; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) + (c * M3) is line_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is line_circulant & M2 is line_circulant & M3 is line_circulant implies ((a * M1) - (b * M2)) + (c * M3) is line_circulant )
assume ( M1 is line_circulant & M2 is line_circulant & M3 is line_circulant ) ; ::_thesis: ((a * M1) - (b * M2)) + (c * M3) is line_circulant
then ( c * M3 is line_circulant & (a * M1) - (b * M2) is line_circulant ) by Th6, Th13;
hence ((a * M1) - (b * M2)) + (c * M3) is line_circulant by Th7; ::_thesis: verum
end;
theorem :: MATRIX16:17
for n being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is col_circulant & n > 0 holds
A @ is line_circulant
proof
let n be Element of NAT ; ::_thesis: for D being non empty set
for A being Matrix of n,D st A is col_circulant & n > 0 holds
A @ is line_circulant
let D be non empty set ; ::_thesis: for A being Matrix of n,D st A is col_circulant & n > 0 holds
A @ is line_circulant
let A be Matrix of n,D; ::_thesis: ( A is col_circulant & n > 0 implies A @ is line_circulant )
assume that
A1: A is col_circulant and
A2: n > 0 ; ::_thesis: A @ is line_circulant
consider p being FinSequence of D such that
A3: len p = len A and
A4: A is_col_circulant_about p by A1, Def5;
width A = n by MATRIX_1:24;
then A5: width (A @) = len p by A2, A3, MATRIX_2:10;
for i, j being Nat st [i,j] in Indices (A @) holds
(A @) * (i,j) = p . (((j - i) mod (len p)) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A @) implies (A @) * (i,j) = p . (((j - i) mod (len p)) + 1) )
A6: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume [i,j] in Indices (A @) ; ::_thesis: (A @) * (i,j) = p . (((j - i) mod (len p)) + 1)
then [i,j] in Indices A by MATRIX_1:26;
then ( i in Seg n & j in Seg n ) by A6, ZFMISC_1:87;
then A7: [j,i] in Indices A by A6, ZFMISC_1:87;
then (A @) * (i,j) = A * (j,i) by MATRIX_1:def_6;
hence (A @) * (i,j) = p . (((j - i) mod (len p)) + 1) by A4, A7, Def4; ::_thesis: verum
end;
then A @ is_line_circulant_about p by A5, Def1;
then consider p being FinSequence of D such that
A8: ( len p = width (A @) & A @ is_line_circulant_about p ) by A5;
take p ; :: according to MATRIX16:def_2 ::_thesis: ( len p = width (A @) & A @ is_line_circulant_about p )
thus ( len p = width (A @) & A @ is_line_circulant_about p ) by A8; ::_thesis: verum
end;
theorem :: MATRIX16:18
for n being Element of NAT
for D being non empty set
for t being FinSequence of D
for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds
t = Col (A,1)
proof
let n be Element of NAT ; ::_thesis: for D being non empty set
for t being FinSequence of D
for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds
t = Col (A,1)
let D be non empty set ; ::_thesis: for t being FinSequence of D
for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds
t = Col (A,1)
let t be FinSequence of D; ::_thesis: for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds
t = Col (A,1)
let A be Matrix of n,D; ::_thesis: ( A is_col_circulant_about t & n > 0 implies t = Col (A,1) )
assume that
A1: A is_col_circulant_about t and
A2: n > 0 ; ::_thesis: t = Col (A,1)
A3: len A = n by MATRIX_1:24;
then A4: len t = n by A1, Def4;
A5: dom t = Seg (len t) by FINSEQ_1:def_3;
len (Col (A,1)) = n by A3, MATRIX_1:def_8;
then A6: dom (Col (A,1)) = dom t by A5, A4, FINSEQ_1:def_3;
for k being Nat st k in dom t holds
t . k = (Col (A,1)) . k
proof
let k be Nat; ::_thesis: ( k in dom t implies t . k = (Col (A,1)) . k )
assume A7: k in dom t ; ::_thesis: t . k = (Col (A,1)) . k
then A8: ( 1 <= k & k <= n ) by A5, A4, FINSEQ_1:1;
n >= 0 + 1 by A2, INT_1:7;
then 1 in Seg n ;
then [k,1] in [:(Seg n),(Seg n):] by A5, A4, A7, ZFMISC_1:def_2;
then A9: [k,1] in Indices A by MATRIX_1:24;
len (Col (A,1)) = len A by MATRIX_1:def_8;
then dom (Col (A,1)) = Seg (len A) by FINSEQ_1:def_3;
then k in dom A by A6, A7, FINSEQ_1:def_3;
then (Col (A,1)) . k = A * (k,1) by MATRIX_1:def_8
.= t . (((k - 1) mod (len t)) + 1) by A1, A9, Def4
.= t . ((k - 1) + 1) by A4, A8, Lm1 ;
hence t . k = (Col (A,1)) . k ; ::_thesis: verum
end;
hence t = Col (A,1) by A6, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: MATRIX16:19
for i, j, n, k, l being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
proof
let i, j, n, k, l be Element of NAT ; ::_thesis: for D being non empty set
for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
let D be non empty set ; ::_thesis: for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
let A be Matrix of n,D; ::_thesis: ( A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies A * (i,j) = A * (k,l) )
assume that
A1: A is col_circulant and
A2: [i,j] in [:(Seg n),(Seg n):] and
A3: k = i + 1 and
A4: l = j + 1 and
A5: i < n and
A6: j < n ; ::_thesis: A * (i,j) = A * (k,l)
A7: [i,j] in Indices A by A2, MATRIX_1:24;
j in Seg n by A2, ZFMISC_1:87;
then 1 <= j by FINSEQ_1:1;
then 1 + 1 <= j + 1 by XREAL_1:6;
then A8: 1 <= l by A4, XXREAL_0:2;
l <= n by A4, A6, INT_1:7;
then A9: l in Seg n by A8;
i in Seg n by A2, ZFMISC_1:87;
then 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A10: 1 <= k by A3, XXREAL_0:2;
consider p being FinSequence of D such that
len p = len A and
A11: A is_col_circulant_about p by A1, Def5;
k <= n by A3, A5, INT_1:7;
then ( Indices A = [:(Seg n),(Seg n):] & k in Seg n ) by A10, MATRIX_1:24;
then [k,l] in Indices A by A9, ZFMISC_1:87;
then A * (k,l) = p . (((k - l) mod (len p)) + 1) by A11, Def4
.= p . (((i - j) mod (len p)) + 1) by A3, A4
.= A * (i,j) by A11, A7, Def4 ;
hence A * (i,j) = A * (k,l) ; ::_thesis: verum
end;
theorem Th20: :: MATRIX16:20
for n being Element of NAT
for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
let K be Field; ::_thesis: for a being Element of K
for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
let a be Element of K; ::_thesis: for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
let M1 be Matrix of n,K; ::_thesis: ( M1 is col_circulant implies a * M1 is col_circulant )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume M1 is col_circulant ; ::_thesis: a * M1 is col_circulant
then consider p being FinSequence of K such that
A2: len p = len M1 and
A3: M1 is_col_circulant_about p by Def5;
A4: len M1 = n by MATRIX_1:24;
then A5: dom p = Seg n by A2, FINSEQ_1:def_3;
A6: len (a * p) = len p by MATRIXR1:16;
A7: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
A8: for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) = (a * p) . (((i - j) mod (len p)) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) = (a * p) . (((i - j) mod (len p)) + 1) )
assume [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) = (a * p) . (((i - j) mod (len p)) + 1)
then A9: [i,j] in Indices M1 by MATRIX_1:26;
then A10: ((i - j) mod (len p)) + 1 in Seg n by A2, A1, A4, Lm3;
(a * M1) * (i,j) = a * (M1 * (i,j)) by A9, MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (((i - j) mod (len p)) + 1)) by A3, A9, Def4
.= (a multfield) . (p /. (((i - j) mod (len p)) + 1)) by A5, A10, PARTFUN1:def_6
.= a * (p /. (((i - j) mod (len p)) + 1)) by FVSUM_1:49
.= (a * p) /. (((i - j) mod (len p)) + 1) by A5, A10, POLYNOM1:def_1
.= (a * p) . (((i - j) mod (len p)) + 1) by A2, A4, A6, A7, A10, PARTFUN1:def_6 ;
hence (a * M1) * (i,j) = (a * p) . (((i - j) mod (len p)) + 1) ; ::_thesis: verum
end;
A11: len (a * M1) = n by MATRIX_1:24;
len p = n by A2, MATRIX_1:24;
then a * M1 is_col_circulant_about a * p by A11, A6, A8, Def4;
then consider q being FinSequence of K such that
A12: ( len q = len (a * M1) & a * M1 is_col_circulant_about q ) by A2, A11, A6, MATRIX_1:24;
take q ; :: according to MATRIX16:def_5 ::_thesis: ( len q = len (a * M1) & a * M1 is_col_circulant_about q )
thus ( len q = len (a * M1) & a * M1 is_col_circulant_about q ) by A12; ::_thesis: verum
end;
theorem Th21: :: MATRIX16:21
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 + M2 is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 + M2 is col_circulant
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 + M2 is col_circulant
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is col_circulant & M2 is col_circulant implies M1 + M2 is col_circulant )
assume that
A1: M1 is col_circulant and
A2: M2 is col_circulant ; ::_thesis: M1 + M2 is col_circulant
consider p being FinSequence of K such that
A3: len p = len M1 and
A4: M1 is_col_circulant_about p by A1, Def5;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
consider q being FinSequence of K such that
A7: len q = len M2 and
A8: M2 is_col_circulant_about q by A2, Def5;
A9: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A10: len (M1 + M2) = n by MATRIX_1:24;
A11: len M1 = n by MATRIX_1:24;
then A12: dom p = Seg n by A3, FINSEQ_1:def_3;
A13: len M2 = n by MATRIX_1:24;
then dom q = Seg n by A7, FINSEQ_1:def_3;
then A14: dom (p + q) = dom p by A12, POLYNOM1:1;
then A15: len (p + q) = n by A12, FINSEQ_1:def_3;
A16: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1) )
assume A17: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1)
then A18: ((i - j) mod (len (p + q))) + 1 in Seg n by A6, A12, A16, A14, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A9, A6, A17, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),(q . (((i - j) mod (len q)) + 1))) by A8, A5, A6, A17, Def4
.= the addF of K . ((p . (((i - j) mod (len (p + q))) + 1)),(q . (((i - j) mod (len (p + q))) + 1))) by A3, A4, A7, A9, A11, A13, A6, A15, A17, Def4
.= (p + q) . (((i - j) mod (len (p + q))) + 1) by A12, A14, A18, FUNCOP_1:22 ;
hence (M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1) ; ::_thesis: verum
end;
then M1 + M2 is_col_circulant_about p + q by A10, A15, Def4;
then consider r being FinSequence of K such that
A19: ( len r = len (M1 + M2) & M1 + M2 is_col_circulant_about r ) by A10, A15;
take r ; :: according to MATRIX16:def_5 ::_thesis: ( len r = len (M1 + M2) & M1 + M2 is_col_circulant_about r )
thus ( len r = len (M1 + M2) & M1 + M2 is_col_circulant_about r ) by A19; ::_thesis: verum
end;
theorem Th22: :: MATRIX16:22
for n being Element of NAT
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
(M1 + M2) + M3 is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
(M1 + M2) + M3 is col_circulant
let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
(M1 + M2) + M3 is col_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies (M1 + M2) + M3 is col_circulant )
assume that
A1: ( M1 is col_circulant & M2 is col_circulant ) and
A2: M3 is col_circulant ; ::_thesis: (M1 + M2) + M3 is col_circulant
M1 + M2 is col_circulant by A1, Th21;
hence (M1 + M2) + M3 is col_circulant by A2, Th21; ::_thesis: verum
end;
theorem :: MATRIX16:23
for n being Element of NAT
for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) + (b * M2) is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) + (b * M2) is col_circulant
let K be Field; ::_thesis: for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) + (b * M2) is col_circulant
let a, b be Element of K; ::_thesis: for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) + (b * M2) is col_circulant
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is col_circulant & M2 is col_circulant implies (a * M1) + (b * M2) is col_circulant )
assume ( M1 is col_circulant & M2 is col_circulant ) ; ::_thesis: (a * M1) + (b * M2) is col_circulant
then ( a * M1 is col_circulant & b * M2 is col_circulant ) by Th20;
hence (a * M1) + (b * M2) is col_circulant by Th21; ::_thesis: verum
end;
theorem :: MATRIX16:24
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) + (c * M3) is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) + (c * M3) is col_circulant
let K be Field; ::_thesis: for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) + (c * M3) is col_circulant
let a, b, c be Element of K; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) + (c * M3) is col_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies ((a * M1) + (b * M2)) + (c * M3) is col_circulant )
assume that
A1: ( M1 is col_circulant & M2 is col_circulant ) and
A2: M3 is col_circulant ; ::_thesis: ((a * M1) + (b * M2)) + (c * M3) is col_circulant
A3: c * M3 is col_circulant by A2, Th20;
( a * M1 is col_circulant & b * M2 is col_circulant ) by A1, Th20;
hence ((a * M1) + (b * M2)) + (c * M3) is col_circulant by A3, Th22; ::_thesis: verum
end;
theorem Th25: :: MATRIX16:25
for n being Element of NAT
for K being Field
for M1 being Matrix of n,K st M1 is col_circulant holds
- M1 is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is col_circulant holds
- M1 is col_circulant
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is col_circulant holds
- M1 is col_circulant
let M1 be Matrix of n,K; ::_thesis: ( M1 is col_circulant implies - M1 is col_circulant )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices (- M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume M1 is col_circulant ; ::_thesis: - M1 is col_circulant
then consider p being FinSequence of K such that
A3: len p = len M1 and
A4: M1 is_col_circulant_about p by Def5;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then A5: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A6: ( len (- M1) = n & len (- p) = len p ) by CARD_1:def_7, MATRIX_1:24;
A7: len M1 = n by MATRIX_1:24;
then A8: dom p = Seg n by A3, FINSEQ_1:def_3;
for i, j being Nat st [i,j] in Indices (- M1) holds
(- M1) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) implies (- M1) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1) )
assume A9: [i,j] in Indices (- M1) ; ::_thesis: (- M1) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1)
then A10: ((i - j) mod n) + 1 in Seg n by A2, Lm3;
(- M1) * (i,j) = - (M1 * (i,j)) by A1, A2, A9, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . (p . (((i - j) mod (len p)) + 1)) by A4, A1, A2, A9, Def4
.= (- p) . (((i - j) mod (len p)) + 1) by A3, A7, A8, A10, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1) by A5, CARD_1:def_7; ::_thesis: verum
end;
then - M1 is_col_circulant_about - p by A3, A7, A6, Def4;
then consider r being FinSequence of K such that
A11: ( len r = len (- M1) & - M1 is_col_circulant_about r ) by A3, A6, MATRIX_1:24;
take r ; :: according to MATRIX16:def_5 ::_thesis: ( len r = len (- M1) & - M1 is_col_circulant_about r )
thus ( len r = len (- M1) & - M1 is_col_circulant_about r ) by A11; ::_thesis: verum
end;
theorem :: MATRIX16:26
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 - M2 is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 - M2 is col_circulant
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 - M2 is col_circulant
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is col_circulant & M2 is col_circulant implies M1 - M2 is col_circulant )
assume that
A1: M1 is col_circulant and
A2: M2 is col_circulant ; ::_thesis: M1 - M2 is col_circulant
- M2 is col_circulant by A2, Th25;
hence M1 - M2 is col_circulant by A1, Th21; ::_thesis: verum
end;
theorem Th27: :: MATRIX16:27
for n being Element of NAT
for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) - (b * M2) is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) - (b * M2) is col_circulant
let K be Field; ::_thesis: for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) - (b * M2) is col_circulant
let a, b be Element of K; ::_thesis: for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) - (b * M2) is col_circulant
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is col_circulant & M2 is col_circulant implies (a * M1) - (b * M2) is col_circulant )
assume that
A1: M1 is col_circulant and
A2: M2 is col_circulant ; ::_thesis: (a * M1) - (b * M2) is col_circulant
b * M2 is col_circulant by A2, Th20;
then A3: - (b * M2) is col_circulant by Th25;
a * M1 is col_circulant by A1, Th20;
hence (a * M1) - (b * M2) is col_circulant by A3, Th21; ::_thesis: verum
end;
theorem :: MATRIX16:28
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) - (c * M3) is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) - (c * M3) is col_circulant
let K be Field; ::_thesis: for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) - (c * M3) is col_circulant
let a, b, c be Element of K; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) - (c * M3) is col_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies ((a * M1) + (b * M2)) - (c * M3) is col_circulant )
assume that
A1: ( M1 is col_circulant & M2 is col_circulant ) and
A2: M3 is col_circulant ; ::_thesis: ((a * M1) + (b * M2)) - (c * M3) is col_circulant
c * M3 is col_circulant by A2, Th20;
then A3: - (c * M3) is col_circulant by Th25;
( a * M1 is col_circulant & b * M2 is col_circulant ) by A1, Th20;
then (a * M1) + (b * M2) is col_circulant by Th21;
hence ((a * M1) + (b * M2)) - (c * M3) is col_circulant by A3, Th21; ::_thesis: verum
end;
theorem :: MATRIX16:29
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) - (c * M3) is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) - (c * M3) is col_circulant
let K be Field; ::_thesis: for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) - (c * M3) is col_circulant
let a, b, c be Element of K; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) - (c * M3) is col_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies ((a * M1) - (b * M2)) - (c * M3) is col_circulant )
assume that
A1: ( M1 is col_circulant & M2 is col_circulant ) and
A2: M3 is col_circulant ; ::_thesis: ((a * M1) - (b * M2)) - (c * M3) is col_circulant
c * M3 is col_circulant by A2, Th20;
then A3: - (c * M3) is col_circulant by Th25;
(a * M1) - (b * M2) is col_circulant by A1, Th27;
hence ((a * M1) - (b * M2)) - (c * M3) is col_circulant by A3, Th21; ::_thesis: verum
end;
theorem :: MATRIX16:30
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) + (c * M3) is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) + (c * M3) is col_circulant
let K be Field; ::_thesis: for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) + (c * M3) is col_circulant
let a, b, c be Element of K; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) + (c * M3) is col_circulant
let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is col_circulant & M2 is col_circulant & M3 is col_circulant implies ((a * M1) - (b * M2)) + (c * M3) is col_circulant )
assume ( M1 is col_circulant & M2 is col_circulant & M3 is col_circulant ) ; ::_thesis: ((a * M1) - (b * M2)) + (c * M3) is col_circulant
then ( c * M3 is col_circulant & (a * M1) - (b * M2) is col_circulant ) by Th20, Th27;
hence ((a * M1) - (b * M2)) + (c * M3) is col_circulant by Th21; ::_thesis: verum
end;
theorem Th31: :: MATRIX16:31
for K being Field
for p being FinSequence of K st p is first-line-of-circulant holds
- p is first-line-of-circulant
proof
let K be Field; ::_thesis: for p being FinSequence of K st p is first-line-of-circulant holds
- p is first-line-of-circulant
let p be FinSequence of K; ::_thesis: ( p is first-line-of-circulant implies - p is first-line-of-circulant )
set n = len p;
assume p is first-line-of-circulant ; ::_thesis: - p is first-line-of-circulant
then consider M1 being Matrix of len p,K such that
A1: M1 is_line_circulant_about p by Def3;
set M2 = - M1;
A2: Indices M1 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A3: Indices (- M1) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then A4: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A5: len (- p) = len p by CARD_1:def_7;
A6: dom p = Seg (len p) by FINSEQ_1:def_3;
A7: for i, j being Nat st [i,j] in Indices (- M1) holds
(- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) implies (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) )
assume A8: [i,j] in Indices (- M1) ; ::_thesis: (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
then A9: ((j - i) mod (len p)) + 1 in Seg (len p) by A3, Lm3;
(- M1) * (i,j) = - (M1 * (i,j)) by A2, A3, A8, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A1, A2, A3, A8, Def1
.= (- p) . (((j - i) mod (len p)) + 1) by A6, A9, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) by A4, CARD_1:def_7; ::_thesis: verum
end;
width (- M1) = len p by MATRIX_1:24;
then - M1 is_line_circulant_about - p by A5, A7, Def1;
then consider M2 being Matrix of len (- p),K such that
A10: M2 is_line_circulant_about - p by A5;
take M2 ; :: according to MATRIX16:def_3 ::_thesis: M2 is_line_circulant_about - p
thus M2 is_line_circulant_about - p by A10; ::_thesis: verum
end;
theorem :: MATRIX16:32
for K being Field
for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (- p) = - (LCirc p)
proof
let K be Field; ::_thesis: for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (- p) = - (LCirc p)
let p be FinSequence of K; ::_thesis: ( p is first-line-of-circulant implies LCirc (- p) = - (LCirc p) )
set n = len p;
A1: ( len (LCirc p) = len p & width (LCirc p) = len p ) by MATRIX_1:24;
A2: Indices (LCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A3: len (- p) = len p by CARD_1:def_7;
assume A4: p is first-line-of-circulant ; ::_thesis: LCirc (- p) = - (LCirc p)
then - p is first-line-of-circulant by Th31;
then A5: LCirc (- p) is_line_circulant_about - p by Def7;
A6: LCirc p is_line_circulant_about p by A4, Def7;
A7: for i, j being Nat st [i,j] in Indices (LCirc p) holds
(LCirc (- p)) * (i,j) = - ((LCirc p) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (LCirc p) implies (LCirc (- p)) * (i,j) = - ((LCirc p) * (i,j)) )
assume A8: [i,j] in Indices (LCirc p) ; ::_thesis: (LCirc (- p)) * (i,j) = - ((LCirc p) * (i,j))
then ((j - i) mod (len p)) + 1 in Seg (len p) by A2, Lm3;
then A9: ((j - i) mod (len p)) + 1 in dom p by FINSEQ_1:def_3;
[i,j] in Indices (LCirc (- p)) by A3, A8, MATRIX_1:26;
then (LCirc (- p)) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) by A5, Def1
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A3, A9, FUNCT_1:13
.= (comp K) . ((LCirc p) * (i,j)) by A6, A8, Def1
.= - ((LCirc p) * (i,j)) by VECTSP_1:def_13 ;
hence (LCirc (- p)) * (i,j) = - ((LCirc p) * (i,j)) ; ::_thesis: verum
end;
( len (LCirc (- p)) = len p & width (LCirc (- p)) = len p ) by A3, MATRIX_1:24;
hence LCirc (- p) = - (LCirc p) by A1, A7, MATRIX_3:def_2; ::_thesis: verum
end;
theorem Th33: :: MATRIX16:33
for K being Field
for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
p + q is first-line-of-circulant
proof
let K be Field; ::_thesis: for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
p + q is first-line-of-circulant
let p, q be FinSequence of K; ::_thesis: ( p is first-line-of-circulant & q is first-line-of-circulant & len p = len q implies p + q is first-line-of-circulant )
set n = len p;
assume that
A1: p is first-line-of-circulant and
A2: q is first-line-of-circulant and
A3: len p = len q ; ::_thesis: p + q is first-line-of-circulant
consider M2 being Matrix of len p,K such that
A4: M2 is_line_circulant_about q by A2, A3, Def3;
A5: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
A6: dom p = Seg (len p) by FINSEQ_1:def_3;
dom q = Seg (len p) by A3, FINSEQ_1:def_3;
then A7: dom (p + q) = dom p by A6, POLYNOM1:1;
then A8: len (p + q) = len p by A6, FINSEQ_1:def_3;
consider M1 being Matrix of len p,K such that
A9: M1 is_line_circulant_about p by A1, Def3;
A10: Indices M1 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
set M3 = M1 + M2;
A11: width (M1 + M2) = len p by MATRIX_1:24;
A12: Indices M2 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) )
assume A13: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
then A14: [i,j] in Indices M1 by A10, MATRIX_1:24;
then A15: ((j - i) mod (len (p + q))) + 1 in dom (p + q) by A10, A6, A5, A7, Lm3;
A16: [i,j] in Indices M2 by A12, A13, MATRIX_1:24;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A14, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),(q . (((j - i) mod (len q)) + 1))) by A4, A16, Def1
.= the addF of K . ((p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1))) by A3, A9, A8, A14, Def1
.= (p + q) . (((j - i) mod (len (p + q))) + 1) by A15, FUNCOP_1:22 ;
hence (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) ; ::_thesis: verum
end;
then M1 + M2 is_line_circulant_about p + q by A11, A8, Def1;
then consider M3 being Matrix of len (p + q),K such that
len (p + q) = width M3 and
A17: M3 is_line_circulant_about p + q by A11, A8;
take M3 ; :: according to MATRIX16:def_3 ::_thesis: M3 is_line_circulant_about p + q
thus M3 is_line_circulant_about p + q by A17; ::_thesis: verum
end;
theorem Th34: :: MATRIX16:34
for K being Field
for p, q being FinSequence of K st len p = len q & p is first-line-of-circulant & q is first-line-of-circulant holds
LCirc (p + q) = (LCirc p) + (LCirc q)
proof
let K be Field; ::_thesis: for p, q being FinSequence of K st len p = len q & p is first-line-of-circulant & q is first-line-of-circulant holds
LCirc (p + q) = (LCirc p) + (LCirc q)
let p, q be FinSequence of K; ::_thesis: ( len p = len q & p is first-line-of-circulant & q is first-line-of-circulant implies LCirc (p + q) = (LCirc p) + (LCirc q) )
set n = len p;
assume that
A1: len p = len q and
A2: p is first-line-of-circulant and
A3: q is first-line-of-circulant ; ::_thesis: LCirc (p + q) = (LCirc p) + (LCirc q)
A4: ( LCirc q is_line_circulant_about q & Indices (LCirc p) = Indices (LCirc q) ) by A1, A3, Def7, MATRIX_1:26;
p + q is first-line-of-circulant by A1, A2, A3, Th33;
then A5: LCirc (p + q) is_line_circulant_about p + q by Def7;
A6: dom p = Seg (len p) by FINSEQ_1:def_3;
A7: LCirc p is_line_circulant_about p by A2, Def7;
A8: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
A9: Indices (LCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
dom q = Seg (len p) by A1, FINSEQ_1:def_3;
then dom (p + q) = dom p by A6, POLYNOM1:1;
then A10: len (p + q) = len p by A6, FINSEQ_1:def_3;
then A11: Indices (LCirc p) = Indices (LCirc (p + q)) by MATRIX_1:26;
A12: for i, j being Nat st [i,j] in Indices (LCirc p) holds
(LCirc (p + q)) * (i,j) = ((LCirc p) * (i,j)) + ((LCirc q) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (LCirc p) implies (LCirc (p + q)) * (i,j) = ((LCirc p) * (i,j)) + ((LCirc q) * (i,j)) )
assume A13: [i,j] in Indices (LCirc p) ; ::_thesis: (LCirc (p + q)) * (i,j) = ((LCirc p) * (i,j)) + ((LCirc q) * (i,j))
then A14: ((j - i) mod (len p)) + 1 in Seg (len p) by A9, Lm3;
(LCirc (p + q)) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) by A5, A11, A13, Def1
.= the addF of K . ((p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1))) by A8, A10, A14, FUNCOP_1:22
.= the addF of K . (((LCirc p) * (i,j)),(q . (((j - i) mod (len q)) + 1))) by A1, A10, A7, A13, Def1
.= ((LCirc p) * (i,j)) + ((LCirc q) * (i,j)) by A4, A13, Def1 ;
hence (LCirc (p + q)) * (i,j) = ((LCirc p) * (i,j)) + ((LCirc q) * (i,j)) ; ::_thesis: verum
end;
A15: ( len (LCirc p) = len p & width (LCirc p) = len p ) by MATRIX_1:24;
( len (LCirc (p + q)) = len p & width (LCirc (p + q)) = len p ) by A10, MATRIX_1:24;
hence LCirc (p + q) = (LCirc p) + (LCirc q) by A15, A12, MATRIX_3:def_3; ::_thesis: verum
end;
theorem Th35: :: MATRIX16:35
for K being Field
for p being FinSequence of K st p is first-col-of-circulant holds
- p is first-col-of-circulant
proof
let K be Field; ::_thesis: for p being FinSequence of K st p is first-col-of-circulant holds
- p is first-col-of-circulant
let p be FinSequence of K; ::_thesis: ( p is first-col-of-circulant implies - p is first-col-of-circulant )
set n = len p;
assume p is first-col-of-circulant ; ::_thesis: - p is first-col-of-circulant
then consider M1 being Matrix of len p,K such that
A1: M1 is_col_circulant_about p by Def6;
set M2 = - M1;
A2: Indices M1 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A3: Indices (- M1) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then A4: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A5: len (- p) = len p by CARD_1:def_7;
A6: dom p = Seg (len p) by FINSEQ_1:def_3;
A7: for i, j being Nat st [i,j] in Indices (- M1) holds
(- M1) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) implies (- M1) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1) )
assume A8: [i,j] in Indices (- M1) ; ::_thesis: (- M1) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1)
then A9: ((i - j) mod (len p)) + 1 in Seg (len p) by A3, Lm3;
(- M1) * (i,j) = - (M1 * (i,j)) by A2, A3, A8, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . (p . (((i - j) mod (len p)) + 1)) by A1, A2, A3, A8, Def4
.= (- p) . (((i - j) mod (len p)) + 1) by A6, A9, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1) by A4, CARD_1:def_7; ::_thesis: verum
end;
len (- M1) = len p by MATRIX_1:24;
then - M1 is_col_circulant_about - p by A5, A7, Def4;
then consider M2 being Matrix of len (- p),K such that
A10: M2 is_col_circulant_about - p by A5;
take M2 ; :: according to MATRIX16:def_6 ::_thesis: M2 is_col_circulant_about - p
thus M2 is_col_circulant_about - p by A10; ::_thesis: verum
end;
theorem :: MATRIX16:36
for K being Field
for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (- p) = - (CCirc p)
proof
let K be Field; ::_thesis: for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (- p) = - (CCirc p)
let p be FinSequence of K; ::_thesis: ( p is first-col-of-circulant implies CCirc (- p) = - (CCirc p) )
set n = len p;
A1: dom p = Seg (len p) by FINSEQ_1:def_3;
A2: Indices (CCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
assume A3: p is first-col-of-circulant ; ::_thesis: CCirc (- p) = - (CCirc p)
then A4: CCirc p is_col_circulant_about p by Def8;
- p is first-col-of-circulant by A3, Th35;
then A5: CCirc (- p) is_col_circulant_about - p by Def8;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A6: len (- p) = len p by CARD_1:def_7;
then A7: Indices (CCirc p) = Indices (CCirc (- p)) by MATRIX_1:26;
A8: for i, j being Nat st [i,j] in Indices (CCirc p) holds
(CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (CCirc p) implies (CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j)) )
assume A9: [i,j] in Indices (CCirc p) ; ::_thesis: (CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j))
then A10: ((i - j) mod (len p)) + 1 in Seg (len p) by A2, Lm3;
(CCirc (- p)) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1) by A5, A7, A9, Def4
.= (comp K) . (p . (((i - j) mod (len p)) + 1)) by A6, A1, A10, FUNCT_1:13
.= (comp K) . ((CCirc p) * (i,j)) by A4, A9, Def4
.= - ((CCirc p) * (i,j)) by VECTSP_1:def_13 ;
hence (CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j)) ; ::_thesis: verum
end;
A11: ( len (CCirc p) = len p & width (CCirc p) = len p ) by MATRIX_1:24;
( len (CCirc (- p)) = len p & width (CCirc (- p)) = len p ) by A6, MATRIX_1:24;
hence CCirc (- p) = - (CCirc p) by A11, A8, MATRIX_3:def_2; ::_thesis: verum
end;
theorem Th37: :: MATRIX16:37
for K being Field
for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds
p + q is first-col-of-circulant
proof
let K be Field; ::_thesis: for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds
p + q is first-col-of-circulant
let p, q be FinSequence of K; ::_thesis: ( p is first-col-of-circulant & q is first-col-of-circulant & len p = len q implies p + q is first-col-of-circulant )
set n = len p;
assume that
A1: p is first-col-of-circulant and
A2: q is first-col-of-circulant and
A3: len p = len q ; ::_thesis: p + q is first-col-of-circulant
consider M2 being Matrix of len p,K such that
A4: M2 is_col_circulant_about q by A2, A3, Def6;
A5: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
A6: dom p = Seg (len p) by FINSEQ_1:def_3;
dom q = Seg (len p) by A3, FINSEQ_1:def_3;
then A7: dom (p + q) = dom p by A6, POLYNOM1:1;
then A8: len (p + q) = len p by A6, FINSEQ_1:def_3;
consider M1 being Matrix of len p,K such that
A9: M1 is_col_circulant_about p by A1, Def6;
A10: Indices M1 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
set M3 = M1 + M2;
A11: len (M1 + M2) = len p by MATRIX_1:24;
A12: Indices M2 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1) )
assume A13: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1)
then A14: [i,j] in Indices M1 by A10, MATRIX_1:24;
then A15: ((i - j) mod (len (p + q))) + 1 in dom (p + q) by A10, A6, A5, A7, Lm3;
A16: [i,j] in Indices M2 by A12, A13, MATRIX_1:24;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A14, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),(q . (((i - j) mod (len q)) + 1))) by A4, A16, Def4
.= the addF of K . ((p . (((i - j) mod (len (p + q))) + 1)),(q . (((i - j) mod (len (p + q))) + 1))) by A3, A9, A8, A14, Def4
.= (p + q) . (((i - j) mod (len (p + q))) + 1) by A15, FUNCOP_1:22 ;
hence (M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1) ; ::_thesis: verum
end;
then M1 + M2 is_col_circulant_about p + q by A11, A8, Def4;
then consider M3 being Matrix of len (p + q),K such that
len (p + q) = len M3 and
A17: M3 is_col_circulant_about p + q by A11, A8;
take M3 ; :: according to MATRIX16:def_6 ::_thesis: M3 is_col_circulant_about p + q
thus M3 is_col_circulant_about p + q by A17; ::_thesis: verum
end;
theorem Th38: :: MATRIX16:38
for K being Field
for p, q being FinSequence of K st len p = len q & p is first-col-of-circulant & q is first-col-of-circulant holds
CCirc (p + q) = (CCirc p) + (CCirc q)
proof
let K be Field; ::_thesis: for p, q being FinSequence of K st len p = len q & p is first-col-of-circulant & q is first-col-of-circulant holds
CCirc (p + q) = (CCirc p) + (CCirc q)
let p, q be FinSequence of K; ::_thesis: ( len p = len q & p is first-col-of-circulant & q is first-col-of-circulant implies CCirc (p + q) = (CCirc p) + (CCirc q) )
set n = len p;
assume that
A1: len p = len q and
A2: p is first-col-of-circulant and
A3: q is first-col-of-circulant ; ::_thesis: CCirc (p + q) = (CCirc p) + (CCirc q)
A4: ( CCirc q is_col_circulant_about q & Indices (CCirc p) = Indices (CCirc q) ) by A1, A3, Def8, MATRIX_1:26;
p + q is first-col-of-circulant by A1, A2, A3, Th37;
then A5: CCirc (p + q) is_col_circulant_about p + q by Def8;
A6: dom p = Seg (len p) by FINSEQ_1:def_3;
A7: CCirc p is_col_circulant_about p by A2, Def8;
A8: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
A9: Indices (CCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
dom q = Seg (len p) by A1, FINSEQ_1:def_3;
then dom (p + q) = dom p by A6, POLYNOM1:1;
then A10: len (p + q) = len p by A6, FINSEQ_1:def_3;
then A11: Indices (CCirc p) = Indices (CCirc (p + q)) by MATRIX_1:26;
A12: for i, j being Nat st [i,j] in Indices (CCirc p) holds
(CCirc (p + q)) * (i,j) = ((CCirc p) * (i,j)) + ((CCirc q) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (CCirc p) implies (CCirc (p + q)) * (i,j) = ((CCirc p) * (i,j)) + ((CCirc q) * (i,j)) )
assume A13: [i,j] in Indices (CCirc p) ; ::_thesis: (CCirc (p + q)) * (i,j) = ((CCirc p) * (i,j)) + ((CCirc q) * (i,j))
then A14: ((i - j) mod (len p)) + 1 in Seg (len p) by A9, Lm3;
(CCirc (p + q)) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1) by A5, A11, A13, Def4
.= the addF of K . ((p . (((i - j) mod (len (p + q))) + 1)),(q . (((i - j) mod (len (p + q))) + 1))) by A8, A10, A14, FUNCOP_1:22
.= the addF of K . (((CCirc p) * (i,j)),(q . (((i - j) mod (len q)) + 1))) by A1, A10, A7, A13, Def4
.= ((CCirc p) * (i,j)) + ((CCirc q) * (i,j)) by A4, A13, Def4 ;
hence (CCirc (p + q)) * (i,j) = ((CCirc p) * (i,j)) + ((CCirc q) * (i,j)) ; ::_thesis: verum
end;
A15: ( len (CCirc p) = len p & width (CCirc p) = len p ) by MATRIX_1:24;
( len (CCirc (p + q)) = len p & width (CCirc (p + q)) = len p ) by A10, MATRIX_1:24;
hence CCirc (p + q) = (CCirc p) + (CCirc q) by A15, A12, MATRIX_3:def_3; ::_thesis: verum
end;
theorem :: MATRIX16:39
for n being Element of NAT
for K being Field st n > 0 holds
1. (K,n) is col_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field st n > 0 holds
1. (K,n) is col_circulant
let K be Field; ::_thesis: ( n > 0 implies 1. (K,n) is col_circulant )
assume A1: n > 0 ; ::_thesis: 1. (K,n) is col_circulant
set M1 = 1. (K,n);
A2: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_1:24;
set p = Col ((1. (K,n)),1);
A3: len (1. (K,n)) = n by MATRIX_1:24;
then A4: len (Col ((1. (K,n)),1)) = n by MATRIX_1:def_8;
A5: dom (1. (K,n)) = Seg n by A3, FINSEQ_1:def_3;
A6: width (1. (K,n)) = n by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) )
A7: (i - j) mod n >= 0 by A1, NAT_D:62;
then A8: ((i - j) mod n) + 1 in NAT by INT_1:3;
assume A9: [i,j] in Indices (1. (K,n)) ; ::_thesis: (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
then A10: j in Seg n by A2, ZFMISC_1:87;
then A11: 1 <= j by FINSEQ_1:1;
A12: j <= n by A10, FINSEQ_1:1;
A13: i in Seg n by A2, A9, ZFMISC_1:87;
then 1 <= i by FINSEQ_1:1;
then A14: 1 - n <= i - j by A12, XREAL_1:13;
- n <= (- n) + 1 by XREAL_1:29;
then A15: - n <= i - j by A14, XXREAL_0:2;
i <= n by A13, FINSEQ_1:1;
then A16: i - j <= n - 1 by A11, XREAL_1:13;
n - 1 < n by XREAL_1:44;
then A17: i - j < n by A16, XXREAL_0:2;
(i - j) mod n <= n - 1
proof
percases ( 0 <= i - j or 0 > i - j ) ;
suppose 0 <= i - j ; ::_thesis: (i - j) mod n <= n - 1
hence (i - j) mod n <= n - 1 by A16, A17, NAT_D:63; ::_thesis: verum
end;
supposeA18: 0 > i - j ; ::_thesis: (i - j) mod n <= n - 1
then i - j <= - 1 by INT_1:8;
then n + (i - j) <= n + (- 1) by XREAL_1:6;
hence (i - j) mod n <= n - 1 by A15, A18, NAT_D:63; ::_thesis: verum
end;
end;
end;
then A19: ((i - j) mod n) + 1 <= (n - 1) + 1 by XREAL_1:6;
((i - j) mod n) + 1 >= 0 + 1 by A7, XREAL_1:6;
then A20: ((i - j) mod n) + 1 in Seg n by A19, A8;
then A21: ((i - j) mod (len (Col ((1. (K,n)),1)))) + 1 in Seg n by A3, MATRIX_1:def_8;
(1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
proof
percases ( i = j or i <> j ) ;
supposeA22: i = j ; ::_thesis: (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
0 + 1 <= n by A1, NAT_1:13;
then 1 in Seg n ;
then A23: [1,1] in Indices (1. (K,n)) by A2, ZFMISC_1:87;
(i - j) mod (len (Col ((1. (K,n)),1))) = 0 by A1, A4, A22, NAT_D:63;
then (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) = (1. (K,n)) * (1,1) by A5, A21, MATRIX_1:def_8
.= 1_ K by A23, MATRIX_1:def_11 ;
hence (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) by A9, A22, MATRIX_1:def_11; ::_thesis: verum
end;
supposeA24: i <> j ; ::_thesis: (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
then A25: i - j <> 0 ;
(i - j) mod n <> 0
proof
percases ( 0 <= i - j or 0 > i - j ) ;
suppose 0 <= i - j ; ::_thesis: (i - j) mod n <> 0
hence (i - j) mod n <> 0 by A17, A25, NAT_D:63; ::_thesis: verum
end;
supposeA26: 0 > i - j ; ::_thesis: (i - j) mod n <> 0
(1 - n) + n <= (i - j) + n by A14, XREAL_1:6;
hence (i - j) mod n <> 0 by A15, A26, NAT_D:63; ::_thesis: verum
end;
end;
end;
then A27: ((i - j) mod (len (Col ((1. (K,n)),1)))) + 1 <> 1 by A3, MATRIX_1:def_8;
set l = ((i - j) mod (len (Col ((1. (K,n)),1)))) + 1;
reconsider l = ((i - j) mod (len (Col ((1. (K,n)),1)))) + 1 as Nat by A3, A8, MATRIX_1:def_8;
0 + 1 <= n by A1, NAT_1:13;
then A28: 1 in Seg n ;
l in dom (1. (K,n)) by A3, A4, A20, FINSEQ_1:def_3;
then A29: [l,1] in Indices (1. (K,n)) by A6, A28, ZFMISC_1:87;
(Col ((1. (K,n)),1)) . l = (1. (K,n)) * (l,1) by A5, A21, MATRIX_1:def_8
.= 0. K by A27, A29, MATRIX_1:def_11 ;
hence (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) by A9, A24, MATRIX_1:def_11; ::_thesis: verum
end;
end;
end;
hence (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) ; ::_thesis: verum
end;
then 1. (K,n) is_col_circulant_about Col ((1. (K,n)),1) by A3, A4, Def4;
then consider p being FinSequence of K such that
A30: ( len p = len (1. (K,n)) & 1. (K,n) is_col_circulant_about p ) by A3, A4;
take p ; :: according to MATRIX16:def_5 ::_thesis: ( len p = len (1. (K,n)) & 1. (K,n) is_col_circulant_about p )
thus ( len p = len (1. (K,n)) & 1. (K,n) is_col_circulant_about p ) by A30; ::_thesis: verum
end;
theorem :: MATRIX16:40
for n being Element of NAT
for K being Field st n > 0 holds
1. (K,n) is line_circulant
proof
let n be Element of NAT ; ::_thesis: for K being Field st n > 0 holds
1. (K,n) is line_circulant
let K be Field; ::_thesis: ( n > 0 implies 1. (K,n) is line_circulant )
set M1 = 1. (K,n);
set p = Line ((1. (K,n)),1);
assume A1: n > 0 ; ::_thesis: 1. (K,n) is line_circulant
A2: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width (1. (K,n)) = n by MATRIX_1:24;
then A4: len (Line ((1. (K,n)),1)) = n by MATRIX_1:def_7;
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1) )
A5: (j - i) mod n >= 0 by A1, NAT_D:62;
then A6: ((j - i) mod n) + 1 in NAT by INT_1:3;
assume A7: [i,j] in Indices (1. (K,n)) ; ::_thesis: (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1)
then A8: j in Seg n by A2, ZFMISC_1:87;
then A9: 1 <= j by FINSEQ_1:1;
A10: j <= n by A8, FINSEQ_1:1;
A11: i in Seg n by A2, A7, ZFMISC_1:87;
then 1 <= i by FINSEQ_1:1;
then A12: j - i <= n - 1 by A10, XREAL_1:13;
n - 1 < n by XREAL_1:44;
then A13: j - i < n by A12, XXREAL_0:2;
i <= n by A11, FINSEQ_1:1;
then A14: 1 - n <= j - i by A9, XREAL_1:13;
- n <= (- n) + 1 by XREAL_1:29;
then A15: - n <= j - i by A14, XXREAL_0:2;
(j - i) mod n <= n - 1
proof
percases ( 0 <= j - i or 0 > j - i ) ;
suppose 0 <= j - i ; ::_thesis: (j - i) mod n <= n - 1
hence (j - i) mod n <= n - 1 by A12, A13, NAT_D:63; ::_thesis: verum
end;
supposeA16: 0 > j - i ; ::_thesis: (j - i) mod n <= n - 1
then j - i <= - 1 by INT_1:8;
then n + (j - i) <= n + (- 1) by XREAL_1:6;
hence (j - i) mod n <= n - 1 by A15, A16, NAT_D:63; ::_thesis: verum
end;
end;
end;
then A17: ((j - i) mod n) + 1 <= (n - 1) + 1 by XREAL_1:6;
((j - i) mod n) + 1 >= 0 + 1 by A5, XREAL_1:6;
then A18: ((j - i) mod n) + 1 in Seg n by A17, A6;
then A19: ((j - i) mod (len (Line ((1. (K,n)),1)))) + 1 in Seg n by A3, MATRIX_1:def_7;
(1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1)
proof
percases ( i = j or i <> j ) ;
supposeA20: i = j ; ::_thesis: (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1)
0 + 1 <= n by A1, NAT_1:13;
then 1 in Seg n ;
then A21: [1,1] in Indices (1. (K,n)) by A2, ZFMISC_1:87;
(j - i) mod (len (Line ((1. (K,n)),1))) = 0 by A1, A4, A20, NAT_D:63;
then (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1) = (1. (K,n)) * (1,1) by A3, A19, MATRIX_1:def_7
.= 1_ K by A21, MATRIX_1:def_11 ;
hence (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1) by A7, A20, MATRIX_1:def_11; ::_thesis: verum
end;
supposeA22: i <> j ; ::_thesis: (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1)
(j - i) mod n <> 0
proof
percases ( 0 <= j - i or 0 > j - i ) ;
suppose 0 <= j - i ; ::_thesis: (j - i) mod n <> 0
then (j - i) mod n = j - i by A13, NAT_D:63;
hence (j - i) mod n <> 0 by A22; ::_thesis: verum
end;
supposeA23: 0 > j - i ; ::_thesis: (j - i) mod n <> 0
(1 - n) + n <= (j - i) + n by A14, XREAL_1:6;
hence (j - i) mod n <> 0 by A15, A23, NAT_D:63; ::_thesis: verum
end;
end;
end;
then A24: ((j - i) mod (len (Line ((1. (K,n)),1)))) + 1 <> 1 by A3, MATRIX_1:def_7;
set l = ((j - i) mod (len (Line ((1. (K,n)),1)))) + 1;
reconsider l = ((j - i) mod (len (Line ((1. (K,n)),1)))) + 1 as Nat by A3, A6, MATRIX_1:def_7;
0 + 1 <= n by A1, NAT_1:13;
then A25: 1 in Seg n ;
l in Seg n by A3, A18, MATRIX_1:def_7;
then A26: [1,l] in Indices (1. (K,n)) by A2, A25, ZFMISC_1:87;
(Line ((1. (K,n)),1)) . l = (1. (K,n)) * (1,l) by A3, A19, MATRIX_1:def_7
.= 0. K by A24, A26, MATRIX_1:def_11 ;
hence (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1) by A7, A22, MATRIX_1:def_11; ::_thesis: verum
end;
end;
end;
hence (1. (K,n)) * (i,j) = (Line ((1. (K,n)),1)) . (((j - i) mod (len (Line ((1. (K,n)),1)))) + 1) ; ::_thesis: verum
end;
then 1. (K,n) is_line_circulant_about Line ((1. (K,n)),1) by A3, A4, Def1;
then consider p being FinSequence of K such that
A27: ( len p = width (1. (K,n)) & 1. (K,n) is_line_circulant_about p ) by A3, A4;
take p ; :: according to MATRIX16:def_2 ::_thesis: ( len p = width (1. (K,n)) & 1. (K,n) is_line_circulant_about p )
thus ( len p = width (1. (K,n)) & 1. (K,n) is_line_circulant_about p ) by A27; ::_thesis: verum
end;
theorem Th41: :: MATRIX16:41
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
a * p is first-line-of-circulant
proof
let K be Field; ::_thesis: for a being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
a * p is first-line-of-circulant
let a be Element of K; ::_thesis: for p being FinSequence of K st p is first-line-of-circulant holds
a * p is first-line-of-circulant
let p be FinSequence of K; ::_thesis: ( p is first-line-of-circulant implies a * p is first-line-of-circulant )
set n = len p;
A1: len (a * p) = len p by MATRIXR1:16;
assume p is first-line-of-circulant ; ::_thesis: a * p is first-line-of-circulant
then consider M1 being Matrix of len p,K such that
A2: M1 is_line_circulant_about p by Def3;
A3: Indices (a * M1) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A4: dom p = Seg (len p) by FINSEQ_1:def_3;
A5: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
A6: for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) )
assume A7: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
then A8: ((j - i) mod (len p)) + 1 in Seg (len p) by A3, Lm3;
then A9: ((j - i) mod (len p)) + 1 in dom (a * p) by A5, MATRIXR1:16;
A10: [i,j] in Indices M1 by A3, A7, MATRIX_1:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (((j - i) mod (len p)) + 1)) by A2, A10, Def1
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by A4, A8, PARTFUN1:def_6
.= a * (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * p) /. (((j - i) mod (len p)) + 1) by A4, A8, POLYNOM1:def_1
.= (a * p) . (((j - i) mod (len p)) + 1) by A9, PARTFUN1:def_6 ;
hence (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; ::_thesis: verum
end;
width (a * M1) = len p by MATRIX_1:24;
then a * M1 is_line_circulant_about a * p by A1, A6, Def1;
then consider M2 being Matrix of len (a * p),K such that
A11: M2 is_line_circulant_about a * p by A1;
take M2 ; :: according to MATRIX16:def_3 ::_thesis: M2 is_line_circulant_about a * p
thus M2 is_line_circulant_about a * p by A11; ::_thesis: verum
end;
theorem Th42: :: MATRIX16:42
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (a * p) = a * (LCirc p)
proof
let K be Field; ::_thesis: for a being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (a * p) = a * (LCirc p)
let a be Element of K; ::_thesis: for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (a * p) = a * (LCirc p)
let p be FinSequence of K; ::_thesis: ( p is first-line-of-circulant implies LCirc (a * p) = a * (LCirc p) )
set n = len p;
A1: len (a * p) = len p by MATRIXR1:16;
assume A2: p is first-line-of-circulant ; ::_thesis: LCirc (a * p) = a * (LCirc p)
then a * p is first-line-of-circulant by Th41;
then A3: LCirc (a * p) is_line_circulant_about a * p by Def7;
A4: Indices (LCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A5: LCirc p is_line_circulant_about p by A2, Def7;
A6: for i, j being Nat st [i,j] in Indices (LCirc p) holds
(LCirc (a * p)) * (i,j) = a * ((LCirc p) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (LCirc p) implies (LCirc (a * p)) * (i,j) = a * ((LCirc p) * (i,j)) )
A7: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
assume A8: [i,j] in Indices (LCirc p) ; ::_thesis: (LCirc (a * p)) * (i,j) = a * ((LCirc p) * (i,j))
then A9: ((j - i) mod (len p)) + 1 in Seg (len p) by A4, Lm3;
A10: dom p = Seg (len p) by FINSEQ_1:def_3;
[i,j] in Indices (LCirc (a * p)) by A1, A8, MATRIX_1:26;
then (LCirc (a * p)) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by A3, Def1
.= (a * p) /. (((j - i) mod (len p)) + 1) by A1, A9, A7, PARTFUN1:def_6
.= a * (p /. (((j - i) mod (len p)) + 1)) by A9, A10, POLYNOM1:def_1
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a multfield) . (p . (((j - i) mod (len p)) + 1)) by A9, A10, PARTFUN1:def_6
.= (a multfield) . ((LCirc p) * (i,j)) by A5, A8, Def1
.= a * ((LCirc p) * (i,j)) by FVSUM_1:49 ;
hence (LCirc (a * p)) * (i,j) = a * ((LCirc p) * (i,j)) ; ::_thesis: verum
end;
A11: ( len (LCirc p) = len p & width (LCirc p) = len p ) by MATRIX_1:24;
( len (LCirc (a * p)) = len p & width (LCirc (a * p)) = len p ) by A1, MATRIX_1:24;
hence LCirc (a * p) = a * (LCirc p) by A11, A6, MATRIX_3:def_5; ::_thesis: verum
end;
theorem :: MATRIX16:43
for K being Field
for a, b being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
(a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)
proof
let K be Field; ::_thesis: for a, b being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
(a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)
let a, b be Element of K; ::_thesis: for p being FinSequence of K st p is first-line-of-circulant holds
(a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)
let p be FinSequence of K; ::_thesis: ( p is first-line-of-circulant implies (a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p) )
A1: len (b * p) = len p by MATRIXR1:16;
A2: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
assume A3: p is first-line-of-circulant ; ::_thesis: (a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)
then A4: ( a * p is first-line-of-circulant & b * p is first-line-of-circulant ) by Th41;
( a * (LCirc p) = LCirc (a * p) & b * (LCirc p) = LCirc (b * p) ) by A3, Th42;
then (a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a * p) + (b * p)) by A4, A1, Th34, MATRIXR1:16;
hence (a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p) by A2, FVSUM_1:55; ::_thesis: verum
end;
theorem :: MATRIX16:44
for K being Field
for a being Element of K
for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
proof
let K be Field; ::_thesis: for a being Element of K
for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
let a be Element of K; ::_thesis: for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
let p, q be FinSequence of K; ::_thesis: ( p is first-line-of-circulant & q is first-line-of-circulant & len p = len q implies (a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q)) )
assume that
A1: ( p is first-line-of-circulant & q is first-line-of-circulant ) and
A2: len p = len q ; ::_thesis: (a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
A3: ( len (LCirc p) = len p & width (LCirc p) = len p ) by MATRIX_1:24;
( len (LCirc q) = len p & width (LCirc q) = len p ) by A2, MATRIX_1:24;
then (a * (LCirc p)) + (a * (LCirc q)) = a * ((LCirc p) + (LCirc q)) by A3, MATRIX_5:20
.= a * (LCirc (p + q)) by A1, A2, Th34
.= LCirc (a * (p + q)) by A1, A2, Th33, Th42 ;
hence (a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q)) ; ::_thesis: verum
end;
theorem :: MATRIX16:45
for K being Field
for a, b being Element of K
for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q))
proof
let K be Field; ::_thesis: for a, b being Element of K
for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q))
let a, b be Element of K; ::_thesis: for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q))
let p, q be FinSequence of K; ::_thesis: ( p is first-line-of-circulant & q is first-line-of-circulant & len p = len q implies (a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q)) )
set n = len p;
assume that
A1: p is first-line-of-circulant and
A2: q is first-line-of-circulant and
A3: len p = len q ; ::_thesis: (a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q))
A4: ( a * p is first-line-of-circulant & b * q is first-line-of-circulant ) by A1, A2, Th41;
A5: len (b * q) = len p by A3, MATRIXR1:16;
(a * (LCirc p)) + (b * (LCirc q)) = (LCirc (a * p)) + (b * (LCirc q)) by A1, Th42
.= (LCirc (a * p)) + (LCirc (b * q)) by A2, Th42
.= LCirc ((a * p) + (b * q)) by A4, A5, Th34, MATRIXR1:16 ;
hence (a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q)) ; ::_thesis: verum
end;
theorem Th46: :: MATRIX16:46
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
a * p is first-col-of-circulant
proof
let K be Field; ::_thesis: for a being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
a * p is first-col-of-circulant
let a be Element of K; ::_thesis: for p being FinSequence of K st p is first-col-of-circulant holds
a * p is first-col-of-circulant
let p be FinSequence of K; ::_thesis: ( p is first-col-of-circulant implies a * p is first-col-of-circulant )
set n = len p;
A1: len (a * p) = len p by MATRIXR1:16;
assume p is first-col-of-circulant ; ::_thesis: a * p is first-col-of-circulant
then consider M1 being Matrix of len p,K such that
A2: M1 is_col_circulant_about p by Def6;
A3: Indices (a * M1) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A4: dom p = Seg (len p) by FINSEQ_1:def_3;
A5: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
A6: for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) = (a * p) . (((i - j) mod (len (a * p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) = (a * p) . (((i - j) mod (len (a * p))) + 1) )
assume A7: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) = (a * p) . (((i - j) mod (len (a * p))) + 1)
then A8: ((i - j) mod (len p)) + 1 in Seg (len p) by A3, Lm3;
then A9: ((i - j) mod (len p)) + 1 in dom (a * p) by A5, MATRIXR1:16;
A10: [i,j] in Indices M1 by A3, A7, MATRIX_1:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (((i - j) mod (len p)) + 1)) by A2, A10, Def4
.= (a multfield) . (p /. (((i - j) mod (len p)) + 1)) by A4, A8, PARTFUN1:def_6
.= a * (p /. (((i - j) mod (len p)) + 1)) by FVSUM_1:49
.= (a * p) /. (((i - j) mod (len p)) + 1) by A4, A8, POLYNOM1:def_1
.= (a * p) . (((i - j) mod (len p)) + 1) by A9, PARTFUN1:def_6 ;
hence (a * M1) * (i,j) = (a * p) . (((i - j) mod (len (a * p))) + 1) by MATRIXR1:16; ::_thesis: verum
end;
len (a * M1) = len p by MATRIX_1:24;
then a * M1 is_col_circulant_about a * p by A1, A6, Def4;
then consider M2 being Matrix of len (a * p),K such that
A11: M2 is_col_circulant_about a * p by A1;
take M2 ; :: according to MATRIX16:def_6 ::_thesis: M2 is_col_circulant_about a * p
thus M2 is_col_circulant_about a * p by A11; ::_thesis: verum
end;
theorem Th47: :: MATRIX16:47
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (a * p) = a * (CCirc p)
proof
let K be Field; ::_thesis: for a being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (a * p) = a * (CCirc p)
let a be Element of K; ::_thesis: for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (a * p) = a * (CCirc p)
let p be FinSequence of K; ::_thesis: ( p is first-col-of-circulant implies CCirc (a * p) = a * (CCirc p) )
set n = len p;
A1: len (a * p) = len p by MATRIXR1:16;
assume A2: p is first-col-of-circulant ; ::_thesis: CCirc (a * p) = a * (CCirc p)
then a * p is first-col-of-circulant by Th46;
then A3: CCirc (a * p) is_col_circulant_about a * p by Def8;
A4: Indices (CCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A5: CCirc p is_col_circulant_about p by A2, Def8;
A6: for i, j being Nat st [i,j] in Indices (CCirc p) holds
(CCirc (a * p)) * (i,j) = a * ((CCirc p) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (CCirc p) implies (CCirc (a * p)) * (i,j) = a * ((CCirc p) * (i,j)) )
A7: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
assume A8: [i,j] in Indices (CCirc p) ; ::_thesis: (CCirc (a * p)) * (i,j) = a * ((CCirc p) * (i,j))
then A9: ((i - j) mod (len p)) + 1 in Seg (len p) by A4, Lm3;
A10: dom p = Seg (len p) by FINSEQ_1:def_3;
[i,j] in Indices (CCirc (a * p)) by A1, A8, MATRIX_1:26;
then (CCirc (a * p)) * (i,j) = (a * p) . (((i - j) mod (len (a * p))) + 1) by A3, Def4
.= (a * p) /. (((i - j) mod (len p)) + 1) by A1, A9, A7, PARTFUN1:def_6
.= a * (p /. (((i - j) mod (len p)) + 1)) by A9, A10, POLYNOM1:def_1
.= (a multfield) . (p /. (((i - j) mod (len p)) + 1)) by FVSUM_1:49
.= (a multfield) . (p . (((i - j) mod (len p)) + 1)) by A9, A10, PARTFUN1:def_6
.= (a multfield) . ((CCirc p) * (i,j)) by A5, A8, Def4
.= a * ((CCirc p) * (i,j)) by FVSUM_1:49 ;
hence (CCirc (a * p)) * (i,j) = a * ((CCirc p) * (i,j)) ; ::_thesis: verum
end;
A11: ( len (CCirc p) = len p & width (CCirc p) = len p ) by MATRIX_1:24;
( len (CCirc (a * p)) = len p & width (CCirc (a * p)) = len p ) by A1, MATRIX_1:24;
hence CCirc (a * p) = a * (CCirc p) by A11, A6, MATRIX_3:def_5; ::_thesis: verum
end;
theorem :: MATRIX16:48
for K being Field
for a, b being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
(a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p)
proof
let K be Field; ::_thesis: for a, b being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
(a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p)
let a, b be Element of K; ::_thesis: for p being FinSequence of K st p is first-col-of-circulant holds
(a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p)
let p be FinSequence of K; ::_thesis: ( p is first-col-of-circulant implies (a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p) )
A1: len (b * p) = len p by MATRIXR1:16;
A2: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
assume A3: p is first-col-of-circulant ; ::_thesis: (a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p)
then A4: ( a * p is first-col-of-circulant & b * p is first-col-of-circulant ) by Th46;
( a * (CCirc p) = CCirc (a * p) & b * (CCirc p) = CCirc (b * p) ) by A3, Th47;
then (a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a * p) + (b * p)) by A4, A1, Th38, MATRIXR1:16;
hence (a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p) by A2, FVSUM_1:55; ::_thesis: verum
end;
theorem :: MATRIX16:49
for K being Field
for a being Element of K
for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 holds
(a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))
proof
let K be Field; ::_thesis: for a being Element of K
for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 holds
(a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))
let a be Element of K; ::_thesis: for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 holds
(a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))
let p, q be FinSequence of K; ::_thesis: ( p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 implies (a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q)) )
assume that
A1: ( p is first-col-of-circulant & q is first-col-of-circulant ) and
A2: len p = len q ; ::_thesis: ( not len p > 0 or (a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q)) )
A3: ( len (CCirc p) = len p & width (CCirc p) = len p ) by MATRIX_1:24;
( len (CCirc q) = len p & width (CCirc q) = len p ) by A2, MATRIX_1:24;
then (a * (CCirc p)) + (a * (CCirc q)) = a * ((CCirc p) + (CCirc q)) by A3, MATRIX_5:20
.= a * (CCirc (p + q)) by A1, A2, Th38
.= CCirc (a * (p + q)) by A1, A2, Th37, Th47 ;
hence ( not len p > 0 or (a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q)) ) ; ::_thesis: verum
end;
theorem :: MATRIX16:50
for K being Field
for a, b being Element of K
for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds
(a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q))
proof
let K be Field; ::_thesis: for a, b being Element of K
for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds
(a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q))
let a, b be Element of K; ::_thesis: for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds
(a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q))
let p, q be FinSequence of K; ::_thesis: ( p is first-col-of-circulant & q is first-col-of-circulant & len p = len q implies (a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q)) )
set n = len p;
assume that
A1: p is first-col-of-circulant and
A2: q is first-col-of-circulant and
A3: len p = len q ; ::_thesis: (a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q))
A4: ( a * p is first-col-of-circulant & b * q is first-col-of-circulant ) by A1, A2, Th46;
A5: len (b * q) = len p by A3, MATRIXR1:16;
(a * (CCirc p)) + (b * (CCirc q)) = (CCirc (a * p)) + (b * (CCirc q)) by A1, Th47
.= (CCirc (a * p)) + (CCirc (b * q)) by A2, Th47
.= CCirc ((a * p) + (b * q)) by A4, A5, Th38, MATRIXR1:16 ;
hence (a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q)) ; ::_thesis: verum
end;
notation
let K be set ;
let M be Matrix of K;
synonym circulant M for line_circulant ;
end;
begin
definition
let K be Field;
let M1 be Matrix of K;
let p be FinSequence of K;
predM1 is_anti-circular_about p means :Def9: :: MATRIX16:def 9
( len p = width M1 & ( for i, j being Nat st [i,j] in Indices M1 & i <= j holds
M1 * (i,j) = p . (((j - i) mod (len p)) + 1) ) & ( for i, j being Nat st [i,j] in Indices M1 & i >= j holds
M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) ) );
end;
:: deftheorem Def9 defines is_anti-circular_about MATRIX16:def_9_:_
for K being Field
for M1 being Matrix of K
for p being FinSequence of K holds
( M1 is_anti-circular_about p iff ( len p = width M1 & ( for i, j being Nat st [i,j] in Indices M1 & i <= j holds
M1 * (i,j) = p . (((j - i) mod (len p)) + 1) ) & ( for i, j being Nat st [i,j] in Indices M1 & i >= j holds
M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) ) ) );
definition
let K be Field;
let M be Matrix of K;
attrM is anti-circular means :Def10: :: MATRIX16:def 10
ex p being FinSequence of K st
( len p = width M & M is_anti-circular_about p );
end;
:: deftheorem Def10 defines anti-circular MATRIX16:def_10_:_
for K being Field
for M being Matrix of K holds
( M is anti-circular iff ex p being FinSequence of K st
( len p = width M & M is_anti-circular_about p ) );
definition
let K be Field;
let p be FinSequence of K;
attrp is first-line-of-anti-circular means :Def11: :: MATRIX16:def 11
ex M being Matrix of len p,K st M is_anti-circular_about p;
end;
:: deftheorem Def11 defines first-line-of-anti-circular MATRIX16:def_11_:_
for K being Field
for p being FinSequence of K holds
( p is first-line-of-anti-circular iff ex M being Matrix of len p,K st M is_anti-circular_about p );
definition
let K be Field;
let p be FinSequence of K;
assume A1: p is first-line-of-anti-circular ;
func ACirc p -> Matrix of len p,K means :Def12: :: MATRIX16:def 12
it is_anti-circular_about p;
existence
ex b1 being Matrix of len p,K st b1 is_anti-circular_about p by A1, Def11;
uniqueness
for b1, b2 being Matrix of len p,K st b1 is_anti-circular_about p & b2 is_anti-circular_about p holds
b1 = b2
proof
let M1, M2 be Matrix of len p,K; ::_thesis: ( M1 is_anti-circular_about p & M2 is_anti-circular_about p implies M1 = M2 )
assume that
A2: M1 is_anti-circular_about p and
A3: M2 is_anti-circular_about p ; ::_thesis: M1 = M2
A4: Indices M1 = Indices M2 by MATRIX_1:26;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A5: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
percases ( i <= j or i > j ) ;
supposeA6: i <= j ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then M1 * (i,j) = p . (((j - i) mod (len p)) + 1) by A2, A5, Def9;
hence M1 * (i,j) = M2 * (i,j) by A3, A4, A5, A6, Def9; ::_thesis: verum
end;
supposeA7: i > j ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) by A2, A5, Def9;
hence M1 * (i,j) = M2 * (i,j) by A3, A4, A5, A7, Def9; ::_thesis: verum
end;
end;
end;
hence M1 = M2 by MATRIX_1:27; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines ACirc MATRIX16:def_12_:_
for K being Field
for p being FinSequence of K st p is first-line-of-anti-circular holds
for b3 being Matrix of len p,K holds
( b3 = ACirc p iff b3 is_anti-circular_about p );
theorem :: MATRIX16:51
for n being Element of NAT
for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
proof
let n be Element of NAT ; ::_thesis: for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
let K be Field; ::_thesis: for a being Element of K
for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
let a be Element of K; ::_thesis: for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
let M1 be Matrix of n,K; ::_thesis: ( M1 is anti-circular implies a * M1 is anti-circular )
A1: Indices (a * M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume M1 is anti-circular ; ::_thesis: a * M1 is anti-circular
then consider p being FinSequence of K such that
A2: len p = width M1 and
A3: M1 is_anti-circular_about p by Def10;
A4: width M1 = n by MATRIX_1:24;
then A5: dom p = Seg n by A2, FINSEQ_1:def_3;
A6: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
A7: for i, j being Nat st [i,j] in Indices (a * M1) & i <= j holds
(a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) & i <= j implies (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) )
assume that
A8: [i,j] in Indices (a * M1) and
A9: i <= j ; ::_thesis: (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
A10: ((j - i) mod n) + 1 in Seg n by A1, A8, Lm3;
then A11: ((j - i) mod (len p)) + 1 in dom (a * p) by A2, A4, A6, MATRIXR1:16;
A12: [i,j] in Indices M1 by A1, A8, MATRIX_1:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (((j - i) mod (len p)) + 1)) by A3, A9, A12, Def9
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by A2, A4, A5, A10, PARTFUN1:def_6
.= a * (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * p) /. (((j - i) mod (len p)) + 1) by A2, A4, A5, A10, POLYNOM1:def_1
.= (a * p) . (((j - i) mod (len p)) + 1) by A11, PARTFUN1:def_6 ;
hence (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; ::_thesis: verum
end;
A13: width (a * M1) = n by MATRIX_1:24;
A14: len p = n by A2, MATRIX_1:24;
A15: len (a * p) = len p by MATRIXR1:16;
for i, j being Nat st [i,j] in Indices (a * M1) & i >= j holds
(a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1)
proof
len (a * (- p)) = len (- p) by MATRIXR1:16;
then A16: dom (a * (- p)) = Seg (len (- p)) by FINSEQ_1:def_3
.= dom (- p) by FINSEQ_1:def_3 ;
A17: a * p is Element of n -tuples_on the carrier of K by A15, A14, FINSEQ_2:92;
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) & i >= j implies (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) )
assume that
A18: [i,j] in Indices (a * M1) and
A19: i >= j ; ::_thesis: (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1)
A20: ((j - i) mod n) + 1 in Seg n by A1, A18, Lm3;
A21: p is Element of n -tuples_on the carrier of K by A14, FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by A14, FINSEQ_2:113;
then len (- p) = len p by CARD_1:def_7;
then A22: dom (- p) = Seg n by A2, A4, FINSEQ_1:def_3;
A23: [i,j] in Indices M1 by A1, A18, MATRIX_1:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . ((- p) . (((j - i) mod (len p)) + 1)) by A3, A19, A23, Def9
.= (a multfield) . ((- p) /. (((j - i) mod (len p)) + 1)) by A2, A4, A20, A22, PARTFUN1:def_6
.= a * ((- p) /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * (- p)) /. (((j - i) mod (len p)) + 1) by A2, A4, A20, A22, POLYNOM1:def_1
.= (a * (- p)) . (((j - i) mod (len p)) + 1) by A2, A4, A20, A22, A16, PARTFUN1:def_6
.= (a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1) by A21, FVSUM_1:59
.= ((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1) by A21, FVSUM_1:54
.= ((- (a * (1_ K))) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:8
.= ((- a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def_6
.= ((- ((1_ K) * a)) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def_6
.= (((- (1_ K)) * a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:9
.= ((- (1_ K)) * (a * p)) . (((j - i) mod (len p)) + 1) by A21, FVSUM_1:54
.= (- (a * p)) . (((j - i) mod (len p)) + 1) by A17, FVSUM_1:59 ;
hence (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; ::_thesis: verum
end;
then a * M1 is_anti-circular_about a * p by A13, A15, A14, A7, Def9;
then consider q being FinSequence of K such that
A24: ( len q = width (a * M1) & a * M1 is_anti-circular_about q ) by A2, A13, A15, MATRIX_1:24;
take q ; :: according to MATRIX16:def_10 ::_thesis: ( len q = width (a * M1) & a * M1 is_anti-circular_about q )
thus ( len q = width (a * M1) & a * M1 is_anti-circular_about q ) by A24; ::_thesis: verum
end;
theorem Th52: :: MATRIX16:52
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 + M2 is anti-circular
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 + M2 is anti-circular
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 + M2 is anti-circular
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is anti-circular & M2 is anti-circular implies M1 + M2 is anti-circular )
assume that
A1: M1 is anti-circular and
A2: M2 is anti-circular ; ::_thesis: M1 + M2 is anti-circular
consider p being FinSequence of K such that
A3: len p = width M1 and
A4: M1 is_anti-circular_about p by A1, Def10;
A5: width M1 = n by MATRIX_1:24;
then A6: dom p = Seg n by A3, FINSEQ_1:def_3;
consider q being FinSequence of K such that
A7: len q = width M2 and
A8: M2 is_anti-circular_about q by A2, Def10;
A9: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
A10: width M2 = n by MATRIX_1:24;
then dom q = Seg n by A7, FINSEQ_1:def_3;
then A11: dom (p + q) = dom p by A6, POLYNOM1:1;
then A12: len (p + q) = n by A6, FINSEQ_1:def_3;
A13: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then len (- p) = len p by CARD_1:def_7;
then A14: dom (- p) = Seg n by A3, A5, FINSEQ_1:def_3;
A15: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A16: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A17: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A18: q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:92;
then - q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:113;
then len (- q) = len q by CARD_1:def_7;
then A19: dom (- q) = Seg n by A7, A10, FINSEQ_1:def_3;
A20: for i, j being Nat st [i,j] in Indices (M1 + M2) & i >= j holds
(M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) & i >= j implies (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) )
assume that
A21: [i,j] in Indices (M1 + M2) and
A22: i >= j ; ::_thesis: (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
dom ((- p) + (- q)) = dom (- p) by A14, A19, POLYNOM1:1;
then A23: ((j - i) mod (len (p + q))) + 1 in dom ((- p) + (- q)) by A16, A6, A9, A14, A11, A21, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A17, A16, A21, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),((- q) . (((j - i) mod (len q)) + 1))) by A8, A15, A16, A21, A22, Def9
.= the addF of K . (((- p) . (((j - i) mod (len (p + q))) + 1)),((- q) . (((j - i) mod (len (p + q))) + 1))) by A3, A4, A7, A17, A5, A10, A16, A12, A21, A22, Def9
.= ((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1) by A23, FUNCOP_1:22
.= (- (p + q)) . (((j - i) mod (len (p + q))) + 1) by A3, A7, A13, A18, A5, A10, FVSUM_1:31 ;
hence (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) ; ::_thesis: verum
end;
A24: width (M1 + M2) = n by MATRIX_1:24;
for i, j being Nat st [i,j] in Indices (M1 + M2) & i <= j holds
(M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) & i <= j implies (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) )
assume that
A25: [i,j] in Indices (M1 + M2) and
A26: i <= j ; ::_thesis: (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
A27: ((j - i) mod (len (p + q))) + 1 in dom (p + q) by A16, A6, A9, A11, A25, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A17, A16, A25, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),(q . (((j - i) mod (len q)) + 1))) by A8, A15, A16, A25, A26, Def9
.= the addF of K . ((p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1))) by A3, A4, A7, A17, A5, A10, A16, A12, A25, A26, Def9
.= (p + q) . (((j - i) mod (len (p + q))) + 1) by A27, FUNCOP_1:22 ;
hence (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) ; ::_thesis: verum
end;
then M1 + M2 is_anti-circular_about p + q by A24, A12, A20, Def9;
then consider r being FinSequence of K such that
A28: ( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r ) by A24, A12;
take r ; :: according to MATRIX16:def_10 ::_thesis: ( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r )
thus ( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r ) by A28; ::_thesis: verum
end;
theorem :: MATRIX16:53
for K being Fanoian Field
for n, i, j being Nat
for M1 being Matrix of n,K st [i,j] in Indices M1 & i = j & M1 is anti-circular holds
M1 * (i,j) = 0. K
proof
let K be Fanoian Field; ::_thesis: for n, i, j being Nat
for M1 being Matrix of n,K st [i,j] in Indices M1 & i = j & M1 is anti-circular holds
M1 * (i,j) = 0. K
let n, i, j be Nat; ::_thesis: for M1 being Matrix of n,K st [i,j] in Indices M1 & i = j & M1 is anti-circular holds
M1 * (i,j) = 0. K
let M1 be Matrix of n,K; ::_thesis: ( [i,j] in Indices M1 & i = j & M1 is anti-circular implies M1 * (i,j) = 0. K )
assume that
A1: [i,j] in Indices M1 and
A2: i = j and
A3: M1 is anti-circular ; ::_thesis: M1 * (i,j) = 0. K
consider p being FinSequence of K such that
A4: len p = width M1 and
A5: M1 is_anti-circular_about p by A3, Def10;
A6: M1 * (i,j) = p . (((j - i) mod (len p)) + 1) by A1, A2, A5, Def9;
A7: width M1 = n by MATRIX_1:24;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then len (- p) = len p by CARD_1:def_7;
then ( Indices M1 = [:(Seg n),(Seg n):] & dom (- p) = Seg n ) by A4, A7, FINSEQ_1:def_3, MATRIX_1:24;
then A8: ((j - i) mod (len p)) + 1 in dom (- p) by A1, A4, A7, Lm3;
M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) by A1, A2, A5, Def9
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A8, FUNCT_1:12
.= - (M1 * (i,j)) by A6, VECTSP_1:def_13 ;
then (M1 * (i,j)) + (M1 * (i,j)) = 0. K by RLVECT_1:5;
then ((1_ K) * (M1 * (i,j))) + (M1 * (i,j)) = 0. K by VECTSP_1:def_8;
then ((1_ K) * (M1 * (i,j))) + ((1_ K) * (M1 * (i,j))) = 0. K by VECTSP_1:def_8;
then ( (1_ K) + (1_ K) <> 0. K & ((1_ K) + (1_ K)) * (M1 * (i,j)) = 0. K ) by VECTSP_1:def_7, VECTSP_1:def_19;
hence M1 * (i,j) = 0. K by VECTSP_1:12; ::_thesis: verum
end;
theorem :: MATRIX16:54
for i, j, n, k, l being Element of NAT
for K being Field
for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
M1 * (k,l) = M1 * (i,j)
proof
let i, j, n, k, l be Element of NAT ; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
M1 * (k,l) = M1 * (i,j)
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
M1 * (k,l) = M1 * (i,j)
let M1 be Matrix of n,K; ::_thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )
now__::_thesis:_(_(_i_<=_j_&_(_M1_is_anti-circular_&_[i,j]_in_[:(Seg_n),(Seg_n):]_&_k_=_i_+_1_&_l_=_j_+_1_&_i_<_n_&_j_<_n_&_M1_is_anti-circular_&_[i,j]_in_[:(Seg_n),(Seg_n):]_&_k_=_i_+_1_&_l_=_j_+_1_&_i_<_n_&_j_<_n_implies_M1_*_(k,l)_=_M1_*_(i,j)_)_)_or_(_i_>=_j_&_(_M1_is_anti-circular_&_[i,j]_in_[:(Seg_n),(Seg_n):]_&_k_=_i_+_1_&_l_=_j_+_1_&_i_<_n_&_j_<_n_&_M1_is_anti-circular_&_[i,j]_in_[:(Seg_n),(Seg_n):]_&_k_=_i_+_1_&_l_=_j_+_1_&_i_<_n_&_j_<_n_implies_M1_*_(k,l)_=_M1_*_(i,j)_)_)_)
percases ( i <= j or i >= j ) ;
caseA1: i <= j ; ::_thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n & M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )
then A2: i + 1 <= j + 1 by XREAL_1:6;
A3: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume that
A4: M1 is anti-circular and
A5: [i,j] in [:(Seg n),(Seg n):] and
A6: k = i + 1 and
A7: l = j + 1 and
A8: i < n and
A9: j < n ; ::_thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )
j in Seg n by A5, ZFMISC_1:87;
then 1 <= j by FINSEQ_1:1;
then 1 + 1 <= j + 1 by XREAL_1:6;
then A10: 1 <= j + 1 by XXREAL_0:2;
j + 1 <= n by A9, INT_1:7;
then A11: l in Seg n by A7, A10;
i in Seg n by A5, ZFMISC_1:87;
then 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A12: 1 <= i + 1 by XXREAL_0:2;
consider p being FinSequence of K such that
len p = width M1 and
A13: M1 is_anti-circular_about p by A4, Def10;
i + 1 <= n by A8, INT_1:7;
then k in Seg n by A6, A12;
then [k,l] in Indices M1 by A3, A11, ZFMISC_1:87;
then M1 * (k,l) = p . (((l - k) mod (len p)) + 1) by A6, A7, A13, A2, Def9
.= p . (((j - i) mod (len p)) + 1) by A6, A7
.= M1 * (i,j) by A1, A5, A13, A3, Def9 ;
hence ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) ) ; ::_thesis: verum
end;
caseA14: i >= j ; ::_thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n & M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )
then A15: i + 1 >= j + 1 by XREAL_1:6;
A16: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume that
A17: M1 is anti-circular and
A18: [i,j] in [:(Seg n),(Seg n):] and
A19: k = i + 1 and
A20: l = j + 1 and
A21: i < n and
A22: j < n ; ::_thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) )
j in Seg n by A18, ZFMISC_1:87;
then 1 <= j by FINSEQ_1:1;
then 1 + 1 <= j + 1 by XREAL_1:6;
then A23: 1 <= j + 1 by XXREAL_0:2;
j + 1 <= n by A22, INT_1:7;
then A24: l in Seg n by A20, A23;
i in Seg n by A18, ZFMISC_1:87;
then 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A25: 1 <= i + 1 by XXREAL_0:2;
consider p being FinSequence of K such that
len p = width M1 and
A26: M1 is_anti-circular_about p by A17, Def10;
i + 1 <= n by A21, INT_1:7;
then k in Seg n by A19, A25;
then [k,l] in Indices M1 by A16, A24, ZFMISC_1:87;
then M1 * (k,l) = (- p) . (((l - k) mod (len p)) + 1) by A19, A20, A26, A15, Def9
.= (- p) . (((j - i) mod (len p)) + 1) by A19, A20
.= M1 * (i,j) by A14, A18, A26, A16, Def9 ;
hence ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) ) ; ::_thesis: verum
end;
end;
end;
hence ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * (k,l) = M1 * (i,j) ) ; ::_thesis: verum
end;
theorem Th55: :: MATRIX16:55
for n being Element of NAT
for K being Field
for M1 being Matrix of n,K st M1 is anti-circular holds
- M1 is anti-circular
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1 being Matrix of n,K st M1 is anti-circular holds
- M1 is anti-circular
let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is anti-circular holds
- M1 is anti-circular
let M1 be Matrix of n,K; ::_thesis: ( M1 is anti-circular implies - M1 is anti-circular )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume M1 is anti-circular ; ::_thesis: - M1 is anti-circular
then consider p being FinSequence of K such that
A2: len p = width M1 and
A3: M1 is_anti-circular_about p by Def10;
set r = - p;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then A4: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
A5: Indices (- M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: width M1 = n by MATRIX_1:24;
A7: for i, j being Nat st [i,j] in Indices (- M1) & i <= j holds
(- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) & i <= j implies (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) )
assume that
A8: [i,j] in Indices (- M1) and
A9: i <= j ; ::_thesis: (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
((j - i) mod n) + 1 in Seg n by A5, A8, Lm3;
then A10: ((j - i) mod (len p)) + 1 in dom p by A2, A6, FINSEQ_1:def_3;
(- M1) * (i,j) = - (M1 * (i,j)) by A1, A5, A8, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A3, A1, A5, A8, A9, Def9
.= (- p) . (((j - i) mod (len p)) + 1) by A10, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) by A4, CARD_1:def_7; ::_thesis: verum
end;
A11: width (- M1) = n by MATRIX_1:24;
A12: len (- p) = len p by A4, CARD_1:def_7;
then A13: dom (- p) = Seg (len p) by FINSEQ_1:def_3;
for i, j being Nat st [i,j] in Indices (- M1) & i >= j holds
(- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) & i >= j implies (- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1) )
assume that
A14: [i,j] in Indices (- M1) and
A15: i >= j ; ::_thesis: (- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1)
A16: ((j - i) mod n) + 1 in Seg n by A5, A14, Lm3;
(- M1) * (i,j) = - (M1 * (i,j)) by A1, A5, A14, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . ((- p) . (((j - i) mod (len p)) + 1)) by A3, A1, A5, A14, A15, Def9
.= (- (- p)) . (((j - i) mod (len p)) + 1) by A2, A6, A13, A16, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1) by A4, CARD_1:def_7; ::_thesis: verum
end;
then - M1 is_anti-circular_about - p by A2, A6, A11, A12, A7, Def9;
then consider r being FinSequence of K such that
A17: ( len r = width (- M1) & - M1 is_anti-circular_about r ) by A2, A11, A12, MATRIX_1:24;
take r ; :: according to MATRIX16:def_10 ::_thesis: ( len r = width (- M1) & - M1 is_anti-circular_about r )
thus ( len r = width (- M1) & - M1 is_anti-circular_about r ) by A17; ::_thesis: verum
end;
theorem :: MATRIX16:56
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 - M2 is anti-circular
proof
let n be Element of NAT ; ::_thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 - M2 is anti-circular
let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 - M2 is anti-circular
let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is anti-circular & M2 is anti-circular implies M1 - M2 is anti-circular )
assume that
A1: M1 is anti-circular and
A2: M2 is anti-circular ; ::_thesis: M1 - M2 is anti-circular
- M2 is anti-circular by A2, Th55;
hence M1 - M2 is anti-circular by A1, Th52; ::_thesis: verum
end;
theorem :: MATRIX16:57
for n being Element of NAT
for K being Field
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds
p = Line (M1,1)
proof
let n be Element of NAT ; ::_thesis: for K being Field
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds
p = Line (M1,1)
let K be Field; ::_thesis: for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds
p = Line (M1,1)
let p be FinSequence of K; ::_thesis: for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds
p = Line (M1,1)
let M1 be Matrix of n,K; ::_thesis: ( M1 is_anti-circular_about p & n > 0 implies p = Line (M1,1) )
assume that
A1: M1 is_anti-circular_about p and
A2: n > 0 ; ::_thesis: p = Line (M1,1)
A3: dom p = Seg (len p) by FINSEQ_1:def_3;
A4: width M1 = n by MATRIX_1:24;
then A5: len p = n by A1, Def9;
A6: for k being Nat st k in dom p holds
p . k = (Line (M1,1)) . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = (Line (M1,1)) . k )
assume A7: k in dom p ; ::_thesis: p . k = (Line (M1,1)) . k
then A8: 1 <= k by A3, FINSEQ_1:1;
n >= 0 + 1 by A2, INT_1:7;
then 1 in Seg n ;
then [1,k] in [:(Seg n),(Seg n):] by A3, A5, A7, ZFMISC_1:def_2;
then A9: [1,k] in Indices M1 by MATRIX_1:24;
A10: k <= n by A3, A5, A7, FINSEQ_1:1;
(Line (M1,1)) . k = M1 * (1,k) by A4, A3, A5, A7, MATRIX_1:def_7
.= p . (((k - 1) mod (len p)) + 1) by A1, A8, A9, Def9
.= p . (((k - 1) mod n) + 1) by A1, A4, Def9
.= p . ((k - 1) + 1) by A8, A10, Lm1 ;
hence p . k = (Line (M1,1)) . k ; ::_thesis: verum
end;
len (Line (M1,1)) = n by A4, MATRIX_1:def_7;
then dom (Line (M1,1)) = dom p by A3, A5, FINSEQ_1:def_3;
hence p = Line (M1,1) by A6, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th58: :: MATRIX16:58
for K being Field
for p being FinSequence of K st p is first-line-of-anti-circular holds
- p is first-line-of-anti-circular
proof
let K be Field; ::_thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
- p is first-line-of-anti-circular
let p be FinSequence of K; ::_thesis: ( p is first-line-of-anti-circular implies - p is first-line-of-anti-circular )
set n = len p;
assume p is first-line-of-anti-circular ; ::_thesis: - p is first-line-of-anti-circular
then consider M1 being Matrix of len p,K such that
A1: M1 is_anti-circular_about p by Def11;
set M2 = - M1;
A2: Indices M1 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A3: Indices (- M1) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then A4: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A5: len (- p) = len p by CARD_1:def_7;
then A6: dom (- p) = Seg (len p) by FINSEQ_1:def_3;
A7: for i, j being Nat st [i,j] in Indices (- M1) & i >= j holds
(- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) & i >= j implies (- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1) )
assume that
A8: [i,j] in Indices (- M1) and
A9: i >= j ; ::_thesis: (- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1)
A10: ((j - i) mod (len p)) + 1 in Seg (len p) by A3, A8, Lm3;
(- M1) * (i,j) = - (M1 * (i,j)) by A2, A3, A8, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . ((- p) . (((j - i) mod (len p)) + 1)) by A1, A2, A3, A8, A9, Def9
.= (- (- p)) . (((j - i) mod (len p)) + 1) by A6, A10, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1) by A4, CARD_1:def_7; ::_thesis: verum
end;
A11: for i, j being Nat st [i,j] in Indices (- M1) & i <= j holds
(- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) & i <= j implies (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) )
assume that
A12: [i,j] in Indices (- M1) and
A13: i <= j ; ::_thesis: (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
((j - i) mod (len p)) + 1 in Seg (len p) by A3, A12, Lm3;
then A14: ((j - i) mod (len p)) + 1 in dom p by FINSEQ_1:def_3;
(- M1) * (i,j) = - (M1 * (i,j)) by A2, A3, A12, MATRIX_3:def_2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def_13
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A1, A2, A3, A12, A13, Def9
.= (- p) . (((j - i) mod (len p)) + 1) by A14, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) by A4, CARD_1:def_7; ::_thesis: verum
end;
width (- M1) = len p by MATRIX_1:24;
then - M1 is_anti-circular_about - p by A5, A11, A7, Def9;
then consider M2 being Matrix of len (- p),K such that
A15: M2 is_anti-circular_about - p by A5;
take M2 ; :: according to MATRIX16:def_11 ::_thesis: M2 is_anti-circular_about - p
thus M2 is_anti-circular_about - p by A15; ::_thesis: verum
end;
theorem :: MATRIX16:59
for K being Field
for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (- p) = - (ACirc p)
proof
let K be Field; ::_thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (- p) = - (ACirc p)
let p be FinSequence of K; ::_thesis: ( p is first-line-of-anti-circular implies ACirc (- p) = - (ACirc p) )
set n = len p;
A1: ( len (ACirc p) = len p & width (ACirc p) = len p ) by MATRIX_1:24;
A2: Indices (ACirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A3: len (- p) = len p by CARD_1:def_7;
assume A4: p is first-line-of-anti-circular ; ::_thesis: ACirc (- p) = - (ACirc p)
then - p is first-line-of-anti-circular by Th58;
then A5: ACirc (- p) is_anti-circular_about - p by Def12;
A6: ACirc p is_anti-circular_about p by A4, Def12;
A7: for i, j being Nat st [i,j] in Indices (ACirc p) holds
(ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (ACirc p) implies (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) )
assume A8: [i,j] in Indices (ACirc p) ; ::_thesis: (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j))
now__::_thesis:_(_(_i_<=_j_&_(ACirc_(-_p))_*_(i,j)_=_-_((ACirc_p)_*_(i,j))_)_or_(_i_>=_j_&_(ACirc_(-_p))_*_(i,j)_=_-_((ACirc_p)_*_(i,j))_)_)
percases ( i <= j or i >= j ) ;
caseA9: i <= j ; ::_thesis: (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j))
((j - i) mod (len p)) + 1 in Seg (len p) by A2, A8, Lm3;
then A10: ((j - i) mod (len p)) + 1 in dom p by FINSEQ_1:def_3;
[i,j] in Indices (ACirc (- p)) by A3, A8, MATRIX_1:26;
then (ACirc (- p)) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) by A5, A9, Def9
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A3, A10, FUNCT_1:13
.= (comp K) . ((ACirc p) * (i,j)) by A6, A8, A9, Def9
.= - ((ACirc p) * (i,j)) by VECTSP_1:def_13 ;
hence (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) ; ::_thesis: verum
end;
caseA11: i >= j ; ::_thesis: (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j))
((j - i) mod (len p)) + 1 in Seg (len p) by A2, A8, Lm3;
then A12: ((j - i) mod (len p)) + 1 in dom (- p) by A3, FINSEQ_1:def_3;
[i,j] in Indices (ACirc (- p)) by A3, A8, MATRIX_1:26;
then (ACirc (- p)) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1) by A5, A11, Def9
.= (comp K) . ((- p) . (((j - i) mod (len p)) + 1)) by A3, A12, FUNCT_1:13
.= (comp K) . ((ACirc p) * (i,j)) by A6, A8, A11, Def9
.= - ((ACirc p) * (i,j)) by VECTSP_1:def_13 ;
hence (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) ; ::_thesis: verum
end;
end;
end;
hence (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) ; ::_thesis: verum
end;
( len (ACirc (- p)) = len p & width (ACirc (- p)) = len p ) by A3, MATRIX_1:24;
hence ACirc (- p) = - (ACirc p) by A1, A7, MATRIX_3:def_2; ::_thesis: verum
end;
theorem Th60: :: MATRIX16:60
for K being Field
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
p + q is first-line-of-anti-circular
proof
let K be Field; ::_thesis: for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
p + q is first-line-of-anti-circular
let p, q be FinSequence of K; ::_thesis: ( p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q implies p + q is first-line-of-anti-circular )
set n = len p;
assume that
A1: p is first-line-of-anti-circular and
A2: q is first-line-of-anti-circular and
A3: len p = len q ; ::_thesis: p + q is first-line-of-anti-circular
consider M2 being Matrix of len p,K such that
A4: M2 is_anti-circular_about q by A2, A3, Def11;
A5: width M2 = len p by MATRIX_1:24;
A6: dom p = Seg (len p) by FINSEQ_1:def_3;
len q = width M2 by A4, Def9;
then dom q = Seg (len p) by A5, FINSEQ_1:def_3;
then A7: dom (p + q) = dom p by A6, POLYNOM1:1;
then A8: len (p + q) = len p by A6, FINSEQ_1:def_3;
consider M1 being Matrix of len p,K such that
A9: M1 is_anti-circular_about p by A1, Def11;
A10: Indices M1 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
set M3 = M1 + M2;
A11: q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:92;
then - q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:113;
then A12: len (- q) = len q by CARD_1:def_7;
A13: Indices M2 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A14: Indices (M1 + M2) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A15: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
A16: for i, j being Nat st [i,j] in Indices (M1 + M2) & i <= j holds
(M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) & i <= j implies (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) )
assume that
A17: [i,j] in Indices (M1 + M2) and
A18: i <= j ; ::_thesis: (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
A19: ((j - i) mod (len (p + q))) + 1 in dom (p + q) by A14, A6, A15, A7, A17, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A10, A14, A17, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),(q . (((j - i) mod (len q)) + 1))) by A4, A13, A14, A17, A18, Def9
.= the addF of K . ((p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1))) by A3, A9, A10, A14, A8, A17, A18, Def9
.= (p + q) . (((j - i) mod (len (p + q))) + 1) by A19, FUNCOP_1:22 ;
hence (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) ; ::_thesis: verum
end;
A20: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A21: len (- p) = len p by CARD_1:def_7;
then A22: dom (- p) = Seg (len p) by FINSEQ_1:def_3;
A23: for i, j being Nat st [i,j] in Indices (M1 + M2) & i >= j holds
(M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) & i >= j implies (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) )
assume that
A24: [i,j] in Indices (M1 + M2) and
A25: i >= j ; ::_thesis: (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
( dom (- p) = Seg (len p) & dom (- q) = Seg (len q) ) by A21, A12, FINSEQ_1:def_3;
then dom ((- p) + (- q)) = dom (- p) by A3, POLYNOM1:1;
then A26: ((j - i) mod (len (p + q))) + 1 in dom ((- p) + (- q)) by A14, A6, A15, A22, A7, A24, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A10, A14, A24, MATRIX_3:def_3
.= the addF of K . ((M1 * (i,j)),((- q) . (((j - i) mod (len q)) + 1))) by A4, A13, A14, A24, A25, Def9
.= the addF of K . (((- p) . (((j - i) mod (len p)) + 1)),((- q) . (((j - i) mod (len q)) + 1))) by A9, A10, A14, A24, A25, Def9
.= ((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1) by A3, A8, A26, FUNCOP_1:22
.= (- (p + q)) . (((j - i) mod (len (p + q))) + 1) by A3, A20, A11, FVSUM_1:31 ;
hence (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) ; ::_thesis: verum
end;
width (M1 + M2) = len p by MATRIX_1:24;
then len (p + q) = width (M1 + M2) by A6, A7, FINSEQ_1:def_3;
then ( len (M1 + M2) = len p & M1 + M2 is_anti-circular_about p + q ) by A16, A23, Def9, MATRIX_1:24;
then consider M3 being Matrix of len (p + q),K such that
len (p + q) = len M3 and
A27: M3 is_anti-circular_about p + q by A8;
take M3 ; :: according to MATRIX16:def_11 ::_thesis: M3 is_anti-circular_about p + q
thus M3 is_anti-circular_about p + q by A27; ::_thesis: verum
end;
theorem Th61: :: MATRIX16:61
for K being Field
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
ACirc (p + q) = (ACirc p) + (ACirc q)
proof
let K be Field; ::_thesis: for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
ACirc (p + q) = (ACirc p) + (ACirc q)
let p, q be FinSequence of K; ::_thesis: ( p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q implies ACirc (p + q) = (ACirc p) + (ACirc q) )
set n = len p;
assume that
A1: p is first-line-of-anti-circular and
A2: q is first-line-of-anti-circular and
A3: len p = len q ; ::_thesis: ACirc (p + q) = (ACirc p) + (ACirc q)
A4: dom p = Seg (len p) by FINSEQ_1:def_3;
dom q = Seg (len p) by A3, FINSEQ_1:def_3;
then A5: dom (p + q) = dom p by A4, POLYNOM1:1;
then A6: len (p + q) = len p by A4, FINSEQ_1:def_3;
then A7: Indices (ACirc p) = Indices (ACirc (p + q)) by MATRIX_1:26;
A8: Indices (ACirc p) = Indices (ACirc q) by A3, MATRIX_1:26;
A9: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def_3;
A10: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A11: len (- p) = len p by CARD_1:def_7;
A12: Indices (ACirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
p + q is first-line-of-anti-circular by A1, A2, A3, Th60;
then A13: ACirc (p + q) is_anti-circular_about p + q by Def12;
A14: ACirc q is_anti-circular_about q by A2, Def12;
A15: q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:92;
then - q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:113;
then A16: len (- q) = len q by CARD_1:def_7;
A17: ACirc p is_anti-circular_about p by A1, Def12;
A18: Indices (ACirc q) = [:(Seg (len p)),(Seg (len p)):] by A3, MATRIX_1:24;
A19: for i, j being Nat st [i,j] in Indices (ACirc p) holds
(ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (ACirc p) implies (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) )
assume A20: [i,j] in Indices (ACirc p) ; ::_thesis: (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
then A21: ((j - i) mod (len p)) + 1 in Seg (len p) by A12, Lm3;
now__::_thesis:_(_(_i_<=_j_&_(ACirc_(p_+_q))_*_(i,j)_=_((ACirc_p)_*_(i,j))_+_((ACirc_q)_*_(i,j))_)_or_(_i_>=_j_&_(ACirc_(p_+_q))_*_(i,j)_=_((ACirc_p)_*_(i,j))_+_((ACirc_q)_*_(i,j))_)_)
percases ( i <= j or i >= j ) ;
caseA22: i <= j ; ::_thesis: (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
then (ACirc (p + q)) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) by A13, A7, A20, Def9
.= the addF of K . ((p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1))) by A9, A6, A21, FUNCOP_1:22
.= the addF of K . (((ACirc p) * (i,j)),(q . (((j - i) mod (len q)) + 1))) by A3, A6, A17, A20, A22, Def9
.= ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) by A14, A8, A20, A22, Def9 ;
hence (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) ; ::_thesis: verum
end;
caseA23: i >= j ; ::_thesis: (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
A24: dom (- p) = Seg (len p) by A11, FINSEQ_1:def_3;
dom (- q) = Seg (len q) by A16, FINSEQ_1:def_3;
then ( dom p = Seg (len p) & dom ((- p) + (- q)) = dom (- p) ) by A3, A24, FINSEQ_1:def_3, POLYNOM1:1;
then A25: ((j - i) mod (len (p + q))) + 1 in dom ((- p) + (- q)) by A9, A5, A12, A20, A24, Lm3;
(ACirc (p + q)) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) by A13, A7, A20, A23, Def9
.= ((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1) by A3, A10, A15, FVSUM_1:31
.= the addF of K . (((- p) . (((j - i) mod (len (p + q))) + 1)),((- q) . (((j - i) mod (len (p + q))) + 1))) by A25, FUNCOP_1:22
.= the addF of K . (((ACirc p) * (i,j)),((- q) . (((j - i) mod (len q)) + 1))) by A3, A6, A17, A20, A23, Def9
.= ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) by A14, A12, A18, A20, A23, Def9 ;
hence (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) ; ::_thesis: verum
end;
end;
end;
hence (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) ; ::_thesis: verum
end;
A26: ( len (ACirc p) = len p & width (ACirc p) = len p ) by MATRIX_1:24;
( len (ACirc (p + q)) = len p & width (ACirc (p + q)) = len p ) by A6, MATRIX_1:24;
hence ACirc (p + q) = (ACirc p) + (ACirc q) by A26, A19, MATRIX_3:def_3; ::_thesis: verum
end;
theorem Th62: :: MATRIX16:62
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
a * p is first-line-of-anti-circular
proof
let K be Field; ::_thesis: for a being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
a * p is first-line-of-anti-circular
let a be Element of K; ::_thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
a * p is first-line-of-anti-circular
let p be FinSequence of K; ::_thesis: ( p is first-line-of-anti-circular implies a * p is first-line-of-anti-circular )
set n = len p;
A1: dom p = Seg (len p) by FINSEQ_1:def_3;
assume p is first-line-of-anti-circular ; ::_thesis: a * p is first-line-of-anti-circular
then consider M1 being Matrix of len p,K such that
A2: M1 is_anti-circular_about p by Def11;
A3: Indices (a * M1) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A4: len (a * p) = len p by MATRIXR1:16;
A5: for i, j being Nat st [i,j] in Indices (a * M1) & i >= j holds
(a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1)
proof
len (a * (- p)) = len (- p) by MATRIXR1:16;
then A6: dom (a * (- p)) = Seg (len (- p)) by FINSEQ_1:def_3
.= dom (- p) by FINSEQ_1:def_3 ;
A7: a * p is Element of (len p) -tuples_on the carrier of K by A4, FINSEQ_2:92;
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) & i >= j implies (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) )
assume that
A8: [i,j] in Indices (a * M1) and
A9: i >= j ; ::_thesis: (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1)
A10: ((j - i) mod (len p)) + 1 in Seg (len p) by A3, A8, Lm3;
A11: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then len (- p) = len p by CARD_1:def_7;
then A12: dom (- p) = Seg (len p) by FINSEQ_1:def_3;
A13: [i,j] in Indices M1 by A3, A8, MATRIX_1:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . ((- p) . (((j - i) mod (len p)) + 1)) by A2, A9, A13, Def9
.= (a multfield) . ((- p) /. (((j - i) mod (len p)) + 1)) by A10, A12, PARTFUN1:def_6
.= a * ((- p) /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * (- p)) /. (((j - i) mod (len p)) + 1) by A10, A12, POLYNOM1:def_1
.= (a * (- p)) . (((j - i) mod (len p)) + 1) by A10, A12, A6, PARTFUN1:def_6
.= (a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1) by A11, FVSUM_1:59
.= ((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1) by A11, FVSUM_1:54
.= ((- (a * (1_ K))) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:8
.= ((- a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def_6
.= ((- ((1_ K) * a)) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def_6
.= (((- (1_ K)) * a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:9
.= ((- (1_ K)) * (a * p)) . (((j - i) mod (len p)) + 1) by A11, FVSUM_1:54
.= (- (a * p)) . (((j - i) mod (len p)) + 1) by A7, FVSUM_1:59 ;
hence (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; ::_thesis: verum
end;
A14: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
A15: for i, j being Nat st [i,j] in Indices (a * M1) & i <= j holds
(a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) & i <= j implies (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) )
assume that
A16: [i,j] in Indices (a * M1) and
A17: i <= j ; ::_thesis: (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
A18: ((j - i) mod (len p)) + 1 in Seg (len p) by A3, A16, Lm3;
then A19: ((j - i) mod (len p)) + 1 in dom (a * p) by A14, MATRIXR1:16;
A20: [i,j] in Indices M1 by A3, A16, MATRIX_1:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def_5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (((j - i) mod (len p)) + 1)) by A2, A17, A20, Def9
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by A1, A18, PARTFUN1:def_6
.= a * (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * p) /. (((j - i) mod (len p)) + 1) by A1, A18, POLYNOM1:def_1
.= (a * p) . (((j - i) mod (len p)) + 1) by A19, PARTFUN1:def_6 ;
hence (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; ::_thesis: verum
end;
width (a * M1) = len p by MATRIX_1:24;
then a * M1 is_anti-circular_about a * p by A4, A15, A5, Def9;
then consider M2 being Matrix of len (a * p),K such that
A21: M2 is_anti-circular_about a * p by A4;
take M2 ; :: according to MATRIX16:def_11 ::_thesis: M2 is_anti-circular_about a * p
thus M2 is_anti-circular_about a * p by A21; ::_thesis: verum
end;
theorem Th63: :: MATRIX16:63
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (a * p) = a * (ACirc p)
proof
let K be Field; ::_thesis: for a being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (a * p) = a * (ACirc p)
let a be Element of K; ::_thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (a * p) = a * (ACirc p)
let p be FinSequence of K; ::_thesis: ( p is first-line-of-anti-circular implies ACirc (a * p) = a * (ACirc p) )
set n = len p;
A1: len (a * p) = len p by MATRIXR1:16;
assume A2: p is first-line-of-anti-circular ; ::_thesis: ACirc (a * p) = a * (ACirc p)
then A3: ACirc p is_anti-circular_about p by Def12;
a * p is first-line-of-anti-circular by A2, Th62;
then A4: ACirc (a * p) is_anti-circular_about a * p by Def12;
A5: Indices (ACirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:24;
A6: for i, j being Nat st [i,j] in Indices (ACirc p) holds
(ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (ACirc p) implies (ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j)) )
assume A7: [i,j] in Indices (ACirc p) ; ::_thesis: (ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j))
then A8: ((j - i) mod (len p)) + 1 in Seg (len p) by A5, Lm3;
A9: [i,j] in Indices (ACirc (a * p)) by A1, A7, MATRIX_1:26;
now__::_thesis:_(_(_i_<=_j_&_(ACirc_(a_*_p))_*_(i,j)_=_a_*_((ACirc_p)_*_(i,j))_)_or_(_i_>=_j_&_(ACirc_(a_*_p))_*_(i,j)_=_a_*_((ACirc_p)_*_(i,j))_)_)
percases ( i <= j or i >= j ) ;
caseA10: i <= j ; ::_thesis: (ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j))
A11: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def_3;
A12: dom p = Seg (len p) by FINSEQ_1:def_3;
(ACirc (a * p)) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by A4, A9, A10, Def9
.= (a * p) /. (((j - i) mod (len p)) + 1) by A1, A8, A11, PARTFUN1:def_6
.= a * (p /. (((j - i) mod (len p)) + 1)) by A8, A12, POLYNOM1:def_1
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a multfield) . (p . (((j - i) mod (len p)) + 1)) by A8, A12, PARTFUN1:def_6
.= (a multfield) . ((ACirc p) * (i,j)) by A3, A7, A10, Def9
.= a * ((ACirc p) * (i,j)) by FVSUM_1:49 ;
hence (ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j)) ; ::_thesis: verum
end;
caseA13: i >= j ; ::_thesis: (ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j))
len (a * (- p)) = len (- p) by MATRIXR1:16;
then A14: dom (a * (- p)) = Seg (len (- p)) by FINSEQ_1:def_3
.= dom (- p) by FINSEQ_1:def_3 ;
A15: a * p is Element of (len p) -tuples_on the carrier of K by A1, FINSEQ_2:92;
A16: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then len (- p) = len p by CARD_1:def_7;
then A17: dom (- p) = Seg (len p) by FINSEQ_1:def_3;
a * ((ACirc p) * (i,j)) = (a multfield) . ((ACirc p) * (i,j)) by FVSUM_1:49
.= (a multfield) . ((- p) . (((j - i) mod (len p)) + 1)) by A3, A7, A13, Def9
.= (a multfield) . ((- p) /. (((j - i) mod (len p)) + 1)) by A8, A17, PARTFUN1:def_6
.= a * ((- p) /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * (- p)) /. (((j - i) mod (len p)) + 1) by A8, A17, POLYNOM1:def_1
.= (a * (- p)) . (((j - i) mod (len p)) + 1) by A8, A17, A14, PARTFUN1:def_6
.= (a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1) by A16, FVSUM_1:59
.= ((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1) by A16, FVSUM_1:54
.= ((- (a * (1_ K))) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:8
.= ((- a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def_6
.= ((- ((1_ K) * a)) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def_6
.= (((- (1_ K)) * a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:9
.= ((- (1_ K)) * (a * p)) . (((j - i) mod (len p)) + 1) by A16, FVSUM_1:54
.= (- (a * p)) . (((j - i) mod (len p)) + 1) by A15, FVSUM_1:59
.= (ACirc (a * p)) * (i,j) by A1, A4, A9, A13, Def9 ;
hence (ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j)) ; ::_thesis: verum
end;
end;
end;
hence (ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j)) ; ::_thesis: verum
end;
A18: ( len (ACirc p) = len p & width (ACirc p) = len p ) by MATRIX_1:24;
( len (ACirc (a * p)) = len p & width (ACirc (a * p)) = len p ) by A1, MATRIX_1:24;
hence ACirc (a * p) = a * (ACirc p) by A18, A6, MATRIX_3:def_5; ::_thesis: verum
end;
theorem :: MATRIX16:64
for K being Field
for a, b being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
(a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)
proof
let K be Field; ::_thesis: for a, b being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
(a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)
let a, b be Element of K; ::_thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
(a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)
let p be FinSequence of K; ::_thesis: ( p is first-line-of-anti-circular implies (a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p) )
A1: len (b * p) = len p by MATRIXR1:16;
A2: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
assume A3: p is first-line-of-anti-circular ; ::_thesis: (a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)
then A4: ( a * p is first-line-of-anti-circular & b * p is first-line-of-anti-circular ) by Th62;
(a * (ACirc p)) + (b * (ACirc p)) = (ACirc (a * p)) + (b * (ACirc p)) by A3, Th63
.= (ACirc (a * p)) + (ACirc (b * p)) by A3, Th63
.= ACirc ((a * p) + (b * p)) by A4, A1, Th61, MATRIXR1:16 ;
hence (a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p) by A2, FVSUM_1:55; ::_thesis: verum
end;
theorem :: MATRIX16:65
for K being Field
for a being Element of K
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q))
proof
let K be Field; ::_thesis: for a being Element of K
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q))
let a be Element of K; ::_thesis: for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q))
let p, q be FinSequence of K; ::_thesis: ( p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q implies (a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q)) )
assume that
A1: ( p is first-line-of-anti-circular & q is first-line-of-anti-circular ) and
A2: len p = len q ; ::_thesis: (a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q))
A3: ( len (ACirc p) = len p & width (ACirc p) = len p ) by MATRIX_1:24;
( len (ACirc q) = len p & width (ACirc q) = len p ) by A2, MATRIX_1:24;
then (a * (ACirc p)) + (a * (ACirc q)) = a * ((ACirc p) + (ACirc q)) by A3, MATRIX_5:20
.= a * (ACirc (p + q)) by A1, A2, Th61
.= ACirc (a * (p + q)) by A1, A2, Th60, Th63 ;
hence (a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q)) ; ::_thesis: verum
end;
theorem :: MATRIX16:66
for K being Field
for a, b being Element of K
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))
proof
let K be Field; ::_thesis: for a, b being Element of K
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))
let a, b be Element of K; ::_thesis: for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))
let p, q be FinSequence of K; ::_thesis: ( p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q implies (a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q)) )
set n = len p;
assume that
A1: p is first-line-of-anti-circular and
A2: q is first-line-of-anti-circular and
A3: len p = len q ; ::_thesis: (a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))
A4: ( a * p is first-line-of-anti-circular & b * q is first-line-of-anti-circular ) by A1, A2, Th62;
A5: len (b * q) = len p by A3, MATRIXR1:16;
(a * (ACirc p)) + (b * (ACirc q)) = (ACirc (a * p)) + (b * (ACirc q)) by A1, Th63
.= (ACirc (a * p)) + (ACirc (b * q)) by A2, Th63
.= ACirc ((a * p) + (b * q)) by A4, A5, Th61, MATRIXR1:16 ;
hence (a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q)) ; ::_thesis: verum
end;
registration
let K be Field;
let n be Element of NAT ;
cluster 0. (K,n) -> anti-circular ;
coherence
0. (K,n) is anti-circular
proof
set p = n |-> (0. K);
A1: width (0. (K,n)) = n by MATRIX_1:24;
A2: 0. (K,n,n) = n |-> (n |-> (0. K)) ;
set M1 = 0. (K,n);
A3: len (n |-> (0. K)) = n by CARD_1:def_7;
A4: Indices (0. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: for i, j being Nat st [i,j] in Indices (0. (K,n)) & i >= j holds
(0. (K,n)) * (i,j) = (- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (0. (K,n)) & i >= j implies (0. (K,n)) * (i,j) = (- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1) )
assume that
A6: [i,j] in Indices (0. (K,n)) and
i >= j ; ::_thesis: (0. (K,n)) * (i,j) = (- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1)
A7: ((j - i) mod n) + 1 in Seg n by A4, A6, Lm3;
(- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1) = (n |-> (- (0. K))) . (((j - i) mod n) + 1) by A3, FVSUM_1:25
.= - (0. K) by A7, FUNCOP_1:7
.= 0. K by VECTSP_2:3 ;
hence (0. (K,n)) * (i,j) = (- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1) by A2, A6, MATRIX_3:1; ::_thesis: verum
end;
for i, j being Nat st [i,j] in Indices (0. (K,n)) & i <= j holds
(0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (0. (K,n)) & i <= j implies (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) )
assume that
A8: [i,j] in Indices (0. (K,n)) and
i <= j ; ::_thesis: (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)
((j - i) mod n) + 1 in Seg n by A4, A8, Lm3;
then ((Seg n) --> (0. K)) . (((j - i) mod n) + 1) = 0. K by FUNCOP_1:7;
hence (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) by A3, A2, A8, MATRIX_3:1; ::_thesis: verum
end;
then 0. (K,n) is_anti-circular_about n |-> (0. K) by A1, A3, A5, Def9;
then consider p being FinSequence of K such that
A9: ( len p = width (0. (K,n)) & 0. (K,n) is_anti-circular_about p ) by A1, A3;
take p ; :: according to MATRIX16:def_10 ::_thesis: ( len p = width (0. (K,n)) & 0. (K,n) is_anti-circular_about p )
thus ( len p = width (0. (K,n)) & 0. (K,n) is_anti-circular_about p ) by A9; ::_thesis: verum
end;
end;