:: Sum and Product of Finite Sequences of Elements of a Field
::  by Katarzyna Zawadzka
::
:: Received December 29, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, RLVECT_1, XBOOLE_0, ALGSTR_0, BINOP_1,
      FUNCT_1, ARYTM_3, RELAT_1, VECTSP_1, MESFUNC1, ALGSTR_1, SUPINF_2,
      SETWISEO, LATTICES, STRUCT_0, FUNCOP_1, ARYTM_1, FINSEQOP, FINSEQ_1,
      FINSEQ_2, TARSKI, RVSUM_1, ORDINAL4, XXREAL_0, NAT_1, CARD_3, FINSUB_1,
      FINSEQ_4, SETWOP_2, FINSET_1, CARD_1, PARTFUN1, FINSOP_1, GROUP_1,
      FVSUM_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
      RELAT_1, FUNCT_1, STRUCT_0, ALGSTR_0, PARTFUN1, FUNCT_2, NAT_1, FINSEQ_1,
      FINSEQ_4, BINOP_1, FUNCOP_1, RLVECT_1, SETWISEO, FINSOP_1, FINSEQ_2,
      FINSEQOP, SETWOP_2, GROUP_1, ALGSTR_1, GROUP_4, VECTSP_1, FINSET_1,
      FINSUB_1, MATRIX_1, XXREAL_0;
 constructors PARTFUN1, BINOP_1, SETWISEO, SQUARE_1, NAT_1, FINSEQOP, FINSEQ_4,
      FINSOP_1, SETWOP_2, ALGSTR_1, GROUP_4, MATRIX_1, RELSET_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1,
      FINSUB_1, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1,
      ALGSTR_1, CARD_1, GROUP_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET;


begin :: Auxiliary theorems

reserve i,j,k for Nat;

theorem :: FVSUM_1:1
  for K being Abelian non empty addLoopStr holds the addF of K is commutative;

theorem :: FVSUM_1:2
  for K being add-associative non empty addLoopStr holds the addF
  of K is associative;

theorem :: FVSUM_1:3
  for K being commutative non empty multMagma holds the multF of
  K is commutative;

registration
  let K be Abelian non empty addLoopStr;
  cluster the addF of K -> commutative;
end;

registration
  let K be add-associative non empty addLoopStr;
  cluster the addF of K -> associative;
end;

registration
  let K be commutative non empty multMagma;
  cluster the multF of K -> commutative;
end;

theorem :: FVSUM_1:4
  for K being commutative left_unital non empty multLoopStr holds
  1.K is_a_unity_wrt the multF of K;

theorem :: FVSUM_1:5
  for K being commutative left_unital non empty multLoopStr holds
  the_unity_wrt the multF of K = 1.K;

theorem :: FVSUM_1:6
  for K being left_zeroed right_zeroed non empty addLoopStr holds
  0.K is_a_unity_wrt the addF of K;

theorem :: FVSUM_1:7
  for K being left_zeroed right_zeroed non empty addLoopStr holds
  the_unity_wrt the addF of K = 0.K;

theorem :: FVSUM_1:8
  for K being left_zeroed right_zeroed non empty addLoopStr
  holds the addF of K is having_a_unity;

theorem :: FVSUM_1:9
  for K being commutative left_unital non empty multLoopStr
  holds the multF of K is having_a_unity;

theorem :: FVSUM_1:10
  for K being distributive non empty doubleLoopStr holds the
  multF of K is_distributive_wrt the addF of K;

definition
  let K be non empty multMagma;
  let a be Element of K;
  func a multfield -> UnOp of the carrier of K equals
:: FVSUM_1:def 1
  (the multF of K)[;](a,id
  (the carrier of K));
end;

definition
  let K be non empty addLoopStr;
  func diffield(K) -> BinOp of the carrier of K equals
:: FVSUM_1:def 2
  (the addF of K)*(id the
  carrier of K,comp K);
end;

theorem :: FVSUM_1:11
  for K being non empty addLoopStr, a1,a2 being Element of K holds
  (diffield(K)).(a1,a2) = a1 - a2;

theorem :: FVSUM_1:12
  for K being distributive non empty doubleLoopStr, a being
  Element of K holds a multfield is_distributive_wrt the addF of K;

theorem :: FVSUM_1:13
  for K being left_zeroed right_zeroed add-associative
  right_complementable non empty addLoopStr holds comp K is_an_inverseOp_wrt
  the addF of K;

theorem :: FVSUM_1:14
  for K being left_zeroed right_zeroed add-associative
  right_complementable non empty addLoopStr holds the addF of K is
  having_an_inverseOp;

theorem :: FVSUM_1:15
  for K being left_zeroed right_zeroed add-associative
right_complementable non empty addLoopStr holds the_inverseOp_wrt the addF of
  K = comp K;

theorem :: FVSUM_1:16
  for K being right_zeroed add-associative right_complementable Abelian
  non empty addLoopStr holds comp K is_distributive_wrt the addF of K;

begin

::
:: Some Operations on the i-tuples on Element of K
::

definition
  let K be non empty addLoopStr;
  let p1,p2 be FinSequence of the carrier of K;
  func p1 + p2 -> FinSequence of the carrier of K equals
:: FVSUM_1:def 3
  (the addF of K).:(p1,
  p2);
end;

theorem :: FVSUM_1:17
  for K being non empty addLoopStr, p1, p2 be FinSequence of the carrier
  of K, a1, a2 being Element of K, i being Nat st i in dom (p1+p2) &
  a1 = p1.i & a2 = p2.i holds (p1+p2).i = a1 + a2;

definition
  let i;
  let K be non empty addLoopStr;
  let R1,R2 be Element of i-tuples_on the carrier of K;
  redefine func R1 + R2 -> Element of i-tuples_on the carrier of K;
end;

theorem :: FVSUM_1:18
  for K being non empty addLoopStr, a1,a2 being Element of K, R1,R2
being Element of i-tuples_on the carrier of K holds j in Seg i & a1 = R1.j & a2
  = R2.j implies (R1+R2).j = a1 + a2;

theorem :: FVSUM_1:19
  for K being non empty addLoopStr, a1,a2 being Element of K holds <*a1
  *> + <*a2*> = <*a1+a2*>;

theorem :: FVSUM_1:20
  for K being non empty addLoopStr, a1,a2 being Element of K holds (i|->
  a1) + (i|->a2) = i|->(a1+a2);

theorem :: FVSUM_1:21
  for K being Abelian left_zeroed right_zeroed non empty
addLoopStr, R being Element of i-tuples_on the carrier of K holds R + (i|->(0.
  K)) = R & R = (i|->(0.K)) + R;

definition
  let K be non empty addLoopStr;
  let p be FinSequence of the carrier of K;
  func -p -> FinSequence of the carrier of K equals
:: FVSUM_1:def 4
  (comp K)*p;
end;

reserve K for non empty addLoopStr,
  a for Element of K,
  p for FinSequence of the carrier of K,
  R for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:22
  i in dom -p & a = p.i implies (-p).i = -a;

definition
  let i;
  let K be non empty addLoopStr;
  let R be Element of i-tuples_on the carrier of K;
  redefine func -R -> Element of i-tuples_on the carrier of K;
end;

theorem :: FVSUM_1:23
  j in Seg i & a = R.j implies (-R).j = -a;

theorem :: FVSUM_1:24
  -<*a*> = <*-a*>;

theorem :: FVSUM_1:25
  -(i|->a) = i|->-a;

theorem :: FVSUM_1:26
  for K being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr, R being Element of i-tuples_on the
  carrier of K holds R + -R = (i|->0.K) & -R + R = (i|->0.K);

reserve K for left_zeroed right_zeroed add-associative right_complementable
  non empty addLoopStr,
  R,R1,R2 for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:27
  R1 + R2 = (i|->0.K) implies R1 = -R2 & R2 = -R1;

theorem :: FVSUM_1:28
  --R = R;

theorem :: FVSUM_1:29
  -R1 = -R2 implies R1 = R2;

theorem :: FVSUM_1:30
  for K being Abelian right_zeroed add-associative right_complementable
  non empty addLoopStr, R,R1,R2 being Element of i-tuples_on the carrier of K
  holds R1 + R = R2 + R or R1 + R = R + R2 implies R1 = R2;

theorem :: FVSUM_1:31
  for K being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr, R1,R2 being Element of i-tuples_on
  the carrier of K holds -(R1 + R2) = -R1 + -R2;

definition
  let K be non empty addLoopStr;
  let p1,p2 be FinSequence of the carrier of K;
  func p1 - p2 -> FinSequence of the carrier of K equals
:: FVSUM_1:def 5
  (diffield(K)).:(p1,p2
  );
end;

reserve K for non empty addLoopStr,
  a1,a2 for Element of K,
  p1,p2 for FinSequence of the carrier of K,
  R1,R2 for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:32
  i in dom (p1-p2) & a1 = p1.i & a2 = p2.i implies (p1-p2).i = a1 - a2;

definition
  let i;
  let K be non empty addLoopStr;
  let R1,R2 be Element of i-tuples_on the carrier of K;
  redefine func R1 - R2 -> Element of i-tuples_on the carrier of K;
end;

theorem :: FVSUM_1:33
  j in Seg i & a1 = R1.j & a2 = R2.j implies (R1-R2).j = a1 - a2;

theorem :: FVSUM_1:34
  <*a1*> - <*a2*> = <*a1-a2*>;

theorem :: FVSUM_1:35
  (i|->a1) - (i|->a2) = i|->(a1-a2);

theorem :: FVSUM_1:36
  for K being add-associative right_complementable left_zeroed
right_zeroed non empty addLoopStr, R being Element of i-tuples_on the carrier
  of K holds R - (i|->(0.K)) = R;

theorem :: FVSUM_1:37
  for K being Abelian left_zeroed right_zeroed non empty addLoopStr, R
  being Element of i-tuples_on the carrier of K holds (i|->(0.K)) - R = -R;

theorem :: FVSUM_1:38
  for K being left_zeroed right_zeroed add-associative
right_complementable non empty addLoopStr, R1,R2 being Element of i-tuples_on
  the carrier of K holds R1 - -R2 = R1 + R2;

reserve K for Abelian right_zeroed add-associative right_complementable non
  empty addLoopStr,
  R,R1,R2,R3 for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:39
  -(R1 - R2) = R2 - R1;

theorem :: FVSUM_1:40
  -(R1 - R2) = -R1 + R2;

theorem :: FVSUM_1:41
  R - R = (i|->0.K);

theorem :: FVSUM_1:42
  R1 - R2 = (i|->0.K) implies R1 = R2;

theorem :: FVSUM_1:43
  R1 - R2 - R3 = R1 - (R2 + R3);

theorem :: FVSUM_1:44
  R1 + (R2 - R3) = R1 + R2 - R3;

theorem :: FVSUM_1:45
  R1 - (R2 - R3) = R1 - R2 + R3;

theorem :: FVSUM_1:46
  R1 = R1 + R - R;

theorem :: FVSUM_1:47
  R1 = R1 - R + R;

reserve K for non empty multMagma,
  a,a9,a1,a2 for Element of K,
  p for FinSequence of the carrier of K,
  R for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:48
  for a,b being Element of K holds ((the multF of K)[;](a,id the
  carrier of K)).b = a*b;

theorem :: FVSUM_1:49
  for a,b being Element of K holds (a multfield).b = a*b;

definition
  let K be non empty multMagma;
  let p be FinSequence of the carrier of K;
  let a be Element of K;
  func a*p -> FinSequence of the carrier of K equals
:: FVSUM_1:def 6
  (a multfield)*p;
end;

theorem :: FVSUM_1:50
  i in dom (a*p) & a9 = p.i implies (a*p).i = a*a9;

definition
  let i;
  let K be non empty multMagma;
  let R be Element of i-tuples_on the carrier of K;
  let a be Element of K;
  redefine func a*R -> Element of i-tuples_on the carrier of K;
end;

theorem :: FVSUM_1:51
  j in Seg i & a9 = R.j implies (a*R).j = a*a9;

theorem :: FVSUM_1:52
  a*<*a1*> = <*a*a1*>;

theorem :: FVSUM_1:53
  a1*(i|->a2) = i|->(a1*a2);

theorem :: FVSUM_1:54
  for K being associative non empty multMagma, a1,a2 being Element of
K, R being Element of i-tuples_on the carrier of K holds (a1*a2)*R = a1*(a2*R);

reserve K for distributive non empty doubleLoopStr,
  a,a1,a2 for Element of K ,
  R,R1,R2 for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:55
  (a1 + a2)*R = a1*R + a2*R;

theorem :: FVSUM_1:56
  a*(R1+R2) = a*R1 + a*R2;

theorem :: FVSUM_1:57
  for K being distributive commutative left_unital non empty
doubleLoopStr, R being Element of i-tuples_on the carrier of K holds 1.K * R =
  R;

theorem :: FVSUM_1:58
  for K being add-associative right_zeroed right_complementable
  distributive non empty doubleLoopStr, R being Element of i-tuples_on the
  carrier of K holds 0.K*R = i|->0.K;

theorem :: FVSUM_1:59
  for K being add-associative right_zeroed right_complementable
commutative left_unital distributive non empty doubleLoopStr, R being Element
  of i-tuples_on the carrier of K holds (-1.K) * R = -R;

definition
  let M be non empty multMagma, p1, p2 be FinSequence of the carrier of M;
  func mlt(p1,p2) -> FinSequence of the carrier of M equals
:: FVSUM_1:def 7
  (the multF of M).:
  (p1,p2);
end;

reserve K for non empty multMagma,
  a1,a2,b1,b2 for Element of K,
  p1,p2 for FinSequence of the carrier of K,
  R1,R2 for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:60
  i in dom mlt(p1,p2) & a1 = p1.i & a2 = p2.i implies mlt(p1,p2).i = a1
  * a2;

definition
  let i;
  let K be non empty multMagma;
  let R1,R2 be Element of i-tuples_on the carrier of K;
  redefine func mlt(R1,R2) -> Element of i-tuples_on the carrier of K;
end;

theorem :: FVSUM_1:61
  j in Seg i & a1 = R1.j & a2 = R2.j implies mlt(R1,R2).j = a1 * a2;

theorem :: FVSUM_1:62
  mlt(<*a1*>,<*a2*>) = <*a1*a2*>;

reserve K for commutative non empty multMagma,
  p,q for FinSequence of the carrier of K,
  R1,R2 for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:63
  mlt(R1,R2) = mlt(R2,R1);

theorem :: FVSUM_1:64
  mlt(p,q)=mlt(q,p);

theorem :: FVSUM_1:65
  for K being associative non empty multMagma, R1,R2,R3 being Element
  of i-tuples_on the carrier of K holds mlt(R1,mlt(R2,R3)) = mlt(mlt(R1,R2),R3)
;

reserve K for commutative associative non empty multMagma,
  a,a1,a2 for Element of K,
  R for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:66
  mlt(i|->a,R) = a*R & mlt(R,i|->a) = a*R;

theorem :: FVSUM_1:67
  mlt(i|->a1,i|->a2) = i|->(a1*a2);

theorem :: FVSUM_1:68
  for K being associative non empty multMagma, a being Element of K,
R1,R2 being Element of i-tuples_on the carrier of K holds a*mlt(R1,R2) = mlt(a*
  R1,R2);

reserve K for commutative associative non empty multMagma,
  a for Element of K,
  R,R1,R2 for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:69
  a*mlt(R1,R2) = mlt(a*R1,R2) & a*mlt(R1,R2) = mlt(R1,a*R2);

theorem :: FVSUM_1:70
  a*R = mlt(i|->a,R);

begin

::
::The Sum of Finite Number of Elements
::

registration
  cluster Abelian right_zeroed -> left_zeroed for non empty addLoopStr;
end;

definition
  let K be Abelian add-associative right_zeroed right_complementable non
  empty addLoopStr;
  let p be FinSequence of the carrier of K;
  redefine func Sum(p) equals
:: FVSUM_1:def 8
  (the addF of K) $$ p;
end;

reserve K for add-associative right_zeroed right_complementable non empty
  addLoopStr,
  a for Element of K,
  p for FinSequence of the carrier of K;

theorem :: FVSUM_1:71
  Sum(p^<*a*>) = Sum p + a;

theorem :: FVSUM_1:72
  Sum(<*a*>^p) = a + Sum p;

theorem :: FVSUM_1:73
  for K being Abelian add-associative right_zeroed right_complementable
  distributive non empty doubleLoopStr, a being Element of K, p being
  FinSequence of the carrier of K holds Sum(a*p) = a*(Sum p);

theorem :: FVSUM_1:74
  for K being non empty addLoopStr for R being Element of 0-tuples_on
  the carrier of K holds Sum R = 0.K;

reserve K for Abelian add-associative right_zeroed right_complementable non
  empty addLoopStr,
  p for FinSequence of the carrier of K,
  R1,R2 for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:75
  Sum -p = -(Sum p);

theorem :: FVSUM_1:76
  Sum(R1 + R2) = Sum R1 + Sum R2;

theorem :: FVSUM_1:77
  Sum(R1 - R2) = Sum R1 - Sum R2;

begin

reserve K for commutative associative well-unital non empty doubleLoopStr,
  a ,a1,a2,a3 for Element of K,
  p1 for FinSequence of the carrier of K,
  R1,R2 for Element of i-tuples_on the carrier of K;

theorem :: FVSUM_1:78
  Product(<*a*>^p1) = a * Product p1;

theorem :: FVSUM_1:79
  Product<*a1,a2,a3*> = a1 * a2 * a3;

theorem :: FVSUM_1:80
  for R being Element of 0-tuples_on the carrier of K holds Product R = 1.K;

theorem :: FVSUM_1:81
  Product(i|->(1_K)) = 1_K;

theorem :: FVSUM_1:82
  for K being add-associative right_zeroed right_complementable Abelian
  commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr for p being FinSequence of the carrier of
  K holds (ex k st k in dom p & p.k = 0.K) iff Product p = 0.K;

theorem :: FVSUM_1:83
  Product((i+j) |-> a) = (Product(i|->a))*(Product(j|->a));

theorem :: FVSUM_1:84
  Product((i*j) |-> a) = Product(j|->(Product(i|->a)));

theorem :: FVSUM_1:85
  Product(i|->(a1*a2)) = (Product(i|->a1))*(Product(i|->a2));

theorem :: FVSUM_1:86
  Product mlt(R1,R2) = Product R1 * Product R2;

theorem :: FVSUM_1:87
  Product(a*R1) = Product (i|->a) * Product R1;

begin :: The Product of Vectors

definition
  let K be non empty doubleLoopStr;
  let p,q be FinSequence of the carrier of K;
  func p "*" q -> Element of K equals
:: FVSUM_1:def 9
  Sum(mlt(p,q));
end;

theorem :: FVSUM_1:88
  for K being commutative associative left_unital Abelian
add-associative right_zeroed right_complementable non empty doubleLoopStr for
  a,b being Element of K holds <*a*> "*" <*b*>= a * b;

theorem :: FVSUM_1:89
  for K being commutative associative left_unital Abelian
add-associative right_zeroed right_complementable non empty doubleLoopStr for
  a1,a2,b1,b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*>= a1*b1 + a2*b2;

theorem :: FVSUM_1:90
  for p,q be FinSequence of the carrier of K holds p "*" q = q "*" p;