:: Isomorphisms of Direct Products of Cyclic Groups of Prime-power Order
::  by Hiroshi Yamazaki , Hiroyuki Okazaki , Kazuhisa Nakasho and Yasunari Shidama
::
:: Received October 7, 2013
:: Copyright (c) 2013-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 GROUP_18, FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI,
      BINOP_1, GROUP_1, XXREAL_0, GROUP_2, GROUP_3, LOPBAN_1, CARD_1, NUMBERS,
      FUNCT_4, GROUP_6, GROUP_7, POWER, FUNCOP_1, ALGSTR_0, PARTFUN1, FUNCT_2,
      SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1,
      ARYTM_3, FINSET_1, INT_2, PBOOLE, NEWTON, INT_1, GROUP_4, CQC_SIM1,
      REAL_1, XCMPLX_0, SEQ_4;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
      PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE,
      CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, INT_2,
      FINSEQ_1, SEQ_4, POWER, NEWTON, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2,
      GROUP_3, GROUP_4, GROUP_5, GROUP_6, PRALG_1, GROUP_7, GROUP_17;
 constructors REALSET1, FUNCT_4, GROUP_6, MONOID_0, PRALG_1, GROUP_4, GROUP_5,
      GROUP_7, RELSET_1, WELLORD2, NAT_D, NAT_3, SEQ_4, GROUP_17, POWER;
 registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1,
      FUNCT_2, FUNCOP_1, GROUP_7, GROUP_3, XXREAL_0, RELSET_1, FINSEQ_1, INT_1,
      GR_CY_1, FINSET_1, NAT_3, FUNCT_1, XCMPLX_0, MEMBERED, NEWTON, VALUED_0,
      XXREAL_2, FINSEQ_2, PBOOLE, GROUP_6, POWER;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Basic Properties of Cyclic Groups of prime-power order

definition let G be finite Group;
  func Ordset G -> Subset of NAT equals
:: GROUP_18:def 1
    the set of all ord a where a is Element of G;
end;

registration let G be finite Group;
  cluster Ordset G -> finite non empty;
end;

theorem :: GROUP_18:1
  for G be finite Group holds
    ex g be Element of G st ord g = upper_bound Ordset G;

theorem :: GROUP_18:2
  for G being strict Group, N be strict normal Subgroup of G
  st G is commutative
  holds G./.N is commutative;

theorem :: GROUP_18:3  ::: improve GR_CY_2:6
  for G being finite Group, a, b be Element of G
  holds b in gr {a} iff ex p be Element of NAT st b = a |^p;

theorem :: GROUP_18:4
  for G being finite Group, a be Element of G,
  n, p, s being Element of NAT
  st card gr{a} = n & n = p * s
  holds ord(a |^ p) = s;

theorem :: GROUP_18:5
  for k being Element of NAT, G being finite Group, a being Element of G
  holds gr{a} = gr{(a |^ k)} iff k gcd (ord a) = 1;

theorem :: GROUP_18:6
  for k being Element of NAT, G being finite Group,
      a being Element of G st k gcd (ord a) = 1
  holds ord a = ord(a |^ k);

theorem :: GROUP_18:7
  for k being Element of NAT, G being finite Group, a being Element of G
  holds (ord a) divides k * ord(a |^ k);

theorem :: GROUP_18:8
  for G being Group, a, b being Element of G st b in gr{a}
  holds gr{b} is strict Subgroup of gr{a};

definition
  let G be strict commutative Group, x be Element of Subgroups G;
  func modetrans(x) -> normal strict Subgroup of G equals
:: GROUP_18:def 2
  x;
end;

theorem :: GROUP_18:9
  for G, H be Group, K be Subgroup of H, f be Homomorphism of G, H holds
  ex J be strict Subgroup of G
  st the carrier of J = f"(the carrier of K);

theorem :: GROUP_18:10
  for p being Nat, G being finite Group, x, d be Element of G
  st ord d = p & p is prime & x in gr{d}
  holds x = 1_G or gr{x} = gr{d};

theorem :: GROUP_18:11
  for G being Group, H, K be normal Subgroup of G
  st (the carrier of H) /\ (the carrier of K) = {1_G}
  holds (nat_hom H) | (the carrier of K) is one-to-one;

theorem :: GROUP_18:12
  for G, F being finite commutative Group, a be Element of G,
  f be Homomorphism of G, F
  holds the carrier of gr{f.a} = f.: (the carrier of gr{a});

theorem :: GROUP_18:13
  for G, F being finite commutative Group, a be Element of G,
  f be Homomorphism of G, F
  holds ord(f.a) <= ord a;

theorem :: GROUP_18:14
  for G, F being finite commutative Group, a be Element of G,
  f be Homomorphism of G, F st f is one-to-one
  holds ord(f.a) = ord a;

theorem :: GROUP_18:15
  for G, F being Group, H be Subgroup of G, f be Homomorphism of G, F
  holds f| (the carrier of H) is Homomorphism of H, F;

theorem :: GROUP_18:16
  for G, F being finite commutative Group, a be Element of G,
  f be Homomorphism of G, F
  st f| (the carrier of gr{a}) is one-to-one
  holds ord(f.a) = ord a;

theorem :: GROUP_18:17
  for G being finite commutative Group, p being Prime, m be Nat,
  a be Element of G st card(G) = p|^m & a <> 1_G
  holds ex n be Nat st ord a = p|^(n+1);

theorem :: GROUP_18:18
  for p being Prime, j, m, k be Nat st m = p|^k & not p divides j
  holds j gcd m = 1;

begin :: Isomorphism of cyclic groups of prime-power order

theorem :: GROUP_18:19
  for G being strict finite commutative Group, p being Prime, m be Nat
  st card(G) = p|^m
  ex K be normal strict Subgroup of G, n, k be Nat, g be Element of G st
  ord g = upper_bound Ordset G & K is finite commutative
  & (the carrier of K) /\ (the carrier of gr{g}) = {1_G}
  & (for x be Element of G
  holds ex b1, a1 be Element of G st b1 in K & a1 in gr{g} & x = b1*a1)
  & ord g = p|^n
  & k = m - n & n <= m
  & card K = p|^k
  & ex F being Homomorphism of product <*K,gr{g}*>, G st F is bijective
  & for a,b be Element of G st a in K & b in gr{g}
  holds F.(<*a,b*>) = a*b;

theorem :: GROUP_18:20
  for G being strict finite commutative Group, p being Prime, m be Nat
  st card(G) = p|^m holds
  ex k be non zero Nat, a be k-element FinSequence of G,
  Inda be k-element FinSequence of NAT,
  F be associative Group-like commutative multMagma-Family of Seg k,
  HFG be Homomorphism of product F, G
  st (for i be Nat st i in Seg k
  holds ex ai be Element of G
  st ai = a.i & F.i = gr{ai} & ord(ai) = p|^(Inda.i))
  & (for i be Nat st 1 <= i & i <= k -1 holds Inda.i <= Inda.(i+1))
  & (for p,q be Element of Seg k st p <> q
  holds (the carrier of (F.p)) /\ (the carrier of (F.q)) ={1_G})
  & HFG is bijective
  & for x be (the carrier of G)-valued total (Seg k)-defined Function
  st for p be Element of Seg k holds x.p in F.p
  holds x in product F & HFG.x = Product x;

theorem :: GROUP_18:21
  for G being strict finite commutative Group, p being Prime, m be Nat
  st card(G) = p|^m holds
  ex k be non zero Nat, a be k-element FinSequence of G,
  Inda be k-element FinSequence of NAT,
  F be associative Group-like commutative multMagma-Family of Seg k
  st (for i be Nat st i in Seg k holds ex ai be Element of G
  st ai = a.i & F.i = gr{ai} & ord(ai) = p|^(Inda.i))
  & (for i be Nat st 1 <= i & i <= k -1 holds Inda.i <= Inda.(i+1))
  & (for p,q be Element of Seg k st p <> q
  holds (the carrier of (F.p)) /\ (the carrier of (F.q)) ={1_G})
  & (for y be Element of G holds
  ex x be (the carrier of G)-valued total (Seg k) -defined Function
  st (for p be Element of Seg k holds x.p in F.p) & y = Product x)
  & for x1, x2 be (the carrier of G)-valued total (Seg k) -defined Function
  st (for p be Element of Seg k holds x1.p in F.p)
   & (for p be Element of Seg k holds x2.p in F.p)
   & Product x1 = Product x2 holds x1 = x2;