The Mizar abstract of PRVECT

Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users
The abstract of the Mizar article:: Product of Families of Groups and Vector Spaces
by
Anna Lango, and
Grzegorz Bancerek
Received December 29, 1992
MML identifier: PRVECT_1
[ Mizar article, MML identifier index ]
environ

 vocabulary RLVECT_1, VECTSP_1, BINOP_1, FUNCT_1, FINSEQOP, ARYTM_1, FINSEQ_2,
      RELAT_1, CARD_3, CAT_1, SETWISEO, FUNCOP_1, PARTFUN1, FINSEQ_1, BOOLE,
      ZF_REFLE, FRAENKEL, FUNCT_3, FUNCT_6, GROUP_2, PRVECT_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, CARD_3, RELAT_1,
      FUNCT_1, STRUCT_0, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCOP_1,
      RLVECT_1, VECTSP_1, FINSEQOP, FINSEQ_1, FRAENKEL, FUNCT_6, SETWISEO,
      FINSEQ_2;
 constructors FUNCT_5, CARD_3, FUNCT_3, BINOP_1, VECTSP_1, FINSEQOP, FRAENKEL,
      FUNCT_6, SETWISEO, MEMBERED, PARTFUN1, XBOOLE_0;
 clusters FUNCT_1, VECTSP_1, FRAENKEL, STRUCT_0, FINSEQ_2, GROUP_1, RELSET_1,
      AMI_1, FUNCOP_1, FINSEQ_1, ARYTM_3, MEMBERED, ZFMISC_1, FUNCT_2,
      PARTFUN1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Abelian Groups and Fields

reserve G for Abelian add-associative right_complementable right_zeroed
    (non empty LoopStr);

canceled 2;

theorem :: PRVECT_1:3
 the Zero of G is_a_unity_wrt the add of G;

theorem :: PRVECT_1:4
 for G being AbGroup holds comp G is_an_inverseOp_wrt the add of G;

reserve GS for non empty LoopStr;

theorem :: PRVECT_1:5
    the add of GS is commutative associative &
  the Zero of GS is_a_unity_wrt the add of GS &
  comp GS is_an_inverseOp_wrt the add of GS implies
   GS is AbGroup;

reserve F for Field;

canceled 4;

theorem :: PRVECT_1:10
    the Zero of F is_a_unity_wrt the add of F;

theorem :: PRVECT_1:11
 the unity of F is_a_unity_wrt the mult of F;

begin :: The $n$-Product of a Binary and Unary Operation

 reserve F for Field,
         n for Nat,
         D for non empty set,
         d for Element of D,
         B for BinOp of D,
         C for UnOp of D;

definition let D,n;
  let F be BinOp of D;
  let x,y be Element of n-tuples_on D;
  redefine func F.:(x,y) -> Element of n-tuples_on D;
 end;

definition let D be non empty set;
           let F be BinOp of D;
           let n be Nat;
  func product(F,n) -> BinOp of n-tuples_on D means
:: PRVECT_1:def 1
   for x,y being Element of n-tuples_on D holds
              it.(x,y)=F.:(x,y);
  end;

definition let D;
           let F be UnOp of D;
           let n;
  func product(F,n) -> UnOp of n-tuples_on D means
:: PRVECT_1:def 2
     for x being Element of n-tuples_on D holds it.x=F*x;
 end;

definition let D be non empty set;
 let n; let x be Element of D;
 redefine func n |-> x -> Element of n-tuples_on D;
 synonym n .--> x;
end;

canceled 2;

theorem :: PRVECT_1:14
  B is commutative implies product(B,n) is commutative;

theorem :: PRVECT_1:15
  B is associative implies product(B,n) is associative;

theorem :: PRVECT_1:16
  d is_a_unity_wrt B implies n .--> d is_a_unity_wrt product(B,n);

theorem :: PRVECT_1:17
  B has_a_unity & B is associative & C is_an_inverseOp_wrt B implies
   product(C,n) is_an_inverseOp_wrt product(B,n);

begin :: The $n$-Power of a Group and of a Field

definition let F be non empty LoopStr, n;
  assume F is Abelian add-associative right_zeroed right_complementable;
  func n -Group_over F -> strict AbGroup equals
:: PRVECT_1:def 3
     LoopStr(# n-tuples_on the carrier of F,
        product(the add of F,n),
        (n .--> the Zero of F) qua Element of n-tuples_on the carrier of F#);
end;

definition let F be AbGroup, n;
 cluster n-Group_over F -> non empty;
end;

reserve x,y for set;

definition let F,n;
  func n -Mult_over F -> Function of
    [:the carrier of F,n-tuples_on the carrier of F:],
    n-tuples_on the carrier of F means
:: PRVECT_1:def 4
   for x being Element of F,
       v being Element of n-tuples_on the carrier of F holds
    it.(x,v) = (the mult of F)[;](x,v);
 end;

definition let F,n;
  func n -VectSp_over F -> strict VectSpStr over F means
:: PRVECT_1:def 5
   the LoopStr of it = n -Group_over F &
   the lmult of it = n -Mult_over F;
 end;

definition let F,n;
 cluster n -VectSp_over F -> non empty;
end;

 reserve D for non empty set,
         H,G for BinOp of D,
         d for Element of D,
         t1,t2 for Element of n-tuples_on D;

theorem :: PRVECT_1:18
  H is_distributive_wrt G implies H[;](d,G.:(t1,t2)) = G.:
(H[;](d,t1),H[;](d,t2));

definition let D be non empty set,
             n be Nat,
             F be BinOp of D,
             x be Element of D,
             v be Element of n-tuples_on D;
  redefine func F[;](x,v) -> Element of n-tuples_on D;
 end;

definition let F,n;
  cluster n -VectSp_over F -> VectSp-like;
 end;

begin :: Sequences of domains

reserve x,y,y1,y2,z for set,
         i for Nat,
         A for AbGroup,
         D for non empty set;

definition
  cluster non empty non-empty FinSequence;
 end;

definition
  let f be non-empty Function;
  cluster product f -> functional non empty;
 end;

definition
  mode Domain-Sequence is non empty non-empty FinSequence;
 end;

definition
  let a be non empty Function;
  cluster dom a -> non empty;
 end;

scheme NEFinSeqLambda {w()-> non empty FinSequence, F(set)->set}:
 ex p being non empty FinSequence st len p = len w() &
  for i being Element of dom w() holds p.i = F(i);

definition
  let a be non-empty non empty Function;
  let i be Element of dom a;
  cluster a.i -> non empty;
end;

definition let a be non-empty non empty Function;
 let f be Element of product a;
 let i be Element of dom a;
 redefine func f.i -> Element of a.i;
end;

begin :: The Product of Families of Operations

reserve a for Domain-Sequence,
        i for Element of dom a,
        p for FinSequence;

definition let a be non-empty non empty Function;
 canceled 2;

  mode BinOps of a -> Function means
:: PRVECT_1:def 8
   dom it = dom a & for i being Element of dom a holds it.i is BinOp of a.i;
  mode UnOps of a -> Function means
:: PRVECT_1:def 9

   dom it = dom a & for i being Element of dom a holds it.i is UnOp of a.i;
end;

definition let a;
 cluster -> FinSequence-like BinOps of a;
 cluster -> FinSequence-like UnOps of a;
end;

theorem :: PRVECT_1:19
 p is BinOps of a iff len p = len a &
  for i holds p.i is BinOp of a.i;

theorem :: PRVECT_1:20
 p is UnOps of a iff len p = len a &
  for i holds p.i is UnOp of a.i;

definition let a;
  let b be BinOps of a;
  let i;
  redefine func b.i -> BinOp of a.i;
 end;

definition let a;
 let u be UnOps of a;
 let i;
 redefine func u.i -> UnOp of a.i;
end;

definition let F be functional non empty set;
 let u be UnOp of F, f be Element of F;
 redefine func u.f -> Element of F;
end;

theorem :: PRVECT_1:21
   for d,d' being UnOp of product a st
  for f being Element of product a, i being Element of dom a
    holds (d.f).i = (d'.f).i holds d = d';

theorem :: PRVECT_1:22
 for u being UnOps of a holds
  doms u = a & product rngs u c= product a;

definition let a;
 let u be UnOps of a;
 redefine func Frege u -> UnOp of product a;
end;

theorem :: PRVECT_1:23
 for u being UnOps of a for f being Element of product a,
     i being Element of dom a holds (Frege u).f.i = (u.i).(f.i);

definition let F be functional non empty set;
 let b be BinOp of F, f,g be Element of F;
 redefine func b.(f,g) -> Element of F;
end;

theorem :: PRVECT_1:24
 for d,d' being BinOp of product a st
  for f,g being Element of product a, i being Element of dom a
      holds (d.(f,g)).i = (d'.(f,g)).i holds d = d';

reserve i for Element of dom a;

definition let a;
 let b be BinOps of a;
 func [:b:] -> BinOp of product a means
:: PRVECT_1:def 10
  for f,g being Element of product a,
      i being Element of dom a holds (it.(f,g)).i = (b.i).(f.i,g.i);
end;

theorem :: PRVECT_1:25
 for b being BinOps of a st for i holds b.i is commutative
  holds [:b:] is commutative;

theorem :: PRVECT_1:26
 for b being BinOps of a st for i holds b.i is associative
  holds [:b:] is associative;

theorem :: PRVECT_1:27
 for b being BinOps of a, f being Element of product a st
  for i holds f.i is_a_unity_wrt b.i holds f is_a_unity_wrt [:b:];

theorem :: PRVECT_1:28
 for b being BinOps of a, u being UnOps of a st
  for i holds u.i is_an_inverseOp_wrt b.i & b.i has_a_unity holds
   Frege u is_an_inverseOp_wrt [:b:];

begin :: The Product of Groups

definition let F be Function;
  attr F is AbGroup-yielding means
:: PRVECT_1:def 11
    x in rng F implies x is AbGroup;
end;

definition
  cluster non empty AbGroup-yielding FinSequence;
end;

definition
 mode Group-Sequence is non empty AbGroup-yielding FinSequence;
end;

definition
  let g be Group-Sequence;
  let i be Element of dom g;
  redefine func g.i -> AbGroup;
 end;

definition let g be Group-Sequence;
 func carr g -> Domain-Sequence means
:: PRVECT_1:def 12
  len it = len g & for j be Element of dom g holds it.j = the carrier of g.j;
end;

reserve g for Group-Sequence, i for Element of dom carr g;

definition let g,i;
 redefine func g.i -> AbGroup;
end;

definition let g;
 func addop g -> BinOps of carr g means
:: PRVECT_1:def 13
  len it = len carr g & for i holds it.i = the add of g.i;
 func complop g -> UnOps of carr g means
:: PRVECT_1:def 14
  len it = len carr g & for i holds it.i = comp g.i;
 func zeros g -> Element of product carr g means
:: PRVECT_1:def 15
  for i holds it.i = the Zero of g.i;
end;

definition
 let G be Group-Sequence;
 func product G -> strict AbGroup equals
:: PRVECT_1:def 16
     LoopStr(# product carr G, [:addop G:], zeros G #);
end;
The abstract of the Mizar article:

Product of Families of Groups and Vector Spaces
