:: Properties of Groups
:: by Gijs Geleijnse and Grzegorz Bancerek
::
:: Received May 31, 2004
:: Copyright (c) 2004-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 NUMBERS, STRUCT_0, GROUP_1, SUBSET_1, GROUP_2, FINSET_1, INT_2,
CARD_1, GRAPH_1, RELAT_1, TARSKI, ALGSTR_0, ZFMISC_1, PBOOLE, REALSET1,
NEWTON, INT_1, ARYTM_3, GROUP_4, ARYTM_1, NAT_1, FINSEQ_1, FUNCT_1,
XXREAL_0, CQC_SIM1, XBOOLE_0, SETFAM_1, GROUP_8;
notations XBOOLE_0, CARD_1, TARSKI, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, RELAT_1, REALSET1, FUNCT_1, FUNCT_2, PBOOLE, INT_1,
NAT_1, FINSET_1, GROUP_2, GROUP_4, GR_CY_1, FINSEQ_1, DOMAIN_1, STRUCT_0,
ALGSTR_0, GROUP_1, INT_2;
constructors WELLORD2, BINOP_1, REAL_1, NAT_D, BINOP_2, REALSET2, GROUP_4,
GR_CY_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
FINSEQ_1, STRUCT_0, GROUP_1, GROUP_2, GR_CY_1, ORDINAL1, FINSET_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FUNCT_1, WELLORD2, STRUCT_0;
equalities REALSET1, ALGSTR_0, ORDINAL1;
expansions TARSKI, STRUCT_0;
theorems GROUP_2, GR_CY_1, GR_CY_2, NAT_1, TARSKI, XBOOLE_0, GROUP_1, CARD_1,
GROUP_6, ALTCAT_1, FUNCT_2, GROUP_4, INT_2, XCMPLX_1, INT_1, FINSEQ_1,
FUNCT_1, NEWTON, ORDINAL1, NAT_D, XXREAL_0, RELAT_1, PARTFUN1;
schemes SUBSET_1, NAT_1, FINSEQ_1, FUNCT_2;
begin
reserve G for strict Group,
a,b,x,y,z for Element of G,
H,K for strict Subgroup of G,
p for Element of NAT,
A for Subset of G;
theorem
for G being strict finite Group holds
p is prime & card G = p implies ex a being Element of G st ord a = p
proof
let G be strict finite Group;
assume that
A1: p is prime and
A2: card G = p;
G is cyclic Group by A1,A2,GR_CY_1:21;
hence thesis by A2,GR_CY_1:19;
end;
theorem
for G being Group, H being Subgroup of G, a1,a2 being Element of H
for b1,b2 being Element of G st a1 = b1 & a2 = b2 holds a1*a2 = b1*b2
proof
let G be Group, H be Subgroup of G;
let a1,a2 be Element of H;
A1: the carrier of H c= the carrier of G by GROUP_2:def 5;
let b1,b2 be Element of G such that
A2: a1 = b1 and
A3: a2 = b2;
dom the multF of G = [:the carrier of G, the carrier of G:] by FUNCT_2:def 1;
then
A4: the
multF of G is ManySortedSet of [:the carrier of G, the carrier of G :]
by PARTFUN1:def 2;
the multF of H = (the multF of G)||the carrier of H by GROUP_2:def 5;
hence thesis by A1,A2,A3,A4,ALTCAT_1:5;
end;
theorem
for G being Group, H being Subgroup of G, a being Element of H
for b being Element of G st a = b for n being Element of NAT
holds a|^n = b|^n by GROUP_4:1;
theorem
for G being Group, H being Subgroup of G, a being Element of H
for b being Element of G st a = b for i being Integer
holds a|^i = b|^i by GROUP_4:2;
theorem
for G being Group, H being Subgroup of G, a being Element of H
for b being Element of G st a = b & G is finite holds ord a = ord b
proof
let G be Group, H be Subgroup of G;
let a be Element of H;
let b be Element of G such that
A1: a =b and
A2: G is finite;
A3: not a is being_of_order_0 by A2,GR_CY_1:6;
A4: not b is being_of_order_0 by A2,GR_CY_1:6;
A5: a |^ (ord a) = 1_H by A3,GROUP_1:def 11;
A6: b |^ ord b = 1_G by A4,GROUP_1:def 11;
a |^ (ord a) = b |^ (ord a) by A1,GROUP_4:1;
then
A7: ord b divides ord a by A5,A6,GROUP_1:44,GROUP_2:44;
a |^ (ord b) = 1_G by A1,A6,GROUP_4:1;
then a |^ (ord b) = 1_H by GROUP_2:44;
then ord a divides ord b by GROUP_1:44;
hence thesis by A7,NAT_D:5;
end;
theorem
for G being Group, H being Subgroup of G, h being Element of G st
h in H holds H * h c= the carrier of H
proof
let G be Group, H be Subgroup of G;
let h be Element of G such that
A1: h in H;
let a be object;
assume a in H * h;
then consider g being Element of G such that
A2: a = g * h and
A3: g in H by GROUP_2:104;
g * h in H by A1,A3,GROUP_2:50;
hence thesis by A2;
end;
theorem Th7:
for G being Group for a being Element of G st a <> 1_G holds gr {a} <> (1).G
proof
let G be Group;
let a be Element of G such that
A1: a <> 1_G;
assume
A2: gr {a} = (1).G;
A3: the carrier of (1).G = {1_G} by GROUP_2:def 7;
A4: {a} c= the carrier of gr {a} by GROUP_4:def 4;
for xx being set holds xx = a implies xx = 1_G
proof
let xx be set;
assume xx = a;
then xx in {a} by TARSKI:def 1;
hence thesis by A2,A3,A4,TARSKI:def 1;
end;
hence thesis by A1;
end;
theorem
for G being Group, m being Integer holds (1_G) |^ m = 1_G by GROUP_1:31;
theorem Th9:
for m being Integer holds a |^ (m * ord a) = 1_G
proof
let m be Integer;
per cases;
suppose a is being_of_order_0;
then ord a = 0 by GROUP_1:def 11;
hence thesis by GROUP_1:25;
end;
suppose a is not being_of_order_0;
then
A1: a |^ ord a = 1_G by GROUP_1:def 11;
(1_G) |^ m = 1_G by GROUP_1:31;
hence thesis by A1,GROUP_1:35;
end;
end;
theorem Th10:
for a st a is not being_of_order_0
for m being Integer holds a |^ m = a |^(m mod ord a)
proof
let a such that
A1: a is not being_of_order_0;
let m be Integer;
ord a <> 0 by A1,GROUP_1:def 11;
then m mod ord a = m - (m div ord a) * ord a by INT_1:def 10;
then a |^(m mod ord a) = a |^ (m + - 1 * (m div ord a) * ord a)
.= (a|^m) * a |^((-(m div ord a)) * ord a) by GROUP_1:33
.= (a|^m) * 1_G by Th9
.= (a|^m) by GROUP_1:def 4;
hence thesis;
end;
theorem Th11:
b is not being_of_order_0 implies gr {b} is finite
proof
assume
A1: b is not being_of_order_0;
then
A2: ord b <> 0 by GROUP_1:def 11;
deffunc B(Nat) = b |^ $1;
consider f being FinSequence such that
A3: len f = ord b & for i being Nat st i in dom f holds
f.i = B(i) from FINSEQ_1:sch 2;
A4: dom f = Seg ord b by A3,FINSEQ_1:def 3;
the carrier of gr {b} c= rng f
proof
let x be object;
assume x in the carrier of gr {b};
then
A5: x in gr {b};
then x in G by GROUP_2:40;
then reconsider a = x as Element of G;
consider m being Integer such that
A6: a = b|^m by A5,GR_CY_1:5;
set k = m mod ord b;
reconsider k as Element of NAT by INT_1:3;
A7: a = b|^k by A1,A6,Th10;
per cases;
suppose
A8: k = 0;
ord b >= 0+1 by A2,NAT_1:13;
then
A9: ord b in Seg ord b by FINSEQ_1:1;
a = 1_G by A7,A8,GROUP_1:25
.= b |^ ord b by A1,GROUP_1:def 11
.= f.ord b by A3,A4,A9;
hence thesis by A4,A9,FUNCT_1:def 3;
end;
suppose
A10: k <> 0;
A11: k < ord b by A2,NEWTON:65;
k >= 0+1 by A10,NAT_1:13;
then
A12: k in Seg ord b by A11,FINSEQ_1:1;
then a = f.k by A3,A4,A7;
hence thesis by A4,A12,FUNCT_1:def 3;
end;
end;
hence the carrier of gr {b} is finite;
end;
theorem Th12:
b is being_of_order_0 implies b" is being_of_order_0
proof
assume
A1: b is being_of_order_0;
for n being Nat st b" |^ n = 1_G holds n = 0
proof
let n be Nat;
assume b" |^ n = 1_G;
then (b |^n)" = 1_G by GROUP_1:37;
then (b |^n)" = (1_G)" by GROUP_1:8;
then b |^n = 1_G by GROUP_1:9;
hence thesis by A1,GROUP_1:def 10;
end;
hence thesis by GROUP_1:def 10;
end;
theorem Th13:
b is being_of_order_0 iff for n being Integer st b |^n = 1_G holds n = 0
proof
thus b is being_of_order_0 implies for n being Integer st b |^n = 1_G
holds n = 0
proof
assume
A1: b is being_of_order_0;
A2: for m being Nat holds b |^ - m = 1_G implies m = 0
proof
let m be Nat;
assume
A3: b |^ - m = 1_G;
b |^ -m = (b |^ m)" by GROUP_1:36;
then
A4: b" |^ m = 1_G by A3,GROUP_1:37;
b" is being_of_order_0 by A1,Th12;
hence thesis by A4,GROUP_1:def 10;
end;
for n being Integer holds b |^ n = 1_G implies n = 0
proof
let n be Integer;
assume
A5: b |^ n = 1_G;
consider k being Nat such that
A6: n = k or n = - k by INT_1:2;
per cases by A6;
suppose n = k;
hence thesis by A1,A5,GROUP_1:def 10;
end;
suppose
A7: n = -k;
then k = 0 by A2,A5;
hence thesis by A7;
end;
end;
hence thesis;
end;
assume for n being Integer holds b|^n = 1_G implies n = 0;
then for n being Nat holds b |^n = 1_G implies n = 0;
hence thesis by GROUP_1:def 10;
end;
theorem
for G st ex a st a <> 1_G holds (for H holds H = G or H = (1).G) iff
G is cyclic & G is finite & ex p being Element of NAT
st card G = p & p is prime
proof
let G such that
A1: ex a st a <> 1_G;
thus (for H holds H = G or H = (1).G) implies
G is cyclic & G is finite & ex p being Element of NAT
st card G = p & p is prime
proof
assume
A2: for H holds H = G or H = (1).G;
consider b such that
A3: b <> 1_G by A1;
A4: gr {b} = G by A2,A3,Th7;
A5: b is not being_of_order_0
proof
assume
A6: b is being_of_order_0;
then
A7: b|^2 <> 1_G by GROUP_1:def 10;
not b in gr{b|^2}
proof
assume b in gr{b|^2};
then consider j1 being Integer such that
A8: b = (b|^2)|^j1 by GR_CY_1:5;
b = b |^ (2 *j1) by A8,GROUP_1:35;
then b" * (b |^ (2 * j1)) = 1_G by GROUP_1:def 5;
then (b|^ -1) * (b |^(2 * j1)) = 1_G by GROUP_1:32;
then b |^ (-1 + (2 * j1)) = 1_G by GROUP_1:33;
then -1 + (2 * j1) = 0 by A6,Th13;
hence thesis by INT_1:9;
end;
then gr{b|^2} <> G;
hence contradiction by A2,A7,Th7;
end;
then consider n being Element of NAT such that
A9: n = ord b and b is not being_of_order_0;
A10: G is finite by A4,A5,Th11;
then
A11: card G = n by A4,A9,GR_CY_1:7;
n is prime
proof
assume
A12: not n is prime;
ex u,v being Element of NAT st u >1 & v > 1 & n = u * v
proof
A13: not (n>1 & for m being Nat holds
m divides n implies m = 1 or m = n) by A12,INT_2:def 4;
n >= 1 by A10,A11,GROUP_1:45;
then n > 1 by A3,A9,GROUP_1:43,XXREAL_0:1;
then consider m being Nat such that
A14: m <> 1 and
A15: m <> n and
A16: m divides n by A13;
reconsider m as Element of NAT by ORDINAL1:def 12;
consider o being Nat such that
A17: n = m * o by A16,NAT_D:def 3;
reconsider o as Element of NAT by ORDINAL1:def 12;
take u = m;
take v = o;
u <> 0
proof
assume u = 0;
then n = 0 * (n div 0) by A16,NAT_D:3;
hence contradiction by A10,A11;
end;
then
A18: 0 + 1 <= u by INT_1:7;
0 < v by A10,A11,A17;
then
A19: 0 + 1 <= v by INT_1:7;
v <> 1 by A15,A17;
hence thesis by A14,A17,A18,A19,XXREAL_0:1;
end;
then consider u, v being Element of NAT such that
A20: u > 1 and
A21: v > 1 and
A22: n = u *v;
ord (b |^v) = u by A4,A10,A11,A22,GR_CY_2:8;
then
A23: card gr {b |^v } = u by A10,GR_CY_1:7;
A24: u <> n by A20,A21,A22,XCMPLX_1:7;
gr {b |^v } <> (1).G by A20,A23,GROUP_2:69;
hence thesis by A2,A11,A23,A24;
end;
hence thesis by A4,A5,A11,Th11,GR_CY_2:4;
end;
assume that
G is cyclic and
A25: G is finite and
A26: ex p being Element of NAT st card G = p & p is prime;
let H;
reconsider G as finite Group by A25;
reconsider H as Subgroup of G;
card G = card H * index H by GROUP_2:147;
then
A27: card H divides card G by NAT_D:def 3;
per cases by A26,A27,INT_2:def 4;
suppose card H = card G;
hence thesis by GROUP_2:73;
end;
suppose card H = 1;
hence thesis by GROUP_2:70;
end;
end;
theorem Th15:
for G being Group, x,y,z being Element of G for A being Subset of G holds
z in x * A * y iff ex a being Element of G st z = x * a * y & a in A
proof
let G be Group;
let x,y,z be Element of G;
let A be Subset of G;
thus z in x * A * y implies ex a being Element of G st z = x * a * y & a in A
proof
assume z in x * A * y;
then consider b being Element of G such that
A1: z = b * y and
A2: b in x * A by GROUP_2:28;
consider u being Element of G such that
A3: b = x * u and
A4: u in A by A2,GROUP_2:27;
take u;
thus thesis by A1,A3,A4;
end;
given a being Element of G such that
A5: z = x * a * y and
A6: a in A;
ex h being Element of G st z = h * y & h in x * A by A5,A6,GROUP_2:27;
hence thesis by GROUP_2:28;
end;
theorem
for G being Group, A being non empty Subset of G holds
for x being Element of G holds card A = card (x" * A * x)
proof
let G be Group, A be non empty Subset of G;
let x be Element of G;
set B = x" * A * x;
A is non empty & B is non empty proof set a = the Element of A;
x" * a * x in B by Th15;
hence thesis;
end;
then reconsider B as non empty Subset of G;
deffunc F(Element of G) = x"*$1*x;
consider f being Function of A, the carrier of G such that
A1: for a being Element of A holds f.a = F(a) from FUNCT_2:sch 4;
A2: dom f = A by FUNCT_2:def 1;
A3: rng f c= B
proof
let s be object;
assume s in rng f;
then consider a being object such that
A4: a in A and
A5: s = f.a by A2,FUNCT_1:def 3;
reconsider a as Element of A by A4;
s = F(a) by A1,A5;
hence thesis by Th15;
end;
A6: B c= rng f
proof
let s be object;
assume s in B;
then consider a being Element of G such that
A7: s = x" * a * x and
A8: a in A by Th15;
ex x being Element of G st x in dom f & s = f.x
proof
take a;
thus thesis by A1,A7,A8,FUNCT_2:def 1;
end;
hence thesis by FUNCT_1:def 3;
end;
reconsider f as Function of A,B by A2,A3,FUNCT_2:2;
deffunc FF(Element of G) = x*$1*x";
consider g being Function of B, the carrier of G such that
A9: for b being Element of B holds g.b = FF(b) from FUNCT_2:sch 4;
A10: dom g = B by FUNCT_2:def 1;
rng g c= A
proof
let s be object;
assume s in rng g;
then consider a being object such that
A11: a in B and
A12: s = g.a by A10,FUNCT_1:def 3;
reconsider a as Element of B by A11;
A13: s = FF(a) by A9,A12;
consider c being Element of G such that
A14: a = x" * c * x and
A15: c in A by Th15;
s = x * (x" * c) * x * x" by A13,A14,GROUP_1:def 3
.= (x * x") * c * x * x" by GROUP_1:def 3
.= (x * x") * c * (x * x") by GROUP_1:def 3
.= 1_G * c * (x * x") by GROUP_1:def 5
.= 1_G * c * 1_G by GROUP_1:def 5
.= 1_G * c by GROUP_1:def 4
.= c by GROUP_1:def 4;
hence thesis by A15;
end;
then reconsider g as Function of B,A by A10,FUNCT_2:2;
A16: for a,b being Element of A st f.a = f.b holds a = b
proof
let a,b be Element of A such that
A17: f.a = f.b;
A18: x" * a * x in B by Th15;
A19: x" * b * x in B by Th15;
A20: g.(f.a) = g.(x" * a * x) by A1
.= x * (x" * a * x) * x" by A9,A18
.= x * (x" * a) * x * x" by GROUP_1:def 3
.= (x * x") * a * x * x" by GROUP_1:def 3
.= (x * x") * a * (x * x") by GROUP_1:def 3
.= 1_G * a * (x * x") by GROUP_1:def 5
.= a * (x * x") by GROUP_1:def 4
.= a * 1_G by GROUP_1:def 5
.= a by GROUP_1:def 4;
g.(f.b) = g.(x" * b * x) by A1
.= x * (x" * b * x) * x" by A9,A19
.= x * (x" * b) * x * x" by GROUP_1:def 3
.= (x * x") * b * x * x" by GROUP_1:def 3
.= (x * x") * b * (x * x") by GROUP_1:def 3
.= 1_G * b * (x * x") by GROUP_1:def 5
.= b * (x * x") by GROUP_1:def 4
.= b * 1_G by GROUP_1:def 5
.= b by GROUP_1:def 4;
hence thesis by A17,A20;
end;
A,B are_equipotent
proof
take f;
thus thesis by A3,A6,A16,FUNCT_2:def 1,GROUP_6:1,XBOOLE_0:def 10;
end;
hence thesis by CARD_1:5;
end;
definition
let G, H, K;
func Double_Cosets (H, K) -> Subset-Family of G means
A in it iff ex a st A = H * a * K;
existence
proof
defpred P[set] means ex a st $1 = H * a * K;
ex F being Subset-Family of G st for A being Subset of G holds
A in F iff P[A] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Subset-Family of G;
defpred P[set] means ex a st $1 = H * a * K;
assume
A1: for A holds A in F1 iff P[A];
assume
A2: for A holds A in F2 iff P[A];
thus thesis from SUBSET_1:sch 4(A1,A2);
end;
end;
theorem Th17:
z in H * x * K iff ex g,h being Element of G st
z = g * x * h & g in H & h in K
proof
thus z in H * x * K implies ex g,h being Element of G st
z = g * x * h & g in H & h in K
proof
assume z in H * x * K;
then consider g1, g2 being Element of G such that
A1: z = g1 * g2 and
A2: g1 in H * x and
A3: g2 in K by GROUP_2:94;
ex h1 being Element of G st ( g1 = h1 * x)&( h1 in H) by A2,GROUP_2:104;
hence thesis by A1,A3;
end;
given g,h being Element of G such that
A4: z = g * x * h and
A5: g in H and
A6: h in K;
ex g1, g2 being Element of G st z = g1 * g2 & g1 in H * x & g2 in K
by A5,A4,A6,GROUP_2:104;
hence thesis by GROUP_2:94;
end;
theorem
for H, K holds H * x * K = H * y * K or
not ex z st z in H * x * K & z in H * y * K
proof
let H, K;
per cases;
suppose not ex z st z in H * x * K & z in H * y * K;
hence thesis;
end;
suppose ex z st z in H * x * K & z in H * y * K;
then consider z such that
A1: z in H * x * K and
A2: z in H * y * K;
consider h1, k1 being Element of G such that
A3: z = h1 * x * k1 and
A4: h1 in H and
A5: k1 in K by A1,Th17;
consider h2, k2 being Element of G such that
A6: z = h2 * y * k2 and
A7: h2 in H and
A8: k2 in K by A2,Th17;
for a be object st a in H * x * K holds a in H * y * K
proof
let a be object;
assume a in H * x * K;
then consider h,k being Element of G such that
A9: a = h * x * k and
A10: h in H and
A11: k in K by Th17;
ex c,d being Element of G st a = c * y * d & c in H & d in K
proof
h = h * 1_G by GROUP_1:def 4;
then
A12: h * x * k = h * 1_G * x * 1_G * k by GROUP_1:def 4;
1_G = h1" * h1 by GROUP_1:def 5;
then
A13: h * x * k = h * (h1" * h1) * x * (k1 * k1") * k by A12,GROUP_1:def 5
.= h * (h1" * h1) * x * k1 * k1" * k by GROUP_1:def 3
.= h * h1" * h1 * x * k1 * k1" * k by GROUP_1:def 3
.= h * h1" * (h1 * x) * k1 * k1" * k by GROUP_1:def 3
.= h * h1" * (h2 * y * k2) * k1" * k by A3,A6,GROUP_1:def 3
.= h * h1" * (h2 * y) * k2 * k1" * k by GROUP_1:def 3
.= (h * h1") * h2 * y * k2 * k1" * k by GROUP_1:def 3
.= (h * h1" * h2) * y * (k2 * k1") * k by GROUP_1:def 3
.= (h * h1" * h2) * y * (k2 * k1" * k) by GROUP_1:def 3;
take h * h1" * h2;
take k2 * k1" * k;
h1" in H by A4,GROUP_2:51;
then
A14: h * h1" in H by A10,GROUP_2:50;
k1" in K by A5,GROUP_2:51;
then k2 * k1" in K by A8,GROUP_2:50;
hence thesis by A7,A9,A11,A13,A14,GROUP_2:50;
end;
hence thesis by Th17;
end;
then
A15: H * x * K c= H * y * K;
for a be object st a in H * y * K holds a in H * x * K
proof
let a be object;
assume a in H * y * K;
then consider h,k being Element of G such that
A16: a = h * y * k and
A17: h in H and
A18: k in K by Th17;
ex c,d being Element of G st a = c * x * d & c in H & d in K
proof
h = h * 1_G by GROUP_1:def 4;
then
A19: h * y * k = h * 1_G * y * 1_G * k by GROUP_1:def 4;
1_G = h2" * h2 by GROUP_1:def 5;
then
A20: h * y * k = h * (h2" * h2) * y * (k2 * k2") * k by A19,GROUP_1:def 5
.= h * (h2" * h2) * y * k2 * k2" * k by GROUP_1:def 3
.= h * h2" * h2 * y * k2 * k2" * k by GROUP_1:def 3
.= h * h2" * (h2 * y) * k2 * k2" * k by GROUP_1:def 3
.= h * h2" * (h1 * x * k1) * k2" * k by A3,A6,GROUP_1:def 3
.= h * h2" * (h1 * x) * k1 * k2" * k by GROUP_1:def 3
.= (h * h2") * h1 * x * k1 * k2" * k by GROUP_1:def 3
.= (h * h2" * h1) * x * (k1 * k2") * k by GROUP_1:def 3
.= (h * h2" * h1) * x * (k1 * k2" * k) by GROUP_1:def 3;
take h * h2" * h1;
take k1 * k2" * k;
h2" in H by A7,GROUP_2:51;
then
A21: h * h2" in H by A17,GROUP_2:50;
k2" in K by A8,GROUP_2:51;
then k1 * k2" in K by A5,GROUP_2:50;
hence thesis by A4,A16,A18,A20,A21,GROUP_2:50;
end;
hence thesis by Th17;
end;
then H * y * K c= H * x * K;
hence thesis by A15,XBOOLE_0:def 10;
end;
end;
reserve G for Group;
reserve H, B, A for Subgroup of G,
D for Subgroup of A;
registration
let G,A;
cluster Left_Cosets A -> non empty;
coherence;
end;
notation
let G be Group;
let H be Subgroup of G;
synonym index (G,H) for index H;
end;
theorem Th19:
D = A /\ B & G is finite implies index(G,B) >= index(A,D)
proof
assume that
A1: D = A /\ B and
A2: G is finite;
reconsider LCB = Left_Cosets B as finite non empty set by A2;
reconsider LCD = Left_Cosets D as finite non empty set by A2;
A3: now
let x,y be Element of G;
let x9,y9 be Element of A such that
A4: x9 = x and
A5: y9 = y;
A6: y9" = y" by A5,GROUP_2:48;
A7: y9"*x9 in A;
x*B = y*B iff y"*x in B by GROUP_2:114;
then x*B = y*B iff y9"*x9 in B by A4,A6,GROUP_2:43;
then x*B = y*B iff y9"*x9 in D by A1,A7,GROUP_2:82;
hence x*B = y*B iff x9*D = y9*D by GROUP_2:114;
end;
defpred P[set, set] means ex a being Element of G, a9 being Element of A st
a = a9 & $2 = a*B & $1 = a9*D;
A8: for x being Element of LCD ex y being Element of LCB st P[x,y]
proof
let x be Element of LCD;
x in LCD;
then consider a9 being Element of A such that
A9: x = a9*D by GROUP_2:def 15;
reconsider a = a9 as Element of G by GROUP_2:42;
reconsider y = a*B as Element of LCB by GROUP_2:def 15;
take y,a,a9;
thus thesis by A9;
end;
consider F being Function of LCD, LCB such that
A10: for a being Element of LCD holds P[a,F.a] from FUNCT_2:sch 3(A8);
A11: dom F = LCD by FUNCT_2:def 1;
A12: rng F c= LCB by RELAT_1:def 19;
A13: index D = card LCD by GROUP_2:def 18;
A14: index B = card LCB by GROUP_2:def 18;
F is one-to-one
proof
let x1,x2 be object;
assume that
A15: x1 in dom F and
A16: x2 in dom F;
reconsider z1 = x1, z2 = x2 as Element of LCD by A15,A16,FUNCT_2:def 1;
A17: ex a being Element of G, a9 being Element of A st ( a = a9)&
( F.z1 = a*B)&( z1 = a9*D) by A10;
ex b being Element of G, b9 being Element of A st ( b = b9)&
( F.z2 = b*B)&( z2 = b9*D) by A10;
hence thesis by A3,A17;
end;
then Segm index D c= Segm index B by A11,A12,A13,A14,CARD_1:10;
hence thesis by NAT_1:39;
end;
theorem Th20:
for G being finite Group, H be Subgroup of G holds index (G,H) > 0
proof
let G be finite Group, H be Subgroup of G;
card G = card H * index H by GROUP_2:147;
hence thesis;
end;
theorem
for G being Group st G is finite for C being Subgroup of G
for A,B being Subgroup of C
for D being Subgroup of A st D = A /\ B
for E being Subgroup of B st E = A /\ B
for F being Subgroup of C st F = A /\ B holds
index (C,A), index (C,B) are_coprime
implies index (C,B) = index (A,D) & index (C,A) = index (B,E)
proof
let G such that
A1: G is finite;
let C be Subgroup of G;
let A,B be Subgroup of C;
let D be Subgroup of A such that
A2: D = A /\ B;
let E be Subgroup of B such that
A3: E = A /\ B;
let F be Subgroup of C such that
A4: F = A /\ B;
assume that
A5: index A, index B are_coprime;
index F = index E * index B by A1,A3,A4,GROUP_2:149;
then
A6: index E * index B = index D * index A by A1,A2,A4,GROUP_2:149;
then (index B qua Integer) divides
((index A qua Integer) * (index D qua Integer)) by INT_1:def 3;
then
A7: (index B qua Integer) divides (index D qua Integer) by A5,INT_2:25;
ex n being Element of NAT st index D = (index B) * n
proof
consider i being Integer such that
A8: index D = (index B qua Integer) * i by A7,INT_1:def 3;
0 <= i by A1,A8,Th20;
then reconsider i as Element of NAT by INT_1:3;
take i;
thus thesis by A8;
end;
then
A9: index B divides index D by NAT_D:def 3;
A10: index(C,B) >= index(A,D) by A1,A2,Th19;
A11: index B = index D
proof
assume
A12: index B <> index D;
index D > 0 by A1,Th20;
then index B <= index D by A9,NAT_D:7;
hence contradiction by A10,A12,XXREAL_0:1;
end;
(index A qua Integer) divides
((index B qua Integer) * (index E qua Integer)) by A6,INT_1:def 3;
then
A13: (index A qua Integer) divides index E by A5,INT_2:25;
ex n being Element of NAT st index E = (index A) * n
proof
consider i being Integer such that
A14: index E = (index A qua Integer) * i by A13,INT_1:def 3;
0 <= i by A1,A14,Th20;
then reconsider i as Element of NAT by INT_1:3;
take i;
thus thesis by A14;
end;
then
A15: index A divides index E by NAT_D:def 3;
A16: index A >= index E by A1,A3,Th19;
index A = index E
proof
assume
A17: index A <> index E;
index E > 0 by A1,Th20;
then index A <= index E by A15,NAT_D:7;
hence contradiction by A16,A17,XXREAL_0:1;
end;
hence thesis by A11;
end;
theorem Th22:
for a being Element of G st a in H holds
for j being Integer holds a |^ j in H
proof
let a be Element of G;
assume
A1: a in H;
let j be Integer;
consider k being Nat such that
A2: j = k or j = - k by INT_1:2;
per cases by A2;
suppose
A3: j =k;
defpred P[Nat] means a |^ $1 in H;
a |^0 = 1_G by GROUP_1:25;
then
A4: P[ 0 ] by GROUP_2:46;
A5: for n being Nat st P[n] holds P[n + 1]
proof
let n be Nat;
assume P[n];
then (a |^ n) * a in H by A1,GROUP_2:50;
hence thesis by GROUP_1:34;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A5);
hence thesis by A3;
end;
suppose
A6: j = - k;
defpred PP[Nat] means a |^ (- $1) in H;
a |^0 = 1_G by GROUP_1:25;
then
A7: PP[ 0 ] by GROUP_2:46;
A8: for n being Nat st PP[n] holds PP[n +1 ]
proof
let n be Nat such that
A9: PP[n];
a" in H by A1,GROUP_2:51;
then a |^(-n) * a" in H by A9,GROUP_2:50;
then a |^(-n) * a |^ (-1) in H by GROUP_1:32;
then a |^(- n + (- 1)) in H by GROUP_1:33;
hence thesis;
end;
for n being Nat holds PP[n] from NAT_1:sch 2(A7,A8);
hence thesis by A6;
end;
end;
theorem Th23:
for G being strict Group st G <> (1).G ex b being Element of G st b <> 1_G
proof
let G be strict Group such that
A1: G <> (1).G;
assume
A2: not ex b being Element of G st b <> 1_G;
for x,y being Element of G holds x = y
proof
let x,y be Element of G;
x = 1_G by A2;
hence thesis by A2;
end;
then G is trivial;
hence contradiction by A1,GROUP_6:12;
end;
theorem Th24:
for G being strict Group for a being Element of G st G = gr{a}
for H being strict Subgroup of G st H <> (1).G holds
ex k being Nat st 0 < k & a |^k in H
proof
let G be strict Group;
let a be Element of G such that
A1: G = gr{a};
let H be strict Subgroup of G;
assume H <> (1).G;
then
A2: H <> (1).H by GROUP_2:63;
consider c being Element of H such that
A3: c <> 1_H by A2,Th23;
A4: c in H;
then c in G by GROUP_2:40;
then reconsider c as Element of G;
A5: c in gr{a} by A1;
ex j being Integer st c = a |^j & j <> 0
proof
assume
A6: not ex j being Integer st c = a |^j & j <> 0;
consider i being Integer such that
A7: c = a |^ i by A5,GR_CY_1:5;
A8: a |^i <> 1_G by A3,A7,GROUP_2:44;
i = 0 by A6,A7;
hence contradiction by A8,GROUP_1:25;
end;
then consider j being Integer such that
A9: c = a |^ j and
A10: j <> 0;
consider n being Nat such that
A11: j = n or j = -n by INT_1:2;
per cases by A11;
suppose
j = n;
hence thesis by A4,A9,A10;
end;
suppose
A12: j = - n;
then
A13: 0 < n by A10;
(a |^ n)" in H by A4,A9,A12,GROUP_1:36;
then (a |^ n)"" in H by GROUP_2:51;
hence thesis by A13;
end;
end;
theorem
for G being strict cyclic Group for H being strict Subgroup of G holds
H is cyclic Group
proof
let G be strict cyclic Group;
let H be strict Subgroup of G;
per cases;
suppose H = (1).G;
hence thesis;
end;
suppose
A1: H <> (1).G;
consider b being Element of G such that
A2: the multMagma of G = gr{b} by GR_CY_1:def 7;
ex m being Nat st 0 < m & b |^m in H & for j being Nat st
0 < j & b |^j in H holds m <= j
proof
defpred P[Nat] means 0 < $1 & b |^$1 in H;
ex k being Nat st P[k] by A1,A2,Th24;
then
A3: ex k being Nat st P[k];
ex m being Nat st P[m] & for j being Nat st P[j]
holds m <= j from NAT_1:sch 5(A3);
hence thesis;
end;
then consider m being Nat such that
A4: 0 < m and
A5: b |^m in H and
A6: for j being Nat st 0 < j & b |^ j in H holds m <= j;
set c = b |^ m;
reconsider c as Element of H by A5;
for a being Element of H holds ex i being Integer st a = c |^ i
proof
let a be Element of H;
ex t being Integer st b |^t in H & b|^t = a
proof
A7: a in G by GROUP_2:41;
A8: a in gr{b} by A2,GROUP_2:41;
a is Element of G by A7;
then consider j1 being Integer such that
A9: a = b |^ j1 by A8,GR_CY_1:5;
b |^ j1 in H by A9;
hence thesis by A9;
end;
then consider t being Integer such that
A10: b |^ t in H and
A11: b |^t = a;
ex r,s being Integer st 0 <= s & s < m & t = m * r + s
proof
take t div m;
take t mod m;
thus thesis by A4,NEWTON:65,66;
end;
then consider r,s being Integer such that
A12: 0 <= s and
A13: s < m and
A14: t = m * r + s;
reconsider s as Element of NAT by A12,INT_1:3;
A15: b |^ t = b |^(m *r) * (b |^s) by A14,GROUP_1:33
.= ((b |^m)|^ r) * (b |^ s) by GROUP_1:35;
A16: (b |^m) |^r in H by A5,Th22;
b |^s in H
proof
set u = b |^t;
set v = (b |^m) |^ r;
A17: v" * u = (v" * v) * b|^s by A15,GROUP_1:def 3
.= 1_G * b |^ s by GROUP_1:def 5
.= b |^ s by GROUP_1:def 4;
v" in H by A16,GROUP_2:51;
hence thesis by A10,A17,GROUP_2:50;
end;
then s = 0 by A6,A13;
then b |^ s = 1_G by GROUP_1:25;
then
A18: b |^ t = (b |^ m) |^r by A15,GROUP_1:def 4;
(b |^m)|^ r = (c) |^ r by GROUP_4:2;
hence thesis by A11,A18;
end;
then H = gr{c} by GR_CY_2:5;
hence thesis by GR_CY_2:4;
end;
end;