:: 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-2026 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, INT_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities GROUP_2, GROUP_6, FINSEQ_1, STRUCT_0, FUNCOP_1, ORDINAL1;
expansions STRUCT_0;
theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, FUNCOP_1, TARSKI, GROUP_1,
GROUP_2, GROUP_3, FUNCT_4, FINSEQ_1, GROUP_4, GROUP_5, GROUP_6, XREAL_1,
ORDINAL1, NAT_1, INT_1, XCMPLX_1, GR_CY_2, XBOOLE_0, RELAT_1, XXREAL_0,
GROUP_7, STRUCT_0, XBOOLE_1, NEWTON, NUMBERS, GROUPP_1, PARTFUN1, INT_2,
NAT_D, ZFMISC_1, GR_CY_1, CARD_1, WELLORD2, GROUP_17, POWER, SEQ_4;
schemes NAT_1, FRAENKEL;
begin :: Basic Properties of Cyclic Groups of prime-power order
definition let G be finite Group;
func Ordset G -> Subset of NAT equals
the set of all ord a where a is Element of G;
coherence
proof
set IT = the set of all ord a where a is Element of G;
IT c= NAT
proof
let a be object;
assume a in IT; then
consider n being Element of G such that
A1: a = ord n;
thus thesis by A1;
end;
hence thesis;
end;
end;
registration let G be finite Group;
cluster Ordset G -> finite non empty;
coherence
proof
deffunc F(Element of G) = ord $1;
GG: (the carrier of G) is finite;
set A = {F(g) where g is Element of G: g in the carrier of G};
T1: A = Ordset G
proof
Y1: A c= Ordset G
proof
let x be object;
assume x in A; then
consider g being Element of G such that
Y2: x = F(g) & g in the carrier of G;
thus thesis by Y2;
end;
Ordset G c= A
proof
let x be object;
assume x in Ordset G; then
consider g being Element of G such that
Y2: x = F(g);
thus thesis by Y2;
end;
hence thesis by Y1,XBOOLE_0:def 10;
end;
P1: A is finite from FRAENKEL:sch 21(GG);
ord(1_G) in A;
hence thesis by P1,T1;
end;
end;
theorem LM202:
for G be finite Group holds
ex g be Element of G st ord g = upper_bound Ordset G
proof
let G be finite Group;
set A = Ordset G;
set l = upper_bound A;
A <> {} & A c= REAL by NUMBERS:19, XBOOLE_1:1;
then l in A by SEQ_4:133;
then consider g being Element of G such that
A3: ord g = l;
take g;
thus thesis by A3;
end;
theorem GROUP630:
for G being strict Group, N be strict normal Subgroup of G
st G is commutative
holds G./.N is commutative
proof
let G be strict Group, N be strict normal Subgroup of G;
assume G is commutative;
then G` = (1).G by GROUP_5:75;
then G` = (1).N by GROUP_2:63;
hence thesis by GROUP_6:30;
end;
theorem GRCY26: ::: 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
proof
let G be finite Group, a, b be Element of G;
reconsider a0 = a as Element of gr{a} by GR_CY_2:2, STRUCT_0:def 5;
X1: gr{a0} = gr{a} by GR_CY_2:3;
hereby
assume b in gr{a};
then reconsider b0 = b as Element of gr{a};
consider p be Element of NAT such that
A1: b0 = a0|^p by X1, GR_CY_2:6;
b= a |^p by GROUP_4:2, A1;
hence ex p be Element of NAT st b = a|^p;
end;
given p be Element of NAT such that
A1: b = a|^p;
b = a0|^p by GROUP_4:2, A1;
hence thesis;
end;
theorem GRCY28:
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
proof
let G be finite Group, a be Element of G, n, p, s be Element of NAT;
assume
AS1: card gr{a} = n & n = p * s;
reconsider a0 = a as Element of gr{a} by GR_CY_2:2, STRUCT_0:def 5;
A0: gr{a0} = gr{a} by GR_CY_2:3;
ord(a0 |^ p) = card(gr{a0 |^ p}) by GR_CY_1:7
.= card(gr{a |^ p}) by GROUP_4:2, GR_CY_2:3
.= ord(a |^ p) by GR_CY_1:7;
hence ord(a |^ p) = s by A0, AS1, GR_CY_2:8;
end;
theorem GRCY212:
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
proof
let k be Element of NAT, G be finite Group,
a be Element of G;
set n = ord a;
reconsider a0 = a as Element of gr{a} by GR_CY_2:2, STRUCT_0:def 5;
A11: gr{a0} = gr{a} by GR_CY_2:3;
card (gr{a}) = n by GR_CY_1:7;
then gr{a} = gr{(a0 |^ k)} iff k gcd n = 1 by A11, GR_CY_2:12;
hence thesis by GROUP_4:2, GR_CY_2:3;
end;
theorem GRCY212A:
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)
proof
let k be Element of NAT, G be finite Group, a be Element of G;
assume k gcd (ord a) = 1; then
A1: gr{a} = gr{(a |^ k)} by GRCY212;
card (gr{a}) =ord a by GR_CY_1:7;
hence thesis by A1, GR_CY_1:7;
end;
theorem GRCY211:
for k being Element of NAT, G being finite Group, a being Element of G
holds (ord a) divides k * ord(a |^ k)
proof
let k be Element of NAT, G be finite Group, a be Element of G;
a in gr{a} by GR_CY_2:2; then
reconsider a0 = a as Element of gr{a};
A11: gr{a0} = gr{a} by GR_CY_2:3;
A12: card (gr{a}) = ord a by GR_CY_1:7;
ord(a |^ k) = card (gr{ a|^ k}) = card (gr{a0 |^ k})
by GR_CY_1:7, GROUP_4:2, GR_CY_2:3;
hence thesis by A11, A12, GR_CY_2:11;
end;
theorem GRCY212:
for G being Group, a, b being Element of G st b in gr{a}
holds gr{b} is strict Subgroup of gr{a}
proof
let G be Group, a, b be Element of G;
assume b in gr{a}; then
reconsider b0 = b as Element of gr{a};
gr{b0} = gr{b} by GR_CY_2:3;
hence thesis;
end;
definition
let G be strict commutative Group, x be Element of Subgroups G;
func modetrans(x) -> normal strict Subgroup of G equals
x;
correctness
proof
x is strict Subgroup of G by GROUP_3:def 1;
hence thesis by GROUP_3:116;
end;
end;
theorem GROUP252INV:
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)
proof
let G, H be Group, K be Subgroup of H, f be Homomorphism of G,H;
f.(1_G) = 1_H by GROUP_6:31;
then f.(1_G) in K by GROUP_2:46;
then reconsider
Ivf = f"(the carrier of K) as non empty Subset of (the carrier of G)
by FUNCT_2:38;
D191: for g1, g2 being Element of G st g1 in Ivf & g2 in Ivf
holds g1 * g2 in Ivf
proof
let g1, g2 be Element of G;
D94: f.(g1*g2) = (f.g1)*(f.g2) by GROUP_6:def 6;
assume g1 in Ivf & g2 in Ivf;
then f.g1 in K & f.g2 in K by FUNCT_2:38;
then (f.g1)*(f.g2) in K by GROUP_2:50;
hence g1*g2 in Ivf by D94, FUNCT_2:38;
end;
for g being Element of G st g in Ivf holds g" in Ivf
proof
let g be Element of G;
assume g in Ivf;
then f.g in K by FUNCT_2:38;
then (f.g)" in K by GROUP_2:51;
then f.(g") in the carrier of K by GROUP_6:32;
hence g" in Ivf by FUNCT_2:38;
end;
then
consider J be strict Subgroup of G such that
D19: the carrier of J = f"(the carrier of K) by GROUP_2:52, D191;
take J;
thus thesis by D19;
end;
theorem GRCY112:
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}
proof
let p be Nat, G be finite Group, x, d be Element of G;
assume
A1: ord d = p & p is prime;
assume x in gr{d};
then
X1: gr{x} is strict Subgroup of gr{d} by GRCY212;
X2: card (gr{d}) = p by A1, GR_CY_1:7;
gr{x} = (1).(gr{d}) implies x = 1_G
proof
assume
X3: gr{x} = (1).(gr{d});
x in the carrier of gr{x} by GR_CY_2:2, STRUCT_0:def 5;
then x in {1_(gr{d})} by X3, GROUP_2:def 7;
then x = 1_(gr{d}) by TARSKI:def 1;
hence x = 1_G by GROUP_2:44;
end;
hence thesis by GR_CY_1:12, A1, X1, X2;
end;
theorem LM204D:
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
proof
let G be Group, H, K be normal Subgroup of G;
assume
AS1: (the carrier of H) /\ (the carrier of K) = {1_G};
set f = nat_hom H;
set g = f| (the carrier of K);
for x1, x2 be object st x1 in dom g & x2 in dom g & g.x1 = g.x2
holds x1 = x2
proof
let x1, x2 be object;
assume
AS2: x1 in dom g & x2 in dom g & g.x1 = g.x2;
then
A1: x1 in (the carrier of K) & x1 in dom f by RELAT_1:57;
reconsider y1= x1 as Element of G by AS2;
A2: x2 in (the carrier of K) & x2 in dom f by AS2, RELAT_1:57;
reconsider y2 = x2 as Element of G by AS2;
A3: y1 * H = f.y1 by GROUP_6:def 8
.= g.x1 by A1, FUNCT_1:49
.= f.y2 by AS2, A2, FUNCT_1:49
.= y2*H by GROUP_6:def 8;
y1*(1_G) in y1*H by GROUP_2:46, GROUP_2:103;
then y1 in y2*H by A3, GROUP_1:def 4;
then consider h be Element of G such that
A4: y1 = y2*h & h in H by GROUP_2:103;
y1 in K & y2 in K by AS2, RELAT_1:57;
then y1 in K & y2" in K by GROUP_2:51;
then
A6: y2"*y1 in K by GROUP_2:50;
y2"*y1 in the carrier of H by A4, GROUP_1:13;
then y2"*y1 in {1_G} by AS1, XBOOLE_0:def 4, A6;
then y2"*y1 = 1_G by TARSKI:def 1;
then y2" = y1" by GROUP_1:12;
hence thesis by GROUP_1:9;
end;
hence thesis by FUNCT_1:def 4;
end;
theorem LM204L:
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})
proof
let G, F be finite commutative Group, a be Element of G,
f be Homomorphism of G, F;
for y be object
holds y in the carrier of gr{f.a} iff y in f.: (the carrier of gr{a})
proof
let y be object;
hereby
assume
AA1: y in the carrier of gr{f.a}; then
reconsider y0 =y as Element of F by TARSKI:def 3, GROUP_2:def 5;
y0 in gr{f.a} by AA1;
then consider i be Element of NAT such that
AA2: y0 =(f.a) |^i by GRCY26;
AA3: y0 = f.(a |^i) by AA2, GROUP_6:37;
a |^i in gr{a} by GRCY26;
hence y in f.: (the carrier of gr{a}) by AA3, FUNCT_2:35;
end;
assume y in f.: (the carrier of gr{a});
then consider x be object such that
AA2: x in dom f & x in (the carrier of gr{a}) & y = f.x by FUNCT_1:def 6;
reconsider x0 = x as Element of G by AA2;
x0 in gr{a} by AA2;
then consider i be Element of NAT such that
AA3: x0 = a |^i by GRCY26;
f.x0 = (f.a) |^i by AA3, GROUP_6:37;
then f.x0 in gr{f.a} by GRCY26;
hence y in the carrier of gr{f.a} by AA2;
end;
hence thesis by TARSKI:2;
end;
theorem LM204E:
for G, F being finite commutative Group, a be Element of G,
f be Homomorphism of G, F
holds ord(f.a) <= ord a
proof
let G, F be finite commutative Group, a be Element of G,
f be Homomorphism of G, F;
P1: the carrier of gr{f.a} = f.: (the carrier of gr{a}) by LM204L;
P2: card (gr{a}) = ord a by GR_CY_1:7;
P3: card (gr{f.a}) = ord(f.a) by GR_CY_1:7;
Segm card (the carrier of gr{f.a}) c= Segm card(the carrier of gr{a})
by P1, CARD_1:67;
hence thesis by P2, P3, NAT_1:39;
end;
theorem LM204F:
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
proof
let G, F being finite commutative Group, a be Element of G,
f be Homomorphism of G, F;
assume
AS: f is one-to-one;
P1: the carrier of gr{f.a} = f.: (the carrier of gr{a}) by LM204L;
P2: card (gr{a}) = ord a by GR_CY_1:7;
P3: card (gr{f.a}) = ord(f.a) by GR_CY_1:7;
dom f = the carrier of G by FUNCT_2:def 1;
then the carrier of gr{a}, the carrier of gr{f.a} are_equipotent
by P1, AS, CARD_1:33, GROUP_2:def 5;
hence thesis by P2, P3, CARD_1:5;
end;
theorem LM204G:
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
proof
let G, F be Group, H be Subgroup of G, f be Homomorphism of G, F;
(the carrier of H) c= the carrier of G by GROUP_2:def 5;
then reconsider g = f| (the carrier of H)
as Function of (the carrier of H),(the carrier of F) by FUNCT_2:32;
for a, b being Element of H holds g.(a * b) = g.a * g.b
proof
let a, b be Element of H;
a in G & b in G by STRUCT_0:def 5, GROUP_2:40;
then reconsider a0 = a,b0 = b as Element of G;
A4: f.a0 = g.a by FUNCT_1:49;
A5: f.b0 = g.b by FUNCT_1:49;
a*b = a0*b0 by GROUP_2:43;
hence g.(a * b) = f.(a0*b0) by FUNCT_1:49
.= (g.a) * (g.b) by GROUP_6:def 6, A4, A5;
end;
hence thesis by GROUP_6:def 6;
end;
theorem LM204H:
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
proof
let G, F be finite commutative Group, a be Element of G,
f be Homomorphism of G, F;
assume
AS: f| (the carrier of gr{a}) is one-to-one;
reconsider H = f| (the carrier of gr{a})
as Homomorphism of gr{a}, F by LM204G;
a in gr{a} by GR_CY_2:2;
then reconsider a0 = a as Element of gr{a};
f.a = H.a0 by FUNCT_1:49;
hence ord(f.a) = ord(a0) by AS, LM204F
.= card(gr{a0}) by GR_CY_1:7
.= card(gr{a}) by GR_CY_2:3
.= ord a by GR_CY_1:7;
end;
theorem LM204I:
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)
proof
let G be finite commutative Group,
p be Prime, m be Nat, a be Element of G;
assume
A1: card(G) = p|^m & a <> 1_G;
reconsider Gra = gr{a} as normal strict Subgroup of G by GROUP_3:116;
consider n1 be Nat such that
A8: (card Gra) = p|^n1 & n1 <= m by GROUPP_1:2, A1, GROUP_2:148;
ord a = p|^n1 by A8, GR_CY_1:7;
then n1 <> 0 by A1, GROUP_1:43, NEWTON:4;
then 1 <= n1 by NAT_1:14;
then n1-1 in NAT by INT_1:3, XREAL_1:48;
then reconsider n = n1-1 as Nat;
take n;
thus ord a = p|^(n+1) by A8, GR_CY_1:7;
end;
LM204K1:
for p being Prime, m, k be Nat st m divides (p|^k) & m <> 1
holds ex j be Nat st m = p|^(j+1)
proof
let p be Prime, m, k be Nat;
assume
AS1: m divides (p|^k) & m <> 1;
then consider r being Nat such that
P1: m = p |^ r & r <= k by GROUPP_1:2;
r <> 0 by P1, AS1, NEWTON:4;
then 1 <= r by NAT_1:14;
then r-1 in NAT by INT_1:3, XREAL_1:48;
then reconsider j = r-1 as Nat;
take j;
thus m = p |^(j+1) by P1;
end;
theorem LM204K:
for p being Prime, j, m, k be Nat st m = p|^k & not p divides j
holds j gcd m = 1
proof
let p be Prime, j, m, k be Nat;
assume
AS: m = p|^k & not p divides j;
assume
A1: j gcd m <> 1;
set q = j gcd m;
q divides j by NAT_D:def 5; then
A4: j=q*(j div q) by NAT_D:3;
q divides m by NAT_D:def 5;
then consider n be Nat such that
A5: q =p|^(n+1) by A1, LM204K1, AS;
j = (p|^n)*p*(j div q) by A4, A5, NEWTON:6
.= ((p|^n)*(j div q))*p;
hence contradiction by AS, INT_1:def 3;
end;
LM204A:
for G being strict finite commutative Group, p being Prime, m be Nat,
g be Element of G st card(G) = p|^m
& ord g = upper_bound Ordset G
ex K be normal strict Subgroup of G
st (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
proof
defpred P[Nat] means
for G being strict finite commutative Group, p being Prime,
g be Element of G st card(G) = p|^$1
& ord g = upper_bound Ordset G
ex K be normal strict Subgroup of G
st(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;
P0: P[0]
proof
let G be strict finite commutative Group, p be Prime,
g be Element of G;
assume
AS1: card(G) = p|^ 0 & ord g = upper_bound Ordset G;
reconsider H = G as strict finite Subgroup of G by GROUP_2:54;
card(H) = 1 by AS1, NEWTON:4; then
A1: (1).G = G by GROUP_2:70;
reconsider K = (1).G as normal strict Subgroup of G;
g in the carrier of (1).G by A1;
then g in {1_G} by GROUP_2:def 7;
then
A2: g = 1_G by TARSKI:def 1;
for x be object holds x in the carrier of gr{g} iff x in {1_G}
proof
let x be object;
hereby
assume
AA1: x in the carrier of gr{g}; then
reconsider x0 = x as Element of G by TARSKI:def 3, GROUP_2:def 5;
x0 in gr{g} by AA1;
then consider i be Element of NAT such that
AA2: x0 = g|^i by GRCY26;
x0 = 1_G by AA2, A2, GROUP_1:31;
hence x in {1_G} by TARSKI:def 1;
end;
assume x in {1_G};
then x = 1_G by TARSKI:def 1;
hence thesis by GROUP_2:46, STRUCT_0:def 5;
end;
then
X1: the carrier of gr{g} = {1_G} by TARSKI:2;
the carrier of K ={1_G} by GROUP_2:def 7;
then
X2: (the carrier of K) /\ (the carrier of gr{g})= {1_G} by X1;
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
proof
let x be Element of G;
x in the carrier of ((1).G) by A1;
then x in {1_G} by GROUP_2:def 7;
then x = 1_G by TARSKI:def 1; then
X3: x= 1_G * 1_G by GROUP_1:def 4;
1_G in gr{g} & 1_G in K by GROUP_2:46;
hence thesis by X3;
end;
hence thesis by X2;
end;
PN: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume AS1: P[k];
let G be strict finite commutative Group, p be Prime,
a be Element of G;
assume
A1: card(G) = p|^(k+1) & ord a = upper_bound Ordset G;
deffunc ordset(finite Group) = Ordset $1;
per cases;
suppose
CA1: card (gr{a}) = card G; then
P1: gr{a} = G by GROUP_2:73;
reconsider K = (1).G as normal strict Subgroup of G;
P2: the carrier of K = {1_G} by GROUP_2:def 7;
P3: the carrier of gr{a} = the carrier of G by CA1, GROUP_2:73;
X1: (the carrier of K) /\ (the carrier of gr{a})
= {1_G} by P2, P3, XBOOLE_1:28;
for x be Element of G holds
ex b1, a1 be Element of G st b1 in K & a1 in gr{a} & x = b1*a1
proof
let x be Element of G;
X2: x in gr{a} by P1;
X3: x= 1_G * x by GROUP_1:def 4;
1_G in K by GROUP_2:46;
hence thesis by X3, X2;
end;
hence thesis by X1;
end;
suppose
B2: card (gr{a}) <> card G;
reconsider Gra = gr{a} as normal strict Subgroup of G by GROUP_3:116;
reconsider
G1 = G ./.Gra as strict finite commutative Group by GROUP630;
A5: ord a = card(gr{a}) by GR_CY_1:7;
A6: card G = (ord a)* (index Gra) by A5, GROUP_2:147;
consider n1 be Nat such that
A8: (card Gra) = p|^n1 & n1 <= (k+1) by GROUPP_1:2, GROUP_2:148, A1;
(k+1)-n1 in NAT by A8, XREAL_1:48, INT_1:3;
then reconsider mn1 = (k+1)-n1 as Nat;
A9: ord a = p|^n1 by A8, GR_CY_1:7;
A10: ord a <> 0 by A8, GR_CY_1:7;
A10A: 0 < ord a by A8, GR_CY_1:7;
index Gra = (p|^(mn1+n1)) / (p|^n1) by A6, XCMPLX_1:89, A1, A9
.= (p|^mn1)*(p|^n1) / (p|^n1) by NEWTON:8
.= p|^(mn1) by XCMPLX_1:89; then
A11: card (G ./.Gra) = p|^(mn1) by GROUP_6:27;
consider b be Element of G such that
A20: not b in Gra by B2, GROUPP_1:12;
reconsider bga = b*Gra as Element of G1 by GROUP_2:def 15;
reconsider
Grbga = gr{bga} as normal strict Subgroup of G1 by GROUP_3:116;
consider s be Nat such that
A18: (card Grbga) = p|^s & s <= mn1 by GROUPP_1:2, GROUP_2:148, A11;
A19: ord bga = p|^s by A18, GR_CY_1:7;
ord bga <> 1
proof
assume ord bga = 1;
then bga = 1_G1 by GROUP_1:43;
then
A191: b*Gra = the carrier of Gra by GROUP_6:24;
b*(1_G) in b*Gra by GROUP_2:46, GROUP_2:103;
hence contradiction by A20, A191, GROUP_1:def 4;
end;
then s <> 0 by A19, NEWTON:4;
then 0 <= s-1 by NAT_1:14, XREAL_1:48;
then s-1 in NAT by INT_1:3;
then reconsider s1 = s-1 as Nat;
reconsider c = b|^(p|^s1) as Element of G;
reconsider cga = c*Gra as Element of G1 by GROUP_2:def 15;
A21: (p|^s1)*p = p|^(s1+1) by NEWTON:6
.= p|^s;
XN1: p|^s is Element of NAT & p|^s1 is Element of NAT
& p is Element of NAT by ORDINAL1:def 12;
A24: ord(bga |^(p|^s1)) = p by XN1, GRCY28, A21, A18;
A23: ord(cga) = p by A24, GROUPP_1:8;
A26: not c in Gra
proof
assume
A261: c in Gra;
cga = carr Gra by A261, GROUP_2:113
.= 1_G1 by GROUP_6:24;
then ord cga = 1 by GROUP_1:42;
hence contradiction by A23, INT_2:def 4;
end;
A24: cga |^p = 1_G1 by A23, GROUP_1:41;
A25: cga |^p = c |^p *Gra by GROUPP_1:8;
(c|^p)*(1_G) in (c |^p)*Gra by GROUP_2:46, GROUP_2:103;
then (c|^p) in (c |^p)*Gra by GROUP_1:def 4;
then (c|^p) in gr{a} by A24, A25, GROUP_6:24; then
consider j be Element of NAT such that
A26B: c|^p = a |^j by GRCY26;
p divides j
proof
assume not p divides j;
then
A27Z: j gcd (ord a) = 1 by A8, LM204K, GR_CY_1:7;
A272: ord(c|^p) = ord a by A26B, A27Z, GRCY212A;
A273: (ord c) = p * ord(c |^ p)
proof
ord(c|^p) <> 0 by A10, A26B, A27Z, GRCY212A; then
A274: (ord c) <= p * ord(c |^ p) by XN1, GRCY211, NAT_D:7;
c <> 1_G by A26, GROUP_2:46;
then
consider k be Nat such that
A2750: ord c = p|^(k+1) by A1, LM204I;
A275B: p*(p|^k) = ord c by A2750, NEWTON:6;
A275: (ord c)/p = p|^k by A275B, XCMPLX_1:89;
(c |^ p) |^(p|^k) = c |^(p*(p|^k)) by GROUP_1:35
.= 1_G by A275B, GROUP_1:41;
then ord(c |^ p) <= (ord c) /p by A275, NAT_D:7, GROUP_1:44;
then p*ord(c |^ p) <= (ord c) by XREAL_1:83;
hence thesis by A274, XXREAL_0:1;
end;
XXX0: 1*(ord a) < p*ord a by A10A, XREAL_1:68, INT_2:def 4;
ord c in Ordset G;
hence contradiction by XXX0, A1, A272, A273, SEQ_4:def 1;
end;
then consider j1 be Nat such that
A28: j =p*j1 by NAT_D:def 3;
A28A: j1 is Element of NAT by ORDINAL1:def 12;
set d= c*a|^(-j1);
A30: d|^p = c|^p*(a|^(-j1)) |^p by GROUP_1:38
.= c|^p*(a|^((-j1)*p)) by GROUP_1:35
.= c|^p*(a|^(-j)) by A28
.= c|^p*(a|^j)" by GROUP_1:36
.= 1_G by A26B, GROUP_1:def 5;
ord d <> 1
proof
assume ord d= 1;
then c*a|^(-j1) = 1_G by GROUP_1:43;
then c" = a|^(-j1) by GROUP_1:12;
then c" = (a|^j1)" by GROUP_1:36;
hence contradiction by A26, A28A, GRCY26, GROUP_1:9;
end;
then
A32: ord d = p by A30, INT_2:def 4, GROUP_1:44;
A33: not d in gr{a}
proof
assume d in gr{a};
then consider k be Element of NAT such that
A331: c*a|^(-j1) = a |^k by GRCY26;
c*(a|^j1)" = a |^k by GROUP_1:36, A331;
then c = (a |^k) *(a|^j1) by GROUP_1:14;
then c = a |^(j1+k) by GROUP_1:33;
hence contradiction by A26, GRCY26;
end;
A3Z: for x be object
holds x in (the carrier of gr{d}) /\ (the carrier of gr{a})
iff x in {1_G}
proof
let x0 be object;
hereby
assume
A310: x0 in (the carrier of gr{d}) /\ (the carrier of gr{a});
then
x0 in the carrier of gr{d}
& x0 in the carrier of gr{a} by XBOOLE_0:def 4;
then
reconsider x = x0 as Element of G by GROUP_2:def 5, TARSKI:def 3;
x in gr{d} by A310, XBOOLE_0:def 4;
then
A322: x = 1_G or gr{x} = gr{d} by GRCY112, A32;
x in gr{a} by A310, XBOOLE_0:def 4;
then
X1: gr{x} is strict Subgroup of gr{a} by GRCY212;
gr{x} <> gr{d}
proof
assume gr{x} = gr{d};
then
XX1: the carrier of gr{d} c= the carrier of gr{a}
by X1, GROUP_2:def 5;
d in gr{d} by GR_CY_2:2;
hence contradiction by A33, XX1;
end;
hence x0 in {1_G} by A322, TARSKI:def 1;
end;
assume x0 in {1_G};
then x0 = 1_G by TARSKI:def 1;
then x0 in (the carrier of gr{d})
& x0 in (the carrier of gr{a}) by GROUP_2:46, STRUCT_0:def 5;
hence thesis by XBOOLE_0:def 4;
end;
then
A33: (the carrier of gr{d}) /\ (the carrier of gr{a}) = {1_G}
by TARSKI:2;
reconsider Grd = gr{d} as normal strict Subgroup of G by GROUP_3:116;
reconsider G2 = G ./.Grd as strict finite commutative Group
by GROUP630;
D5: ord d = card(gr{d}) by GR_CY_1:7;
D6: card G = (ord d)* (index Grd) by D5, GROUP_2:147;
index Grd = (card G) / (ord d) by A32, D6, XCMPLX_1:89
.= p|^k *p /p by A1, A32, NEWTON:6
.= p|^k by XCMPLX_1:89; then
D11: card (G ./.Grd) = p|^k by GROUP_6:27;
set Ordset1 = Ordset G2;
set Pd = nat_hom Grd;
D130: Pd is onto by GROUP_6:59;
reconsider gd = Pd.a as Element of G2;
set H = Pd | (the carrier of Gra);
D14: H is one-to-one by A3Z, LM204D, TARSKI:2;
D14B: for r be Real st r in Ordset1 holds r <= ord gd
proof
assume not for r be Real st r in Ordset1 holds r <= ord gd;
then consider r be Real such that
D141: r in Ordset1 & not r <= ord gd;
D142: ord a < r by D141, D14, LM204H;
consider gx be Element of G2 such that
D143: r = ord gx by D141;
rng Pd = the carrier of G2 by D130, FUNCT_2:def 3;
then
consider a1 be Element of G such that
D232: gx = Pd.a1 by FUNCT_2:113;
ord gx <= ord a1 by D232, LM204E;
then
X1: ord a < ord a1 by XXREAL_0:2, D143, D142;
ord a1 in Ordset G;
hence contradiction by X1, A1, SEQ_4:def 1;
end;
XU1: upper_bound Ordset1 <= ord gd by SEQ_4:45, D14B;
ord gd in Ordset1;
then ord gd <= upper_bound Ordset1 by SEQ_4:def 1;
then ord gd = upper_bound Ordset1 by XXREAL_0:1, XU1;
then
consider K2 be normal strict Subgroup of G2 such that
D17: (the carrier of K2) /\ (the carrier of gr{gd}) = {1_G2}
& for g2 be Element of G2 holds
ex b2, a2 be Element of G2 st b2 in K2 & a2 in gr{gd} & g2 = b2*a2
by AS1, D11;
consider K be strict Subgroup of G such that
D19: the carrier of K = Pd"(the carrier of K2) by GROUP252INV;
reconsider K as normal strict Subgroup of G by GROUP_3:116;
D20: for x be Element of G
st x in (the carrier of K) /\ (the carrier of gr{a})
holds Pd.x in (the carrier of K2) /\ (the carrier of gr{Pd.a})
proof
let x be Element of G;
assume
D20A: x in (the carrier of K) /\ (the carrier of gr{a});
then
D20B: x in (the carrier of gr{a})
& x in (the carrier of K) by XBOOLE_0:def 4;
x in gr{a} by D20A, XBOOLE_0:def 4; then
consider k be Element of NAT such that
D20C: x= a|^ k by GRCY26;
XXX: Pd.x is Element of G2;
Pd.x = ((Pd.a) |^k) by D20C, GROUP_6:37;
then
D233: Pd.x in gr{Pd.a} by XXX, GRCY26;
Pd.x in the carrier of K2 by D20B, D19, FUNCT_2:38;
hence thesis by D233, XBOOLE_0:def 4;
end;
D22: for x be Element of G
st x in (the carrier of K) /\ (the carrier of gr{a})
holds x in (the carrier of Ker Pd) /\ (the carrier of gr{a})
proof
let x be Element of G;
assume
D22A: x in (the carrier of K) /\ (the carrier of gr{a});
then Pd.x in {1_G2} by D17, D20;
then Pd.x = 1_G2 by TARSKI:def 1;
then x in {s where s is Element of G : Pd.s= 1_G2 };
then
D22B: x in (the carrier of (Ker Pd)) by GROUP_6:def 9;
x in (the carrier of gr{a}) by D22A, XBOOLE_0:def 4;
hence thesis by D22B, XBOOLE_0:def 4;
end;
D23A: (the carrier of K) /\ (the carrier of gr{a}) c= {1_G}
proof let x be object;
assume
D221: x in (the carrier of K) /\ (the carrier of gr{a});
then x in (the carrier of K) by XBOOLE_0:def 4; then
reconsider x0 = x as Element of G by TARSKI:def 3, GROUP_2:def 5;
x0 in (the carrier of (Ker Pd)) /\ (the carrier of gr{a})
by D22, D221; then
D222: x0 in the carrier of gr{a}
& x0 in the carrier of Ker Pd by XBOOLE_0:def 4; then
x0 in the carrier of (gr{d}) by GROUP_6:43;
hence x in {1_G} by A33, D222, XBOOLE_0:def 4;
end;
1_G in (the carrier of gr{a}) & 1_G in (the carrier of K)
by STRUCT_0:def 5, GROUP_2:46;
then 1_G in (the carrier of K) /\ (the carrier of gr{a})
by XBOOLE_0:def 4; then
D23B: {1_G } c= (the carrier of K) /\ (the carrier of gr{a})
by ZFMISC_1:31;
for g be Element of G
holds ex b1, a1 be Element of G st b1 in K & a1 in gr{a} & g = b1*a1
proof
let g be Element of G;
reconsider g2 = Pd.g as Element of G2;
consider b2, a2 be Element of G2 such that
D231: b2 in K2 & a2 in gr{gd} & g2 = b2*a2 by D17;
consider i be Element of NAT such that
D231A: a2 = gd|^ i by GRCY26, D231;
rng Pd = the carrier of G2 by D130, FUNCT_2:def 3;
then consider b1 be Element of the carrier of G such that
D232: b2 = Pd.b1 by FUNCT_2:113;
D234: Pd.((a|^i)*b1) = (Pd.(a|^i))*(Pd.b1)by GROUP_6:def 6
.= Pd.g by D231A, D231, D232, GROUP_6:37;
D235: ((a|^i)*b1)* gr{d} = Pd.((a|^i)*b1) by GROUP_6:def 8
.= g*gr{d} by D234, GROUP_6:def 8;
g*1_G in (g*gr{d}) by GROUP_2:46, GROUP_2:103;
then g in ((a|^i)*b1)* gr{d} by D235, GROUP_1:def 4;
then consider y be Element of G such that
D236: g=((a|^i)*b1)* y & y in gr{d} by GROUP_2:103;
D236A: g=(a|^i)*(b1*y) by D236, GROUP_1:def 3;
consider j be Element of NAT such that
D237: y =d|^ j by GRCY26, D236;
D238: Pd.d = d*gr{d} by GROUP_6:def 8
.= carr gr{d} by GR_CY_2:2, GROUP_2:113
.= 1_G2 by GROUP_6:24;
D239: Pd.y = (Pd.d) |^ j by D237, GROUP_6:37
.= 1_G2 by D238, GROUP_1:31;
1_G2 in the carrier of K2 by GROUP_2:46, STRUCT_0:def 5;
then b1 in K & y in K by D19, D231, D232, D239, FUNCT_2:38;
then b1 * y in K by GROUP_2:50;
hence thesis by D236A, GRCY26;
end;
hence thesis by D23A, D23B, XBOOLE_0:def 10;
end;
end;
for k be Nat holds P[k] from NAT_1:sch 2(P0, PN);
hence thesis;
end;
begin :: Isomorphism of cyclic groups of prime-power order
theorem LM204:
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
proof
let G be strict finite commutative Group, p be Prime, m be Nat;
assume
AS: card(G) = p|^m;
consider g be Element of G such that
A0: ord g = upper_bound Ordset G by LM202;
consider K be normal strict Subgroup of G such that
P1: (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
by AS, A0, LM204A;
consider n be Nat such that
Q4: (card gr{g}) = p|^n & n <= m by AS, GROUPP_1:2, GROUP_2:148;
m - n in NAT by Q4, INT_1:3, XREAL_1:48;
then reconsider k= m - n as Nat;
gr{g} is normal Subgroup of G by GROUP_3:116; then
consider F being Homomorphism of product <* K,gr{g} *>, G such that
P5: F is bijective
& for a,b be Element of G st a in K & b in gr{g}
holds F.(<*a,b*>) = a*b by P1, GROUP_17:12;
set s = card K;
set t = card gr{g};
F is one-to-one & dom F = the carrier of product <*K,gr{g}*>
& rng F = the carrier of G by P5, FUNCT_2:def 1, FUNCT_2:def 3; then
X6: card (product <*K,gr{g}*>) = card G by CARD_1:5, WELLORD2:def 4;
(card K) * (p|^n) = p|^(k + n) by X6, Q4, AS, GROUP_17:17
.= (p|^k)*(p|^n) by NEWTON:8;
then card K =(p|^k) by XCMPLX_1:5;
hence thesis by A0, P1, P5, Q4, GR_CY_1:7;
end;
theorem LM205A:
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
proof
defpred P[Nat] means
for G being strict finite commutative Group, p being Prime
st card(G) = p|^$1 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 i, j be Element of Seg k st i <> j
holds (the carrier of (F.i)) /\ (the carrier of (F.j)) = {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;
P1: for n being Nat st for k being Nat st k < n holds P[k] holds P[n]
proof
let n be Nat;
assume
APN: for k being Nat st k < n holds P[k];
thus P[n]
proof
let G be strict finite commutative Group, p be Prime;
assume
AS1: card(G) = p|^n; then
consider H be normal strict Subgroup of G, n0, m0 be Nat,
g0 be Element of G such that
P8: ord g0 = upper_bound Ordset G
& H is finite & H is commutative
& (the carrier of H) /\ (the carrier of gr{g0}) = {1_G}
& (for x be Element of G
holds ex b1, a1 be Element of G st b1 in H & a1 in gr{g0} & x = b1*a1)
& ord g0 = p|^n0
& m0 = n - n0 & n0 <= n
& card H = p|^m0
& ex I0 being Homomorphism of product <*H,gr{g0}*>, G
st I0 is bijective
& for a, b be Element of G st a in H & b in gr{g0}
holds I0.(<*a,b*>) = a*b by LM204;
per cases;
suppose
BBB: n = n0;
reconsider q = 1 as non zero Nat;
set K = gr{g0};
set I = {q};
set F = I --> G;
card G = card gr{g0} by AS1, BBB, P8, GR_CY_1:7; then
X10: G = gr{g0} by GROUP_2:73;
reconsider a=<*g0*> as q-element FinSequence of G by FINSEQ_1:74;
VV1: n0 is Element of NAT by ORDINAL1:def 12;
reconsider Inda=<*n0*> as q-element FinSequence of NAT
by VV1, FINSEQ_1:74;
Z1: for i be Nat st i in Seg q
holds ex ai be Element of G
st ai = a.i & F.i = gr{ai} & ord(ai) = p|^(Inda.i)
proof
let i be Nat;
assume
ASD1: i in Seg q;
D57: i = 1 by TARSKI:def 1, ASD1, FINSEQ_1:2;
then
D58: Inda.i = n0;
a.i = g0 by D57;
hence thesis by ASD1, D58, P8, X10, FINSEQ_1:2, FUNCOP_1:7;
end;
Z2: for i be Nat st 1 <= i & i <= q -1 holds Inda.i <= Inda.(i+1)
proof
let i be Nat;
assume 1 <= i & i <= q -1;
then 1 <= i & i <= 0;
hence thesis;
end;
reconsider F as multMagma-Family of I;
GG1: for s,t be Element of I st s <> t holds
(the carrier of (F.s)) /\ (the carrier of (F.t)) ={1_G}
proof
let s, t be Element of I;
s=q by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
reconsider F as associative Group-like commutative
multMagma-Family of I;
F = q .--> G; then
consider HFG be Homomorphism of product F, G such that
X4: HFG is bijective
& for x be (the carrier of G)-valued total {q}-defined Function
holds HFG.x =Product x by GROUP_17:26;
F = q .--> G;
then for x be (the carrier of G)-valued total I -defined Function
st for p be Element of I
holds x.p in F.p holds x in product F & HFG.x = Product x
by X4, GROUP_17:25;
hence thesis by X4, GG1, Z1, Z2, FINSEQ_1:2;
end;
suppose
AAA: n <> n0;
0 <> n0
proof
assume X0: n0 = 0;
then
X1: ord g0 = 1 by P8, NEWTON:4;
for z be object
holds z in the carrier of G iff z in {1_G}
proof
let z be object;
hereby assume z in the carrier of G;
then
reconsider x=z as Element of G;
ord x in Ordset G; then
X2: ord x <= 1 by X1, P8, SEQ_4:def 1;
ord x = card gr{x} by GR_CY_1:7;
then 1 <= ord x by GROUP_1:45;
then x = 1_G by X2, XXREAL_0:1, GROUP_1:43;
hence z in {1_G} by TARSKI:def 1;
end;
assume z in {1_G};
hence z in the carrier of G;
end; then
XX1: the carrier of G = {1_G} by TARSKI:2;
n = 0
proof
assume n <> 0;
then 1 < p to_power n by POWER:35, INT_2:def 4;
hence contradiction by AS1, XX1, CARD_1:30;
end;
hence contradiction by X0, AAA;
end;
then n - n0 < n - (0 qua Real) by XREAL_1:15;
then
consider k0 be non zero Nat,
a0 be k0-element FinSequence of H,
Inda0 be k0-element FinSequence of NAT,
F0 be associative Group-like commutative multMagma-Family
of (Seg k0), HFG0 be Homomorphism of product F0,H such that
P12:
(for i be Nat st i in Seg k0 holds ex ai be Element of H
st ai = a0.i & F0.i = gr{ai} & ord(ai) = p|^(Inda0.i))
& (for i be Nat st 1 <= i & i <= k0-1 holds Inda0.i <= Inda0.(i+1))
& (for p, q be Element of Seg k0 st p <> q
holds (the carrier of (F0.p)) /\ (the carrier of (F0.q)) ={1_H})
& HFG0 is bijective
& for x be (the carrier of H)-valued total (Seg k0) -defined Function
st for p be Element of (Seg k0)
holds x.p in F0.p
holds x in product F0 & HFG0.x = Product x by P8, APN;
reconsider q = k0+1 as non zero Nat;
set K = gr{g0};
set F = F0 +* ({q}--> K);
set I0 = Seg k0;
set I = Seg q;
INDK1: Inda0.k0 <= n0
proof
assume
K1: not Inda0.k0 <= n0;
K2: 1 <= k0 by NAT_1:14;
1 < p by INT_2:def 4;
then
K3: p to_power n0 < p to_power (Inda0.k0) by K1, POWER:39;
k0 in Seg k0 by K2;
then
consider ai be Element of H such that
C5: ai = a0.k0 & F0.k0 = gr{ai} & ord(ai) = p|^(Inda0.k0) by P12;
reconsider aai = ai as Element of G by TARSKI:def 3, GROUP_2:def 5;
D54: gr{aai} = gr{ai} by GR_CY_2:3;
D55: ord(aai) = card(gr{ai}) by D54, GR_CY_1:7
.= p|^(Inda0.k0) by C5, GR_CY_1:7;
(ord aai) in Ordset G;
hence contradiction by D55, K3, P8, SEQ_4:def 1;
end;
NU0: q is Element of I by FINSEQ_1:4;
DIQ1: for x be object holds x in I0 iff x in I & not x in {q}
proof
let x be object;
hereby
assume
X1: x in I0; then
reconsider x1 = x as Nat;
X4: k0 < k0+1 by NAT_1:16;
x1 <> k0+1 by X1, NAT_1:16, FINSEQ_1:1;
hence x in I & not x in {q}
by X1, X4, FINSEQ_1:5, TARSKI:def 1, TARSKI:def 3;
end;
assume
X1: x in I & not x in {q}; then
reconsider x1 = x as Nat;
X2: 1 <= x1 & x1 <= q by X1, FINSEQ_1:1;
x1 <> q by X1, TARSKI:def 1;
then x1 < k0+1 by X2, XXREAL_0:1;
then x1 <= k0 by NAT_1:13;
hence x in I0 by X2;
end;
then
DIQ0: I0 = I \ {q} by XBOOLE_0:def 5;
NU1: not q in I0
proof
assume q in I0;
then q in I & not q in {q} by DIQ1;
hence contradiction by TARSKI:def 1;
end;
XB1: {q} c= I by FINSEQ_1:4, ZFMISC_1:31;
NU2: I0 \/ {q} = I by DIQ0, XB1, XBOOLE_1:45;
<* g0 *> is FinSequence of G by FINSEQ_1:74;
then
VV1: rng <*g0*> c= the carrier of G by FINSEQ_1:def 4;
the carrier of H c= the carrier of G by GROUP_2:def 5;
then
VV4: rng a0 c= the carrier of G by XBOOLE_1:1;
rng (a0^<*g0*>) = (rng a0) \/ rng (<*g0*>) by FINSEQ_1:31;
then
reconsider a = a0^<*g0*> as q-element FinSequence of G
by VV1, VV4, XBOOLE_1:8, FINSEQ_1:def 4;
rng (Inda0^<*n0*>) = (rng Inda0) \/ (rng (<*n0*>)) by FINSEQ_1:31;
then reconsider
Inda = Inda0^<*n0*> as q-element FinSequence of NAT
by FINSEQ_1:def 4;
LL1: len a0 = k0 by CARD_1:def 7;
LL2: len Inda0 = k0 by CARD_1:def 7;
EX1: for i be Nat st 1 <= i & i <= q -1 holds Inda.i <= Inda.(i+1)
proof
let i be Nat;
assume
EX11: 1 <= i & i <= q -1;
EX13: dom Inda0 = I0 by LL2, FINSEQ_1:def 3;
1 <= k0 by NAT_1:14;
then k0 - 1 in NAT by INT_1:3, XREAL_1:48;
then reconsider k01 = k0 - 1 as Nat;
per cases;
suppose
C1: i <> q -1;
then i < k0 by EX11, XXREAL_0:1;
then
C2: i + 1 <= k0 -1 + 1 by NAT_1:13;
i < k01+1 by C1, EX11, XXREAL_0:1;
then
C6: i <= k01 by NAT_1:13;
i in Seg k0 by EX11;
then
D56: Inda.i = Inda0.i by EX13, FINSEQ_1:def 7;
1 <= i+1 by NAT_1:11;
then i+1 in Seg k0 by C2;
then Inda.(i+1) = Inda0.(i+1) by EX13, FINSEQ_1:def 7;
hence Inda.i <= Inda.(i+1) by D56, P12, C6, EX11;
end;
suppose
C2: i = q -1;
i in Seg k0 by EX11;
then Inda.i = Inda0.i by EX13, FINSEQ_1:def 7;
hence Inda.i <= Inda.(i+1) by C2, INDK1, LL2, FINSEQ_1:42;
end;
end;
D1: dom F = dom F0 \/ dom ({q}--> K) by FUNCT_4:def 1
.= I0 \/ dom ({q}--> K) by PARTFUN1:def 2
.= I0 \/ {q}; then
reconsider F as I -defined Function by NU2, RELAT_1:def 18;
reconsider F as ManySortedSet of I by NU2, PARTFUN1:def 2, D1;
reconsider F as multMagma-Family of I;
P12A:for x be Element of I0
holds F0.x is strict finite commutative Group
& F0.x is Subgroup of H
proof
let x be Element of I0;
reconsider i = x as Nat;
consider ai be Element of H such that
X1: ai = a0.i & F0.i = gr{ai} & ord(ai) = p|^(Inda0.i) by P12;
thus F0.x is strict finite commutative Group
& F0.x is Subgroup of H by X1;
end;
XPF: for i be Nat st i in I holds ex ai be Element of G
st ai = a.i & F.i = gr{ai} & ord(ai) = p|^(Inda.i)
proof
let i be Nat;
assume
DD: i in I;
F5: i in dom F0 \/ dom ({q}--> K) by D1, DD, NU2, FUNCT_4:def 1;
per cases by DD, NU2, XBOOLE_0:def 3;
suppose
D51: i in I0;
then not i in dom ({q}--> K) by DIQ1;
then
D52: F.i = F0.i by F5, FUNCT_4:def 1;
consider ai be Element of H such that
D53: ai = a0.i & F0.i = gr{ai} & ord(ai) = p|^(Inda0.i)
by P12, D51;
ai in H;
then
reconsider aai = ai as Element of G
by GROUP_2:40, STRUCT_0:def 5;
D54: gr{aai} = gr{ai} by GR_CY_2:3;
D55: ord(aai) = card(gr{aai}) by GR_CY_1:7
.= ord(ai) by D54, GR_CY_1:7;
dom Inda0 = I0 by LL2, FINSEQ_1:def 3;
then
D56: Inda.i = Inda0.i by D51, FINSEQ_1:def 7;
dom a0 = I0 by LL1, FINSEQ_1:def 3;
then a.i = a0.i by D51, FINSEQ_1:def 7;
hence
ex ai be Element of G
st ai = a.i & F.i = gr{ai} & ord(ai) = p|^(Inda.i)
by D52, D53, D54, D55, D56;
end;
suppose
D52: i in {q};
D55:F.i = ({q}--> K).i by FUNCT_4:def 1, F5, D52
.= gr{g0} by D52, FUNCOP_1:7;
D56: i =q by TARSKI:def 1, D52;
D57: a.i = g0 by LL1, FINSEQ_1:42, D56;
ord g0 = p|^(Inda.i) by P8, D56, LL2, FINSEQ_1:42;
hence ex ai be Element of G
st ai = a.i & F.i = gr{ai} & ord(ai) = p|^(Inda.i) by D55, D57;
end;
end;
XPFA:
for x be Element of I
holds F.x is strict finite commutative Group & F.x is Subgroup of G
proof
let x be Element of I;
reconsider i = x as Nat;
consider ai be Element of G such that
X1: ai = a.i & F.i = gr{ai} & ord(ai) = p|^(Inda.i) by XPF;
thus thesis by X1;
end;
AR1: for i being Element of I holds F .i is Group-like by XPFA;
AR2: for i being Element of I holds F .i is associative by XPFA;
for i being Element of I holds F .i is commutative by XPFA;
then
reconsider
F as associative Group-like commutative multMagma-Family of I
by AR1, GROUP_7:def 6, AR2, GROUP_7:def 7, GROUP_7:def 8;
consider FHKG being Homomorphism of product <*H, K*>, G such that
XX1: FHKG is bijective
& for a, b be Element of G st a in H & b in K
holds FHKG.(<*a,b*>) = a*b by P8;
XF1: F = F0 +* (q.--> K);
then
consider FHK be Homomorphism of (product F), product <*H, K*>
such that
D7: FHK is bijective
& for x0 be Function, k be Element of K, h be Element of H
st h = HFG0.x0 & x0 in (product F0)
holds FHK.(x0 +* (q.-->k)) = <* h, k *>
by GROUP_17:28, P12, NU0, NU2, NU1;
reconsider HFG = FHKG*FHK as Function of (product F), G;
XX2: HFG is onto by FUNCT_2:27, XX1, D7;
reconsider HFG as Homomorphism of (product F), G;
DX2: for x be (the carrier of G)-valued total I -defined Function
st for p be Element of I holds x.p in F.p
holds x in product F & HFG.x =Product x
proof
let x be (the carrier of G)-valued total I -defined Function;
assume
U1: for p be Element of I holds x.p in F.p;
then x in the carrier of product F by GROUP_17:29;
then
consider x0 be total I0 -defined Function, k be Element of K
such that
U3: x0 in (product F0)
& x = x0 +* (q.-->k) & for p be Element of I0 holds x0.p in F0.p
by XF1, GROUP_17:30, NU2, NU1, NU0;
reconsider h = HFG0.x0 as Element of H by FUNCT_2:5, U3;
reconsider hh=h,kk=k as Element of G by GROUP_2:42;
now
let y be object;
assume y in rng x0;
then
consider z be object such that
DX11: z in dom x0 & y = x0.z by FUNCT_1:def 3;
reconsider z as Element of I0 by DX11;
DX13: x0.z in F0.z by U3;
F0.z is Subgroup of H by P12A;
hence y in the carrier of H
by DX11, STRUCT_0:def 5, DX13, GROUP_2:40;
end;
then reconsider x0 as
(the carrier of H)-valued total I0 -defined Function
by RELAT_1:def 19, TARSKI:def 3;
U5: HFG0.x0 =Product x0 by P12, U3;
the carrier of H c= the carrier of G by GROUP_2:def 5;
then rng x0 c= the carrier of G by XBOOLE_1:1;
then reconsider xx0 = x0 as (the carrier of G)-valued
total I0 -defined Function by RELAT_1:def 19;
U50: Product x0 = Product xx0 by GROUP_17:32;
thus x in product F by GROUP_17:29, U1;
U6: hh in H & kk in K;
thus HFG.x = FHKG.(FHK.x) by FUNCT_2:15, GROUP_17:29, U1
.= FHKG.(<* hh, kk *>) by D7, U3
.= hh*kk by XX1, U6
.= Product x by U5, U50, NU0, NU2, NU1, GROUP_17:33, U3;
end;
for s, t be Element of I st s <> t
holds (the carrier of (F.s)) /\ (the carrier of (F.t)) = {1_G}
proof
let s, t be Element of I;
assume
AA1: s <> t;
dom F = I by PARTFUN1:def 2;
then
D4: s in dom F & t in dom F;
per cases;
suppose s in I0 & t in I0;
then
reconsider ss = s, tt = t as Element of I0;
F5: s in dom F0 \/ dom ({q}--> K) by D4, FUNCT_4:def 1;
K5: t in dom F0 \/ dom ({q}--> K) by D4, FUNCT_4:def 1;
not ss in dom ({q}--> K) by DIQ1;
then
D52: F.ss = F0.ss by FUNCT_4:def 1, F5;
not tt in dom ({q}--> K) by DIQ1;
then
K52: F.tt = F0.tt by FUNCT_4:def 1, K5;
(the carrier of (F0.ss)) /\ (the carrier of (F0.tt)) ={1_H}
by P12, AA1;
hence
(the carrier of (F.s)) /\ (the carrier of (F.t)) ={1_G}
by D52, K52, GROUP_2:44;
end;
suppose
AA3: not (s in I0 & t in I0);
thus (the carrier of (F.s)) /\ (the carrier of (F.t)) = {1_G}
proof
per cases by AA3;
suppose
AA31: not s in I0;
F5: s in dom F0 \/ dom ({q}--> K) by D4, FUNCT_4:def 1;
D52: s in {q} by AA31, DIQ1;
then F.s = ({q}--> K).s by FUNCT_4:def 1, F5;
then
D55: F.s = K by D52, FUNCOP_1:7;
t in I0
proof
assume not t in I0;
then not t in I or t in {q} by DIQ1;
then t = q by TARSKI:def 1;
hence contradiction by AA1, TARSKI:def 1, D52;
end;
then
reconsider tt = t as Element of I0;
K5: tt in dom F0 \/ dom ({q}--> K) by D4, FUNCT_4:def 1;
not tt in dom ({q}--> K) by DIQ1;
then
K52: F.tt = F0.tt by FUNCT_4:def 1, K5;
reconsider S1=F0.tt as Subgroup of H by P12A;
K55: (the carrier of K) /\ (the carrier of S1) c= {1_G}
by P8, XBOOLE_1:26, GROUP_2:def 5;
K56: 1_G in the carrier of K by GROUP_2:46, STRUCT_0:def 5;
1_G in the carrier of S1 by GROUP_2:46, STRUCT_0:def 5;
then 1_G in (the carrier of K) /\ (the carrier of S1)
by XBOOLE_0:def 4, K56;
then {1_G } c= (the carrier of K) /\ (the carrier of S1)
by ZFMISC_1:31;
hence
(the carrier of (F.s)) /\ (the carrier of (F.t)) = {1_G}
by D55, K52, K55, XBOOLE_0:def 10;
end;
suppose
AA32: not t in I0;
F5: t in dom F0 \/ dom ({q}--> K) by D4, FUNCT_4:def 1;
D52: t in {q} by AA32, DIQ1;
then F.t = ({q}--> K).t by FUNCT_4:def 1, F5;
then
D55: F.t = K by D52, FUNCOP_1:7;
s in I0
proof
assume not s in I0;
then not s in I or s in {q} by DIQ1;
then s = q by TARSKI:def 1;
hence contradiction by AA1, TARSKI:def 1, D52;
end;
then
reconsider ss = s as Element of I0;
K5: ss in dom F0 \/ dom ({q}--> K) by D4, FUNCT_4:def 1;
not ss in dom ({q}--> K) by DIQ1;
then
K52: F.ss = F0.ss by FUNCT_4:def 1, K5;
reconsider S1=F0.ss as Subgroup of H by P12A;
K55:
(the carrier of K) /\ (the carrier of S1) c= {1_G}
by P8, XBOOLE_1:26, GROUP_2:def 5;
K56: 1_G in the carrier of K by GROUP_2:46, STRUCT_0:def 5;
1_G in the carrier of S1 by GROUP_2:46, STRUCT_0:def 5;
then 1_G in (the carrier of K) /\ (the carrier of S1)
by XBOOLE_0:def 4, K56;
then {1_G} c= (the carrier of K) /\ (the carrier of S1)
by ZFMISC_1:31;
hence (the carrier of (F.s)) /\ (the carrier of (F.t)) ={1_G}
by D55, K52, K55, XBOOLE_0:def 10;
end;
end;
end;
end;
hence thesis by EX1, XPF, XX2, XX1, D7, DX2;
end;
end;
end;
for k be Nat holds P[k] from NAT_1:sch 4(P1);
hence thesis;
end;
XLM18Th401:
for I be non empty finite set, F be associative Group-like
multMagma-Family of I, x be set st x in the carrier of product F
holds x is total I-defined Function
proof
let I be non empty finite set, F be associative Group-like
multMagma-Family of I, x be set;
assume
A1: x in the carrier of product F;
D1: dom (Carrier F) = I by PARTFUN1:def 2;
the carrier of product F = product (Carrier F) by GROUP_7:def 2;
then consider f be Function such that
D2: x = f & dom f = dom (Carrier F) &
for y be object st y in dom (Carrier F) holds f.y in (Carrier F).y
by CARD_3:def 5, A1;
thus thesis by D2, D1, RELAT_1:def 18, PARTFUN1:def 2;
end;
XLM18Th402:
for I be non empty finite set, F be associative Group-like
multMagma-Family of I, f be Function
st f in the carrier of product F holds
for x be set st x in I
holds ex R be non empty multMagma st R = F.x & f.x in the carrier of R
proof
let I be non empty finite set, F be associative Group-like
multMagma-Family of I, f be Function;
assume
A1: f in the carrier of product F;
D1: dom (Carrier F) = I by PARTFUN1:def 2;
the carrier of product F = product (Carrier F) by GROUP_7:def 2;
then consider g be Function such that
D2: f = g & dom g = dom (Carrier F) &
for y be object st y in dom (Carrier F) holds g.y in (Carrier F).y
by CARD_3:def 5, A1;
let x be set;
assume
A2: x in I;
consider R being 1-sorted such that
A4: R = F .x & (Carrier F) .x = the carrier of R by PRALG_1:def 15,A2;
x in dom F by A2, PARTFUN1:def 2;
then R in rng F by A4, FUNCT_1:3;
then R is non empty multMagma by GROUP_7:def 1;
hence thesis by A2, D2, D1, A4;
end;
theorem
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
proof
let G be strict finite commutative Group, p be Prime, m be Nat;
assume card(G) = p|^m;
then consider 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 such that
P1: (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 by LM205A;
set I = Seg k;
P4: for y be Element of G holds
ex x be (the carrier of G)-valued total I -defined Function
st (for p be Element of I holds x.p in F.p) & y = Product x
proof
let y be Element of G;
y in the carrier of G;
then y in rng HFG by P1, FUNCT_2:def 3;
then consider x be object such that
P2: x in the carrier of product F & y = HFG.x by FUNCT_2:11;
reconsider x as total I-defined Function by P2, XLM18Th401;
P3: for p be Element of I holds x.p in F.p
proof
let p be Element of I;
consider R be non empty multMagma such that
P4: R = F.p & x.p in the carrier of R by XLM18Th402, P2;
thus x.p in (F.p) by P4;
end;
rng x c= the carrier of G
proof
let y be object;
assume y in rng x;
then consider i be object such that
D2: i in dom x & y = x.i by FUNCT_1:def 3;
reconsider i as Element of I by D2;
consider R be non empty multMagma such that
P4: R = F.i & x.i in the carrier of R by P2, XLM18Th402;
reconsider i0 = i as Nat;
consider ai be Element of G such that
XX2: ai = a.i0 & F.i0 = gr{ai} & ord(ai) = p|^(Inda.i0) by P1;
the carrier of (F.i) c= the carrier of G by XX2, GROUP_2:def 5;
hence y in the carrier of G by D2, P4;
end;
then
reconsider x as (the carrier of G)-valued total I -defined Function
by RELAT_1:def 19;
take x;
thus thesis by P1, P2, P3;
end;
now
let x1, x2 be (the carrier of G)-valued total I -defined Function;
assume
AS2: (for p be Element of I holds x1.p in F.p)
& (for p be Element of I holds x2.p in F.p)
& Product x1 = Product x2;
x1 in product F & HFG.x1 =Product x1 by AS2, P1; then
P4: HFG.x1 = HFG.x2 by AS2, P1;
x1 in the carrier of product F
& x2 in the carrier of product F by AS2, P1, STRUCT_0:def 5;
hence x1 = x2 by P4, P1, FUNCT_2:19;
end;
hence thesis by P1, P4;
end;