:: 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;