:: Classes of Conjugation. Normal Subgroups
:: by Wojciech A. Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990-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_1, SUBSET_1, GROUP_2, NAT_1, INT_1, RELAT_1, BINOP_1,
ALGSTR_0, FUNCT_1, STRUCT_0, TARSKI, ZFMISC_1, XBOOLE_0, FINSET_1,
CARD_1, NEWTON, ARYTM_3, XXREAL_0, COMPLEX1, RLSUB_1, CQC_SIM1, SETFAM_1,
PRE_TOPC, GROUP_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, BINOP_1,
RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, CARD_1, STRUCT_0, ALGSTR_0, GROUP_1,
GROUP_2, DOMAIN_1, XXREAL_0, INT_1, INT_2;
constructors SETFAM_1, WELLORD2, BINOP_1, XXREAL_0, NAT_1, INT_2, REALSET1,
REAL_1, GROUP_2, RELSET_1, BINOP_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, XREAL_0, INT_1,
STRUCT_0, GROUP_1, GROUP_2, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE;
definitions XBOOLE_0, BINOP_1, FUNCT_1, GROUP_2, TARSKI, GROUP_1;
equalities BINOP_1, GROUP_2, TARSKI, ALGSTR_0, STRUCT_0;
expansions XBOOLE_0, BINOP_1, GROUP_1, STRUCT_0;
theorems ABSVALUE, CARD_1, CARD_2, ENUMSET1, FINSET_1, FUNCT_1, FUNCT_2,
GROUP_1, GROUP_2, TARSKI, WELLORD2, ZFMISC_1, RELAT_1, XBOOLE_0,
XBOOLE_1, STRUCT_0, XTUPLE_0;
schemes FUNCT_1, FUNCT_2, NAT_1, SUBSET_1, XBOOLE_0, CLASSES1, XFAMILY;
begin
reserve x,y,y1,y2 for set;
reserve G for Group;
reserve a,b,c,d,g,h for Element of G;
reserve A,B,C,D for Subset of G;
reserve H,H1,H2,H3 for Subgroup of G;
reserve n for Nat;
reserve i for Integer;
theorem Th1:
a * b * b" = a & a * b" * b = a & b" * b * a = a & b * b" * a = a
& a * (b * b") = a & a * (b" * b) = a & b" * (b * a) = a & b * (b" * a) = a
proof
thus
A1: a * b * b" = a * (b * b") by GROUP_1:def 3
.= a * 1_G by GROUP_1:def 5
.= a by GROUP_1:def 4;
thus
A2: a * b" * b = a * (b" * b) by GROUP_1:def 3
.= a * 1_G by GROUP_1:def 5
.= a by GROUP_1:def 4;
thus
A3: b" * b * a = 1_G * a by GROUP_1:def 5
.= a by GROUP_1:def 4;
thus b * b" * a = 1_G * a by GROUP_1:def 5
.= a by GROUP_1:def 4;
hence thesis by A1,A2,A3,GROUP_1:def 3;
end;
Lm1: for A be commutative Group, a, b be Element of A holds a * b = b * a;
theorem
G is commutative Group iff the multF of G is commutative
proof
thus G is commutative Group implies the multF of G is commutative
proof
assume
A1: G is commutative Group;
let a,b;
thus (the multF of G).(a,b) = a * b .= b * a by A1,Lm1
.= (the multF of G).(b,a);
end;
assume
A2: the multF of G is commutative;
G is commutative
by A2;
hence thesis;
end;
theorem
(1).G is commutative
proof
let a,b be Element of (1).G;
a in the carrier of (1).G;
then a in {1_G} by GROUP_2:def 7;
then
A1: a = 1_G by TARSKI:def 1;
b in the carrier of (1).G;
then b in {1_G} by GROUP_2:def 7;
hence thesis by A1,TARSKI:def 1;
end;
theorem Th4:
A c= B & C c= D implies A * C c= B * D
proof
assume
A1: A c= B & C c= D;
let x be object;
assume x in A * C;
then ex a,c st x = a * c & a in A & c in C;
hence thesis by A1;
end;
theorem
A c= B implies a * A c= a * B & A * a c= B * a by Th4;
theorem Th6:
H1 is Subgroup of H2 implies a * H1 c= a * H2 & H1 * a c= H2 * a
proof
assume H1 is Subgroup of H2;
then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
hence thesis by Th4;
end;
theorem
a * H = {a} * H;
theorem
H * a = H * {a};
theorem Th9:
A * a * H = A * (a * H)
proof
thus A * a * H = A * ({a} * H) by GROUP_2:96
.= A * (a * H);
end;
theorem
a * H * A = a * (H * A)
proof
thus a * H * A = {a} * H * A .= a * (H * A) by GROUP_2:97;
end;
theorem
A * H * a = A * (H * a)
proof
thus A * H * a = A * (H * {a}) by GROUP_2:97
.= A * (H * a);
end;
theorem
H * a * A = H * (a * A)
proof
thus H * a * A = H * {a} * A .= H * (a * A) by GROUP_2:98;
end;
theorem
H1 * a * H2 = H1 * (a * H2) by Th9;
definition
let G;
func Subgroups G -> set means :Def1:
for x being object holds x in it iff x is strict Subgroup of G;
existence
proof
defpred P[object,object] means
ex H being strict Subgroup of G st $2 = H & $1 = the carrier of H;
defpred P[set] means ex H being strict Subgroup of G st $1 = the carrier
of H;
consider B being set such that
A1: for x holds x in B iff x in bool the carrier of G & P[x] from
XFAMILY:sch 1;
A2: for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2 by GROUP_2:59;
consider f being Function such that
A3: for x,y being object holds [x,y] in f iff x in B & P[x,y]
from FUNCT_1:sch 1(A2);
for x being object holds x in B iff ex y being object st [x,y] in f
proof
let x be object;
thus x in B implies ex y being object st [x,y] in f
proof
assume
A4: x in B;
then consider H being strict Subgroup of G such that
A5: x = the carrier of H by A1;
take H;
thus thesis by A3,A4,A5;
end;
thus thesis by A3;
end;
then
A6: B = dom f by XTUPLE_0:def 12;
for y being object holds y in rng f iff y is strict Subgroup of G
proof
let y be object;
thus y in rng f implies y is strict Subgroup of G
proof
assume y in rng f;
then consider x being object such that
A7: x in dom f & y = f.x by FUNCT_1:def 3;
[x,y] in f by A7,FUNCT_1:def 2;
then ex H being strict Subgroup of G st y = H & x = the carrier of H
by A3;
hence thesis;
end;
assume y is strict Subgroup of G;
then reconsider H = y as strict Subgroup of G;
A8: y is set by TARSKI:1;
reconsider x = the carrier of H as set;
the carrier of H c= the carrier of G by GROUP_2:def 5;
then
A9: x in dom f by A1,A6;
then [x,y] in f by A3,A6;
then y = f.x by A9,FUNCT_1:def 2,A8;
hence thesis by A9,FUNCT_1:def 3;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means $1 is strict Subgroup of G;
let A1,A2 be set;
assume
A10: for x being object holds x in A1 iff P[x];
assume
A11: for x being object holds x in A2 iff P[x];
thus thesis from XBOOLE_0:sch 2(A10,A11);
end;
end;
registration
let G;
cluster Subgroups G -> non empty;
coherence
proof
set x = the strict Subgroup of G;
x in Subgroups G by Def1;
hence thesis;
end;
end;
theorem
for G being strict Group holds G in Subgroups G
proof
let G be strict Group;
G is Subgroup of G by GROUP_2:54;
hence thesis by Def1;
end;
theorem Th15:
G is finite implies Subgroups G is finite
proof
defpred P[object,object] means
ex H being strict Subgroup of G st
$1 = H & $2 = the carrier of H;
assume
A1: G is finite;
A2: for x being object st x in Subgroups G ex y being object st P[x,y]
proof
let x be object;
assume x in Subgroups G;
then reconsider F = x as strict Subgroup of G by Def1;
reconsider y = the carrier of F as set;
take y;
take F;
thus thesis;
end;
consider f being Function such that
A3: dom f = Subgroups G and
A4: for x being object st x in Subgroups G holds P[x,f.x]
from CLASSES1:sch 1(A2);
A5: rng f c= bool the carrier of G
proof
let x be object;
assume x in rng f;
then consider y being object such that
A6: y in dom f & f.y = x by FUNCT_1:def 3;
consider H being strict Subgroup of G such that
y = H and
A7: x = the carrier of H by A3,A4,A6;
the carrier of H c= the carrier of G by GROUP_2:def 5;
hence thesis by A7;
end;
f is one-to-one
proof
let x,y be object;
assume that
A8: x in dom f & y in dom f and
A9: f.x = f.y;
( ex H1 being strict Subgroup of G st x = H1 & f.x = the carrier of
H1)& ex H2 being strict Subgroup of G st y = H2 & f.y = the carrier of H2 by A3
,A4,A8;
hence thesis by A9,GROUP_2:59;
end;
then card Subgroups G c= card bool the carrier of G by A3,A5,CARD_1:10;
hence thesis by A1,CARD_2:49;
end;
definition
let G,a,b;
func a |^ b -> Element of G equals
b" * a * b;
correctness;
end;
theorem Th16:
a |^ g = b |^ g implies a = b
proof
assume a |^ g = b |^ g;
then g" * a = g" * b by GROUP_1:6;
hence thesis by GROUP_1:6;
end;
theorem Th17:
(1_G) |^ a = 1_G
proof
thus (1_G) |^ a = a" * a by GROUP_1:def 4
.= 1_G by GROUP_1:def 5;
end;
theorem Th18:
a |^ b = 1_G implies a = 1_G
proof
assume a |^ b = 1_G;
then b" = b" * a by GROUP_1:12;
hence thesis by GROUP_1:7;
end;
theorem Th19:
a |^ 1_G = a
proof
thus a |^ 1_G = (1_G)" * a by GROUP_1:def 4
.= 1_G * a by GROUP_1:8
.= a by GROUP_1:def 4;
end;
theorem Th20:
a |^ a = a
proof
thus a |^ a = 1_G * a by GROUP_1:def 5
.= a by GROUP_1:def 4;
end;
theorem
a |^ a" = a & a" |^ a = a" by Th1;
theorem Th22:
a |^ b = a iff a * b = b * a
proof
thus a |^ b = a implies a * b = b * a
proof
assume a |^ b = a;
then a = b" * (a * b) by GROUP_1:def 3;
hence thesis by GROUP_1:13;
end;
assume a * b = b * a;
then a = b" * (a * b) by GROUP_1:13;
hence thesis by GROUP_1:def 3;
end;
theorem Th23:
(a * b) |^ g = a |^ g * (b |^ g)
proof
thus (a * b) |^ g = g" * (a * 1_G * b) * g by GROUP_1:def 4
.= g" * (a * (g * g") * b) * g by GROUP_1:def 5
.= g" * (a * g * g" * b) * g by GROUP_1:def 3
.= g" * (a * g * (g" * b)) * g by GROUP_1:def 3
.= g" * (a * g) * (g" * b) * g by GROUP_1:def 3
.= a |^ g * (g" * b) * g by GROUP_1:def 3
.= a |^ g * (b |^ g) by GROUP_1:def 3;
end;
theorem Th24:
a |^ g |^ h = a |^ (g * h)
proof
thus a |^ g |^ h = h" * (g" * a) * g * h by GROUP_1:def 3
.= h" * g" * a * g * h by GROUP_1:def 3
.= (g * h)" * a * g * h by GROUP_1:17
.= a |^ (g * h) by GROUP_1:def 3;
end;
theorem Th25:
a |^ b |^ b" = a & a |^ b" |^ b = a
proof
thus a |^ b |^ b" = a |^ (b * b") by Th24
.= a |^ 1_G by GROUP_1:def 5
.= a by Th19;
thus a |^ b" |^ b = a |^ (b" * b) by Th24
.= a |^ 1_G by GROUP_1:def 5
.= a by Th19;
end;
theorem Th26:
a" |^ b = (a |^ b)"
proof
thus a" |^ b = (a * b)" * b by GROUP_1:17
.= (a * b)" * b""
.= (b" * (a * b))" by GROUP_1:17
.= (a |^ b)" by GROUP_1:def 3;
end;
Lm2: now
let G,a,b;
thus a |^ 0 |^ b = (1_G) |^ b by GROUP_1:25
.= 1_G by Th17
.= (a |^ b) |^ 0 by GROUP_1:25;
end;
Lm3: now
let n;
assume
A1: for G,a,b holds a |^ n |^ b = (a |^ b) |^ n;
let G,a,b;
thus a |^ (n + 1) |^ b = (a |^ n * a) |^ b by GROUP_1:34
.= (a |^ n |^ b) * (a |^ b) by Th23
.= ((a |^ b) |^ n) * (a |^ b) by A1
.= (a |^ b) |^ (n + 1) by GROUP_1:34;
end;
Lm4: for n,G,a,b holds a |^ n |^ b = (a |^ b) |^ n
proof
defpred P[Nat] means a |^ $1 |^ b = (a |^ b) |^ $1;
A1: for k be Nat st P[k] holds P[k+1] by Lm3;
A2: P[0] by Lm2;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem
(a |^ n) |^ b = (a |^ b) |^ n by Lm4;
theorem
(a |^ i) |^ b = (a |^ b) |^ i
proof
per cases;
suppose
i >= 0;
then i = |.i.| by ABSVALUE:def 1;
hence thesis by Lm4;
end;
suppose
A1: i < 0;
hence a |^ i |^ b = (a |^ |.i.|)" |^ b by GROUP_1:30
.= (a |^ |.i.| |^ b)" by Th26
.= ((a |^ b) |^ |.i.|)" by Lm4
.= (a |^ b) |^ i by A1,GROUP_1:30;
end;
end;
theorem Th29:
G is commutative Group implies a |^ b = a
proof
assume G is commutative Group;
hence a |^ b = a * b" * b by Lm1
.= a by Th1;
end;
theorem Th30:
(for a,b holds a |^ b = a) implies G is commutative
proof
assume
A1: for a,b holds a |^ b = a;
let a,b;
a |^ b = a by A1;
hence thesis by Th22;
end;
definition
let G,A,B;
func A |^ B -> Subset of G equals
{g |^ h : g in A & h in B};
coherence
proof
set X = {g |^ h : g in A & h in B};
X c= the carrier of G
proof
let x be object;
assume x in X;
then ex g,h st x = g |^ h & g in A & h in B;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th31:
x in A |^ B iff ex g,h st x = g |^ h & g in A & h in B;
theorem Th32:
A |^ B <> {} iff A <> {} & B <> {}
proof
set x = the Element of A;
set y = the Element of B;
thus A |^ B <> {} implies A <> {} & B <> {}
proof
set x = the Element of A |^ B;
assume A |^ B <> {};
then ex a,b st x = a |^ b & a in A & b in B by Th31;
hence thesis;
end;
assume
A1: A <> {};
assume
A2: B <> {};
then reconsider x,y as Element of G by A1,TARSKI:def 3;
x |^ y in A |^ B by A1,A2;
hence thesis;
end;
theorem Th33:
A |^ B c= B" * A * B
proof
let x be object;
assume x in A |^ B;
then consider a,b such that
A1: x = a |^ b and
A2: a in A and
A3: b in B;
b" in B" by A3;
then b" * a in B" * A by A2;
hence thesis by A1,A3;
end;
theorem Th34:
(A * B) |^ C c= A |^ C * (B |^ C)
proof
let x be object;
assume x in (A * B) |^ C;
then consider a,b such that
A1: x = a |^ b and
A2: a in A * B and
A3: b in C;
consider g,h such that
A4: a = g * h & g in A and
A5: h in B by A2;
A6: h |^ b in B |^ C by A3,A5;
x = (g |^ b) * (h |^ b) & g |^ b in A |^ C by A1,A3,A4,Th23;
hence thesis by A6;
end;
theorem Th35:
A |^ B |^ C = A |^ (B * C)
proof
thus A |^ B |^ C c= A |^ (B * C)
proof
let x be object;
assume x in A |^ B |^ C;
then consider a,c such that
A1: x = a |^ c and
A2: a in A |^ B and
A3: c in C;
consider g,h such that
A4: a = g |^ h and
A5: g in A and
A6: h in B by A2;
x = g |^ (h * c) & h * c in B * C by A1,A3,A4,A6,Th24;
hence thesis by A5;
end;
let x be object;
assume x in A |^ (B * C);
then consider a,b such that
A7: x = a |^ b & a in A and
A8: b in B * C;
consider g,h such that
A9: b = g * h & g in B and
A10: h in C by A8;
a |^ g in A |^ B & x = a |^ g |^ h by A7,A9,Th24;
hence thesis by A10;
end;
theorem
A" |^ B = (A |^ B)"
proof
thus A" |^ B c= (A |^ B)"
proof
let x be object;
assume x in A" |^ B;
then consider a,b such that
A1: x = a |^ b and
A2: a in A" and
A3: b in B;
consider c such that
A4: a = c" & c in A by A2;
x = (c |^ b)" & c |^ b in A |^ B by A1,A3,A4,Th26;
hence thesis;
end;
let x be object;
assume x in (A |^ B)";
then consider a such that
A5: x = a" and
A6: a in A |^ B;
consider b,c such that
A7: a = b |^ c and
A8: b in A and
A9: c in B by A6;
A10: b" in A" by A8;
x = b" |^ c by A5,A7,Th26;
hence thesis by A9,A10;
end;
theorem Th37:
{a} |^ {b} = {a |^ b}
proof
A1: {b}" * {a} * {b} = {b"} * {a} * {b} by GROUP_2:3
.= {b" * a} * {b} by GROUP_2:18
.= {a |^ b} by GROUP_2:18;
{a} |^ {b} c= {b}" * {a} * {b} & {a} |^ {b} <> {} by Th32,Th33;
hence thesis by A1,ZFMISC_1:33;
end;
theorem
{a} |^ {b,c} = {a |^ b,a |^ c}
proof
thus {a} |^ {b,c} c= {a |^ b,a |^ c}
proof
let x be object;
assume x in {a} |^ {b,c};
then consider g,h such that
A1: x = g |^ h and
A2: g in {a} and
A3: h in{b,c};
A4: h = b or h = c by A3,TARSKI:def 2;
g = a by A2,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let x be object;
A5: c in {b,c} by TARSKI:def 2;
assume x in {a |^ b,a |^ c};
then
A6: x = a |^ b or x = a |^ c by TARSKI:def 2;
a in {a} & b in {b,c} by TARSKI:def 1,def 2;
hence thesis by A6,A5;
end;
theorem
{a,b} |^ {c} = {a |^ c,b |^ c}
proof
thus {a,b} |^ {c} c= {a |^ c,b |^ c}
proof
let x be object;
assume x in {a,b} |^ {c};
then consider g,h such that
A1: x = g |^ h and
A2: g in {a,b} and
A3: h in {c};
A4: g = b or g = a by A2,TARSKI:def 2;
h = c by A3,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let x be object;
A5: c in {c} by TARSKI:def 1;
assume x in {a |^ c,b |^ c};
then
A6: x = a |^ c or x = b |^ c by TARSKI:def 2;
a in {a,b} & b in {a,b} by TARSKI:def 2;
hence thesis by A6,A5;
end;
theorem
{a,b} |^ {c,d} = {a |^ c,a |^ d,b |^ c,b |^ d}
proof
thus {a,b} |^ {c,d} c= {a |^ c,a |^ d,b |^ c,b |^ d}
proof
let x be object;
assume x in {a,b} |^ {c,d};
then consider g,h such that
A1: x = g |^ h and
A2: g in {a,b} and
A3: h in {c,d};
A4: h = c or h = d by A3,TARSKI:def 2;
g = a or g = b by A2,TARSKI:def 2;
hence thesis by A1,A4,ENUMSET1:def 2;
end;
let x be object;
A5: c in {c,d} & d in {c,d} by TARSKI:def 2;
assume x in {a |^ c,a |^ d,b |^ c,b |^ d};
then
A6: x = a |^ c or x = a |^ d or x = b |^ c or x = b |^ d by ENUMSET1:def 2;
a in {a,b} & b in {a,b} by TARSKI:def 2;
hence thesis by A6,A5;
end;
definition
let G,A,g;
func A |^ g -> Subset of G equals
A |^ {g};
correctness;
func g |^ A -> Subset of G equals
{g} |^ A;
correctness;
end;
theorem Th41:
x in A |^ g iff ex h st x = h |^ g & h in A
proof
thus x in A |^ g implies ex h st x = h |^ g & h in A
proof
assume x in A |^ g;
then consider a,b such that
A1: x = a |^ b & a in A and
A2: b in {g};
b = g by A2,TARSKI:def 1;
hence thesis by A1;
end;
given h such that
A3: x = h |^ g & h in A;
g in {g} by TARSKI:def 1;
hence thesis by A3;
end;
theorem Th42:
x in g |^ A iff ex h st x = g |^ h & h in A
proof
thus x in g |^ A implies ex h st x = g |^ h & h in A
proof
assume x in g |^ A;
then consider a,b such that
A1: x = a |^ b and
A2: a in {g} and
A3: b in A;
a = g by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
given h such that
A4: x = g |^ h & h in A;
g in {g} by TARSKI:def 1;
hence thesis by A4;
end;
theorem
g |^ A c= A" * g * A
proof
let x be object;
assume x in g |^ A;
then consider a such that
A1: x = g |^ a and
A2: a in A by Th42;
a" in A" by A2;
then a" * g in A" * g by GROUP_2:28;
hence thesis by A1,A2;
end;
theorem
A |^ B |^ g = A |^ (B * g) by Th35;
theorem
A |^ g |^ B = A |^ (g * B) by Th35;
theorem
g |^ A |^ B = g |^ (A * B) by Th35;
theorem Th47:
A |^ a |^ b = A |^ (a * b)
proof
thus A |^ a |^ b = A |^ (a * {b}) by Th35
.= A |^ (a * b) by GROUP_2:18;
end;
theorem
a |^ A |^ b = a |^ (A * b) by Th35;
theorem
a |^ b |^ A = a |^ (b * A)
proof
thus a |^ b |^ A = {a} |^ {b} |^ A by Th37
.= a |^ (b * A) by Th35;
end;
theorem Th50:
A |^ g = g" * A * g
proof
A |^ g c= {g}" * A * {g} by Th33;
hence A |^ g c= g" * A * g by GROUP_2:3;
let x be object;
assume x in g" * A * g;
then consider a such that
A1: x = a * g and
A2: a in g" * A by GROUP_2:28;
consider b such that
A3: a = g" * b and
A4: b in A by A2,GROUP_2:27;
x = b |^ g by A1,A3;
hence thesis by A4,Th41;
end;
theorem
(A * B) |^ a c= (A |^ a) * (B |^ a) by Th34;
theorem Th52:
A |^ 1_G = A
proof
thus A |^ 1_G = (1_G)" * A * 1_G by Th50
.= (1_G)" * A by GROUP_2:37
.= 1_G * A by GROUP_1:8
.= A by GROUP_2:37;
end;
theorem
A <> {} implies (1_G) |^ A = {1_G}
proof
set y = the Element of A;
assume
A1: A <> {};
then reconsider y as Element of G by TARSKI:def 3;
thus (1_G) |^ A c= {1_G}
proof
let x be object;
assume x in (1_G) |^ A;
then ex a st x = (1_G) |^ a & a in A by Th42;
then x = 1_G by Th17;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {1_G};
then x = 1_G by TARSKI:def 1;
then (1_G) |^ y = x by Th17;
hence thesis by A1,Th42;
end;
theorem Th54:
A |^ a |^ a" = A & A |^ a" |^ a = A
proof
thus A |^ a |^ a" = A |^ (a * a") by Th47
.= A |^ 1_G by GROUP_1:def 5
.= A by Th52;
thus A |^ a" |^ a = A |^ (a" * a) by Th47
.= A |^ 1_G by GROUP_1:def 5
.= A by Th52;
end;
theorem Th55:
G is commutative Group iff for A,B st B <> {} holds A |^ B = A
proof
thus G is commutative Group implies for A,B st B <> {} holds A |^ B = A
proof
assume
A1: G is commutative Group;
let A,B;
set y = the Element of B;
assume
A2: B <> {};
then reconsider y as Element of G by TARSKI:def 3;
thus A |^ B c= A
proof
let x be object;
assume x in A |^ B;
then ex a,b st x = a |^ b & a in A & b in B;
hence thesis by A1,Th29;
end;
let x be object;
assume
A3: x in A;
then reconsider a = x as Element of G;
a |^ y = x by A1,Th29;
hence thesis by A2,A3;
end;
assume
A4: for A,B st B <> {} holds A |^ B = A;
now
let a,b;
{a} = {a} |^ {b} by A4
.= {a |^ b} by Th37;
hence a = a |^ b by ZFMISC_1:3;
end;
hence thesis by Th30;
end;
theorem
G is commutative Group iff for A,g holds A |^ g = A
proof
thus G is commutative Group implies for A,g holds A |^ g = A by Th55;
assume
A1: for A,g holds A |^ g = A;
now
let a,b;
{a} = {a} |^ b by A1
.= {a |^ b} by Th37;
hence a = a |^ b by ZFMISC_1:3;
end;
hence thesis by Th30;
end;
theorem
G is commutative Group iff for A,g st A <> {} holds g |^ A = {g}
proof
thus G is commutative Group implies for A,g st A <> {} holds g |^ A = {g} by
Th55;
assume
A1: for A,g st A <> {} holds g |^ A = {g};
now
let a,b;
{a} = a |^ {b} by A1
.= {a |^ b} by Th37;
hence a = a |^ b by ZFMISC_1:3;
end;
hence thesis by Th30;
end;
definition
let G,H,a;
func H |^ a -> strict Subgroup of G means :Def6:
the carrier of it = carr(H) |^ a;
existence
proof
consider H1 being strict Subgroup of G such that
A1: the carrier of H1 = a" * H * a"" by GROUP_2:127;
the carrier of H1 = a" * carr H * a by A1
.= carr(H) |^ a by Th50;
hence thesis;
end;
correctness by GROUP_2:59;
end;
theorem Th58:
x in H |^ a iff ex g st x = g |^ a & g in H
proof
thus x in H |^ a implies ex g st x = g |^ a & g in H
proof
assume x in H |^ a;
then x in the carrier of H |^ a;
then x in carr H |^ a by Def6;
then consider b such that
A1: x = b |^ a & b in carr H by Th41;
take b;
thus thesis by A1;
end;
given g such that
A2: x = g |^ a and
A3: g in H;
g in carr H by A3;
then x in carr H |^ a by A2,Th41;
then x in the carrier of H |^ a by Def6;
hence thesis;
end;
theorem Th59:
the carrier of H |^ a = a" * H * a
proof
thus the carrier of H |^ a = carr(H) |^ a by Def6
.= a" * H * a by Th50;
end;
theorem Th60:
H |^ a |^ b = H |^ (a * b)
proof
the carrier of H |^ a |^ b = carr(H |^ a) |^ b by Def6
.= (carr H |^ a) |^ b by Def6
.= carr H |^ (a * b) by Th47
.= the carrier of H |^ (a * b) by Def6;
hence thesis by GROUP_2:59;
end;
theorem Th61:
for H being strict Subgroup of G holds H |^ 1_G = H
proof
let H be strict Subgroup of G;
the carrier of H |^ 1_G = carr H |^ 1_G by Def6
.= the carrier of H by Th52;
hence thesis by GROUP_2:59;
end;
theorem Th62:
for H being strict Subgroup of G holds
H |^ a |^ a" = H & H |^ a " |^ a = H
proof
let H be strict Subgroup of G;
thus H |^ a |^ a" = H |^ (a * a") by Th60
.= H |^ 1_G by GROUP_1:def 5
.= H by Th61;
thus H |^ a" |^ a = H |^ (a" * a) by Th60
.= H |^ 1_G by GROUP_1:def 5
.= H by Th61;
end;
theorem Th63:
(H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
proof
let g;
thus g in (H1 /\ H2) |^ a implies g in (H1 |^ a) /\ (H2 |^ a)
proof
assume g in (H1 /\ H2) |^ a;
then consider h such that
A1: g = h |^ a and
A2: h in H1 /\ H2 by Th58;
h in H2 by A2,GROUP_2:82;
then
A3: g in H2 |^ a by A1,Th58;
h in H1 by A2,GROUP_2:82;
then g in H1 |^ a by A1,Th58;
hence thesis by A3,GROUP_2:82;
end;
assume
A4: g in (H1 |^ a) /\ (H2 |^ a);
then g in H1 |^ a by GROUP_2:82;
then consider b such that
A5: g = b |^ a and
A6: b in H1 by Th58;
g in H2 |^ a by A4,GROUP_2:82;
then consider c such that
A7: g = c |^ a and
A8: c in H2 by Th58;
b = c by A5,A7,Th16;
then b in (H1 /\ H2) by A6,A8,GROUP_2:82;
hence thesis by A5,Th58;
end;
theorem Th64:
card H = card(H |^ a)
proof
deffunc F(Element of G) = $1 |^ a;
consider f being Function of the carrier of G, the carrier of G such that
A1: for g holds f.g = F(g) from FUNCT_2:sch 4;
set g = f | (the carrier of H);
A2: dom f = the carrier of G & the carrier of H c= the carrier of G by
FUNCT_2:def 1,GROUP_2:def 5;
then
A3: dom g = the carrier of H by RELAT_1:62;
A4: rng g = the carrier of H |^ a
proof
thus rng g c= the carrier of H |^ a
proof
let x be object;
assume x in rng g;
then consider y being object such that
A5: y in dom g and
A6: g.y = x by FUNCT_1:def 3;
reconsider y as Element of H by A2,A5,RELAT_1:62;
reconsider y as Element of G by GROUP_2:42;
A7: f.y = g.y by A5,FUNCT_1:47;
f.y = y |^ a by A1;
then x in carr H |^ a by A6,A7,Th41;
hence thesis by Def6;
end;
let x be object;
assume x in the carrier of H |^ a;
then x in carr H |^ a by Def6;
then consider b such that
A8: x = b |^ a and
A9: b in carr H by Th41;
A10: f.b = b |^ a by A1;
g.b = f.b by A3,A9,FUNCT_1:47;
hence thesis by A3,A8,A9,A10,FUNCT_1:def 3;
end;
g is one-to-one
proof
let x,y be object;
assume that
A11: x in dom g and
A12: y in dom g and
A13: g.x = g.y;
reconsider b = x, c = y as Element of H by A2,A11,A12,RELAT_1:62;
reconsider b,c as Element of G by GROUP_2:42;
A14: f.x = b |^ a & f.y = c |^ a by A1;
f.x = g.x by A11,FUNCT_1:47;
hence thesis by A12,A13,A14,Th16,FUNCT_1:47;
end;
then the carrier of H,the carrier of H |^ a are_equipotent by A3,A4,
WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
theorem Th65:
H is finite iff H |^ a is finite
proof
card H = card(H |^ a) by Th64;
then the carrier of H,the carrier of H |^ a are_equipotent by CARD_1:5;
hence thesis by CARD_1:38;
end;
registration
let G,a;
let H be finite Subgroup of G;
cluster H |^ a -> finite;
coherence by Th65;
end;
theorem
for H being finite Subgroup of G holds card H = card(H |^ a) by Th64;
theorem Th67:
(1).G |^ a = (1).G
proof
A1: the carrier of (1).G = {1_G} by GROUP_2:def 7;
the carrier of (1).G |^ a = (carr (1).G) |^ a by Def6
.= {(1_G) |^ a} by A1,Th37
.= {1_G} by Th17;
hence thesis by GROUP_2:def 7;
end;
theorem
for H being strict Subgroup of G holds H |^ a = (1).G implies H = (1). G
proof
let H be strict Subgroup of G;
assume
A1: H |^ a = (1).G;
then reconsider H as finite Subgroup of G by Th65;
card (1).G = 1 by GROUP_2:69;
then card H = 1 by A1,Th64;
hence thesis by GROUP_2:70;
end;
theorem Th69:
for G being Group, a being Element of G holds (Omega).G |^ a = (Omega).G
proof
let G be Group, a be Element of G;
let h be Element of G;
(h |^ a") |^ a = h |^ (a" * a) by Th24
.= h |^ 1_G by GROUP_1:def 5
.= h by Th19;
hence thesis by Th58,STRUCT_0:def 5;
end;
theorem
for H being strict Subgroup of G holds H |^ a = G implies H = G
proof
let H be strict Subgroup of G;
assume
A1: H |^ a = G;
now
let g;
assume
A2: not g in H;
now
assume g |^ a in H |^ a;
then ex h st g |^ a = h |^ a & h in H by Th58;
hence contradiction by A2,Th16;
end;
hence contradiction by A1;
end;
hence thesis by A1,GROUP_2:62;
end;
theorem Th71:
Index H = Index(H |^ a)
proof
defpred P[object,object] means
ex b st $1 = b * H & $2 = (b |^ a) * (H |^ a);
A1: for x being object st x in Left_Cosets H ex y being object st P[x,y]
proof
let x be object;
assume x in Left_Cosets H;
then consider b such that
A2: x = b * H by GROUP_2:def 15;
reconsider y = (b |^ a) * (H |^ a) as set;
take y;
take b;
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = Left_Cosets H and
A4: for x being object st x in Left_Cosets H holds P[x,f.x]
from CLASSES1:sch 1(A1);
A5: for x,y1,y2 st x in Left_Cosets H & P[x,y1] & P[x,y2] holds y1 = y2
proof
set A = carr H;
let x,y1,y2;
assume x in Left_Cosets H;
given b such that
A6: x = b * H and
A7: y1 = (b |^ a) * (H |^ a);
given c such that
A8: x = c * H and
A9: y2 = (c |^ a) * (H |^ a);
thus y1 = (a" * b * a) * (a" * H * a) by A7,Th59
.= (a" * b * a) * (a" * A) * a by GROUP_2:33
.= (a" * b) * (a * (a" * A)) * a by GROUP_2:32
.= a" * b * (a * a" * A) * a by GROUP_2:32
.= a" * b * (1_G * A) * a by GROUP_1:def 5
.= a" * b * A * a by GROUP_2:37
.= a" * (c * H) * a by A6,A8,GROUP_2:32
.= a" * c * A * a by GROUP_2:32
.= a" * c * (1_G * A) * a by GROUP_2:37
.= a" * c * (a * a" * A) * a by GROUP_1:def 5
.= (a" * c) * (a * (a" * A)) * a by GROUP_2:32
.= (a" * c * a) * (a" * A) * a by GROUP_2:32
.= (a" * c * a) * (a" * H * a) by GROUP_2:33
.= y2 by A9,Th59;
end;
A10: rng f = Left_Cosets(H |^ a)
proof
thus rng f c= Left_Cosets(H |^ a)
proof
let x be object;
assume x in rng f;
then consider y being object such that
A11: y in dom f & f.y = x by FUNCT_1:def 3;
ex b st y = b * H & x = (b |^ a) * (H |^ a) by A3,A4,A11;
hence thesis by GROUP_2:def 15;
end;
let x be object;
assume x in Left_Cosets(H |^ a);
then consider b such that
A12: x = b * (H |^ a) by GROUP_2:def 15;
set c = b |^ a";
A13: x = (c |^ a) * (H |^ a) by A12,Th25;
A14: c * H in Left_Cosets H by GROUP_2:def 15;
then consider d such that
A15: c * H = d * H and
A16: f.(c * H) = (d |^ a) * (H |^ a) by A4;
(c |^ a) * (H |^ a) = (d |^ a) * (H |^ a) by A5,A14,A15;
hence thesis by A3,A13,A14,A16,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A17: x in dom f and
A18: y in dom f and
A19: f.x = f.y;
consider c such that
A20: y = c * H and
A21: f.y = (c |^ a) * (H |^ a) by A3,A4,A18;
consider b such that
A22: x = b * H and
A23: f.x = (b |^ a) * (H |^ a) by A3,A4,A17;
A24: (c |^ a)" * (b |^ a) = (c" |^ a) * (b |^ a) by Th26
.= (c" * b) |^ a by Th23;
(c |^ a)" * (b |^ a) in H |^ a by A19,A23,A21,GROUP_2:114;
then consider d such that
A25: (c" * b) |^ a = d |^ a and
A26: d in H by A24,Th58;
c" * b = d by A25,Th16;
hence thesis by A22,A20,A26,GROUP_2:114;
end;
then Left_Cosets H,Left_Cosets(H |^ a) are_equipotent by A3,A10,
WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
theorem
Left_Cosets H is finite implies index H = index(H |^ a)
proof
assume
A1: Left_Cosets H is finite;
then
A2: ex B being finite set st B = Left_Cosets H & index H = card B by
GROUP_2:def 18;
A3: Index H = Index(H |^ a) by Th71;
then Left_Cosets H,Left_Cosets(H |^ a) are_equipotent by CARD_1:5;
then Left_Cosets(H |^ a) is finite by A1,CARD_1:38;
hence thesis by A2,A3,GROUP_2:def 18;
end;
theorem Th73:
G is commutative Group implies for H being strict Subgroup of G
for a holds H |^ a = H
proof
assume
A1: G is commutative Group;
let H be strict Subgroup of G;
let a;
the carrier of H |^ a = a" * H * a by Th59
.= H * a" * a by A1,GROUP_2:112
.= H * (a" * a) by GROUP_2:107
.= H * 1_G by GROUP_1:def 5
.= the carrier of H by GROUP_2:109;
hence thesis by GROUP_2:59;
end;
definition
let G,a,b;
pred a,b are_conjugated means
:Def7:
ex g st a = b |^ g;
end;
notation
let G,a,b;
antonym a,b are_not_conjugated for a,b are_conjugated;
end;
theorem Th74:
a,b are_conjugated iff ex g st b = a |^ g
proof
thus a,b are_conjugated implies ex g st b = a |^ g
proof
given g such that
A1: a = b |^ g;
a |^ g" = b by A1,Th25;
hence thesis;
end;
given g such that
A2: b = a |^ g;
a = b |^ g" by A2,Th25;
hence thesis;
end;
theorem Th75:
a,a are_conjugated
proof
take 1_G;
thus thesis by Th19;
end;
theorem Th76:
a,b are_conjugated implies b,a are_conjugated
proof
given g such that
A1: a = b |^ g;
b = a |^ g" by A1,Th25;
hence thesis;
end;
definition
let G,a,b;
redefine pred a,b are_conjugated; :: redefines are_conjugated (GROUP_3, definition)
reflexivity by Th75;
symmetry by Th76;
end;
theorem Th77:
a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated
proof
given g such that
A1: a = b |^ g;
given h such that
A2: b = c |^ h;
a = c |^ (h * g) by A1,A2,Th24;
hence thesis;
end;
theorem Th78:
a,1_G are_conjugated or 1_G,a are_conjugated implies a = 1_G
proof
assume
A1: a,1_G are_conjugated or 1_G,a are_conjugated;
now
per cases by A1;
suppose
a,1_G are_conjugated;
then ex g st 1_G = a |^ g by Th74;
hence thesis by Th18;
end;
suppose
1_G,a are_conjugated;
then ex g st 1_G = a |^ g;
hence thesis by Th18;
end;
end;
hence thesis;
end;
theorem Th79:
a |^ carr (Omega).G = {b : a,b are_conjugated}
proof
set A = a |^ carr (Omega).G;
set B = {b : a,b are_conjugated};
thus A c= B
proof
let x be object;
assume
A1: x in A;
then reconsider b = x as Element of G;
ex g st x = a |^ g & g in carr(Omega).G by A1,Th42;
then b,a are_conjugated;
hence thesis;
end;
let x be object;
assume x in B;
then consider b such that
A2: x = b and
A3: a,b are_conjugated;
ex g st b = a |^ g by A3,Def7;
hence thesis by A2,Th42;
end;
definition
let G,a;
func con_class a -> Subset of G equals
a |^ carr (Omega).G;
correctness;
end;
theorem Th80:
x in con_class a iff ex b st b = x & a,b are_conjugated
proof
thus x in con_class a implies ex b st b = x & a,b are_conjugated
proof
assume x in con_class a;
then x in {b : a,b are_conjugated} by Th79;
hence thesis;
end;
given b such that
A1: b = x & a,b are_conjugated;
x in {c : a,c are_conjugated} by A1;
hence thesis by Th79;
end;
theorem Th81:
a in con_class b iff a,b are_conjugated
proof
thus a in con_class b implies a,b are_conjugated
proof
assume a in con_class b;
then ex c st a = c & b,c are_conjugated by Th80;
hence thesis;
end;
assume a,b are_conjugated;
hence thesis by Th80;
end;
theorem Th82:
a |^ g in con_class a by Th80,Th74;
theorem
a in con_class a by Th81;
theorem
a in con_class b implies b in con_class a
proof
assume a in con_class b;
then a,b are_conjugated by Th81;
hence thesis by Th81;
end;
theorem
con_class a = con_class b iff con_class a meets con_class b
proof
thus con_class a = con_class b implies con_class a meets con_class b
by Th81;
assume con_class a meets con_class b;
then consider x being object such that
A1: x in con_class a and
A2: x in con_class b by XBOOLE_0:3;
reconsider x as Element of G by A1;
A3: a,x are_conjugated by A1,Th81;
thus con_class a c= con_class b
proof
let y be object;
assume y in con_class a;
then consider g such that
A4: g = y and
A5: a,g are_conjugated by Th80;
A6: b,x are_conjugated by A2,Th81;
x,a are_conjugated by A1,Th81;
then x,g are_conjugated by A5,Th77;
then b,g are_conjugated by A6,Th77;
hence thesis by A4,Th80;
end;
let y be object;
assume y in con_class b;
then consider g such that
A7: g = y and
A8: b,g are_conjugated by Th80;
x,b are_conjugated by A2,Th81;
then x,g are_conjugated by A8,Th77;
then a,g are_conjugated by A3,Th77;
hence thesis by A7,Th80;
end;
theorem
con_class a = {1_G} iff a = 1_G
proof
thus con_class a = {1_G} implies a = 1_G
proof
assume
A1: con_class a = {1_G};
a in con_class a by Th81;
hence thesis by A1,TARSKI:def 1;
end;
assume
A2: a = 1_G;
thus con_class a c= {1_G}
proof
let x be object;
assume x in con_class a;
then consider b such that
A3: b = x and
A4: a,b are_conjugated by Th80;
b = 1_G by A2,A4,Th78;
hence thesis by A3,TARSKI:def 1;
end;
1_G in con_class a by A2,Th81;
hence thesis by ZFMISC_1:31;
end;
theorem
con_class a * A = A * con_class a
proof
thus con_class a * A c= A * con_class a
proof
let x be object;
assume x in con_class a * A;
then consider b,c such that
A1: x = b * c and
A2: b in con_class a and
A3: c in A;
reconsider h = x as Element of G by A1;
b,a are_conjugated by A2,Th81;
then consider g such that
A4: b = a |^ g;
h |^ c" = c * ((a |^ g) * c) * c" by A1,A4
.= c * (((a |^ g) * c) * c") by GROUP_1:def 3
.= c * (a |^ g) by Th1;
then
A5: x = (c * (a |^ g)) |^ c by Th25
.= (c |^ c) * (a |^ g |^ c) by Th23
.= c * (a |^ g |^ c) by Th20
.= c * (a |^ (g * c)) by Th24;
a |^ (g * c) in con_class a by Th82;
hence thesis by A3,A5;
end;
let x be object;
assume x in A * con_class a;
then consider b,c such that
A6: x = b * c and
A7: b in A and
A8: c in con_class a;
reconsider h = x as Element of G by A6;
c,a are_conjugated by A8,Th81;
then consider g such that
A9: c = a |^ g;
h |^ b = (a |^ g) * b by A6,A9,Th1;
then
A10: x = ((a |^ g) * b) |^ b" by Th25
.= (a |^ g) |^ b" * (b |^ b") by Th23
.= a |^ (g * b") * (b |^ b") by Th24
.= a |^ (g * b") * b by Th1;
a |^ (g * b") in con_class a by Th82;
hence thesis by A7,A10;
end;
definition
let G,A,B;
pred A,B are_conjugated means
ex g st A = B |^ g;
end;
notation
let G,A,B;
antonym A,B are_not_conjugated for A,B are_conjugated;
end;
theorem Th88:
A,B are_conjugated iff ex g st B = A |^ g
proof
thus A,B are_conjugated implies ex g st B = A |^ g
proof
given g such that
A1: A = B |^ g;
A |^ g" = B by A1,Th54;
hence thesis;
end;
given g such that
A2: B = A |^ g;
A = B |^ g" by A2,Th54;
hence thesis;
end;
theorem Th89:
A,A are_conjugated
proof
take 1_G;
thus thesis by Th52;
end;
theorem Th90:
A,B are_conjugated implies B,A are_conjugated
proof
given g such that
A1: A = B |^ g;
B = A |^ g" by A1,Th54;
hence thesis;
end;
definition
let G,A,B;
redefine pred A,B are_conjugated; :: redefines are_conjugated (GROUP_3, definition)
reflexivity by Th89;
symmetry by Th90;
end;
theorem Th91:
A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated
proof
given g such that
A1: A = B |^ g;
given h such that
A2: B = C |^ h;
A = C |^ (h * g) by A1,A2,Th47;
hence thesis;
end;
theorem Th92:
{a},{b} are_conjugated iff a,b are_conjugated
proof
thus {a},{b} are_conjugated implies a,b are_conjugated
proof
assume {a},{b} are_conjugated;
then consider g such that
A1: {a} |^ g = {b} by Th88;
{b} = {a |^ g} by A1,Th37;
then b = a |^ g by ZFMISC_1:3;
hence thesis by Th74;
end;
assume a,b are_conjugated;
then consider g such that
A2: a |^ g = b by Th74;
{b} = {a} |^ g by A2,Th37;
hence thesis by Th88;
end;
theorem Th93:
A,carr H1 are_conjugated implies ex H2 being strict Subgroup of
G st the carrier of H2 = A
proof
assume A,carr H1 are_conjugated;
then consider g such that
A1: A = carr H1 |^ g;
A = the carrier of H1 |^ g by A1,Def6;
hence thesis;
end;
definition
let G,A;
func con_class A -> Subset-Family of G equals
{B : A,B are_conjugated};
coherence
proof
set X = {B: A,B are_conjugated};
X c= bool the carrier of G
proof
let x be object;
assume x in X;
then ex B st x = B & A,B are_conjugated;
hence thesis;
end;
hence thesis;
end;
end;
theorem
x in con_class A iff ex B st x = B & A,B are_conjugated;
theorem Th95:
A in con_class B iff A,B are_conjugated
proof
thus A in con_class B implies A,B are_conjugated
proof
assume A in con_class B;
then ex C st A = C & B,C are_conjugated;
hence thesis;
end;
assume A,B are_conjugated;
hence thesis;
end;
theorem
A |^ g in con_class A
proof
A,A |^ g are_conjugated by Th88;
hence thesis;
end;
theorem
A in con_class A;
theorem
A in con_class B implies B in con_class A
proof
assume A in con_class B;
then A,B are_conjugated by Th95;
hence thesis;
end;
theorem
con_class A = con_class B iff con_class A meets con_class B
proof
thus con_class A = con_class B implies con_class A meets con_class B
proof
A1: A in con_class A;
assume con_class A = con_class B;
hence thesis by A1;
end;
assume con_class A meets con_class B;
then consider x being object such that
A2: x in con_class A and
A3: x in con_class B by XBOOLE_0:3;
reconsider x as Subset of G by A2;
A4: A,x are_conjugated by A2,Th95;
thus con_class A c= con_class B
proof
let y be object;
assume y in con_class A;
then consider C such that
A5: C = y and
A6: A,C are_conjugated;
A7: B,x are_conjugated by A3,Th95;
x,A are_conjugated by A2,Th95;
then x,C are_conjugated by A6,Th91;
then B,C are_conjugated by A7,Th91;
hence thesis by A5;
end;
let y be object;
assume y in con_class B;
then consider C such that
A8: C = y and
A9: B,C are_conjugated;
x,B are_conjugated by A3,Th95;
then x,C are_conjugated by A9,Th91;
then A,C are_conjugated by A4,Th91;
hence thesis by A8;
end;
theorem Th100:
con_class{a} = {{b} : b in con_class a}
proof
set A = {{b} : b in con_class a};
thus con_class{a} c= A
proof
let x be object;
assume x in con_class{a};
then consider B such that
A1: x = B and
A2: {a},B are_conjugated;
consider b such that
A3: {a} |^ b = B by A2,Th88;
a,a |^ b are_conjugated by Th74;
then
A4: a |^ b in con_class a by Th81;
B = {a |^ b} by A3,Th37;
hence thesis by A1,A4;
end;
let x be object;
assume x in A;
then consider b such that
A5: x = {b} and
A6: b in con_class a;
b,a are_conjugated by A6,Th81;
then {b},{a} are_conjugated by Th92;
hence thesis by A5;
end;
theorem
G is finite implies con_class A is finite;
definition
let G,H1,H2;
pred H1,H2 are_conjugated means
ex g st the multMagma of H1 = H2 |^ g;
end;
notation
let G,H1,H2;
antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated;
end;
theorem Th102:
for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated
iff ex g st H2 = H1 |^ g
proof
let H1,H2 be strict Subgroup of G;
thus H1,H2 are_conjugated implies ex g st H2 = H1 |^ g
proof
given g such that
A1: the multMagma of H1 = H2 |^ g;
H1 |^ g" = H2 by A1,Th62;
hence thesis;
end;
given g such that
A2: H2 = H1 |^ g;
H1 = H2 |^ g" by A2,Th62;
hence thesis;
end;
theorem Th103:
for H1 being strict Subgroup of G holds H1,H1 are_conjugated
proof
let H1 be strict Subgroup of G;
take 1_G;
thus thesis by Th61;
end;
theorem Th104:
for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated
implies H2,H1 are_conjugated
proof
let H1,H2 be strict Subgroup of G;
given g such that
A1: the multMagma of H1 = H2 |^ g;
H2 = H1 |^ g" by A1,Th62;
hence thesis;
end;
definition
let G;
let H1,H2 be strict Subgroup of G;
redefine pred H1,H2 are_conjugated; :: redefines are_conjugated (GROUP_3, definition)
reflexivity by Th103;
symmetry by Th104;
end;
theorem Th105:
for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated
& H2,H3 are_conjugated implies H1,H3 are_conjugated
proof
let H1,H2 be strict Subgroup of G;
given g such that
A1: the multMagma of H1 = H2 |^ g;
given h such that
A2: the multMagma of H2 = H3 |^ h;
H1 = H3 |^ (h * g) by A1,A2,Th60;
hence thesis;
end;
reserve L for Subset of Subgroups G;
definition
let G,H;
func con_class H -> Subset of Subgroups G means
:Def12:
for x being object holds x in it iff
ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated;
existence
proof
defpred P[set] means ex H1 being strict Subgroup of G st $1 = H1 & H,H1
are_conjugated;
consider L such that
A1: x in L iff x in Subgroups G & P[x] from SUBSET_1:sch 1;
take L;
let x be object;
thus x in L implies ex H1 being strict Subgroup of G st x = H1 & H,H1
are_conjugated by A1;
given H1 being strict Subgroup of G such that
A2: x = H1 and
A3: H,H1 are_conjugated;
x in Subgroups G by A2,Def1;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
defpred P[object] means
ex H3 being strict Subgroup of G st $1 = H3 & H,H3 are_conjugated;
let A1,A2 be Subset of Subgroups G;
assume
A4: for x being object holds x in A1 iff P[x];
assume
A5: for x being object holds x in A2 iff P[x];
thus thesis from XBOOLE_0:sch 2(A4,A5);
end;
end;
theorem Th106:
x in con_class H implies x is strict Subgroup of G
proof
assume x in con_class H;
then ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated by
Def12;
hence thesis;
end;
theorem Th107:
for H1,H2 being strict Subgroup of G holds H1 in con_class H2
iff H1,H2 are_conjugated
proof
let H1,H2 be strict Subgroup of G;
thus H1 in con_class H2 implies H1,H2 are_conjugated
proof
assume H1 in con_class H2;
then
ex H3 being strict Subgroup of G st H1 = H3 & H2,H3 are_conjugated by Def12
;
hence thesis;
end;
assume H1,H2 are_conjugated;
hence thesis by Def12;
end;
theorem Th108:
for H being strict Subgroup of G holds H |^ g in con_class H
proof
let H be strict Subgroup of G;
H,H |^ g are_conjugated by Th102;
hence thesis by Def12;
end;
theorem Th109:
for H being strict Subgroup of G holds H in con_class H
proof
let H be strict Subgroup of G;
H,H are_conjugated;
hence thesis by Def12;
end;
theorem
for H1,H2 being strict Subgroup of G holds H1 in con_class H2 implies
H2 in con_class H1
proof
let H1,H2 be strict Subgroup of G;
assume H1 in con_class H2;
then H1,H2 are_conjugated by Th107;
hence thesis by Th107;
end;
theorem
for H1,H2 being strict Subgroup of G holds con_class H1 = con_class H2
iff con_class H1 meets con_class H2
proof
let H1,H2 be strict Subgroup of G;
thus con_class H1 = con_class H2 implies con_class H1 meets con_class H2
by Th109;
assume con_class H1 meets con_class H2;
then consider x being object such that
A1: x in con_class H1 and
A2: x in con_class H2 by XBOOLE_0:3;
reconsider x as strict Subgroup of G by A1,Th106;
A3: H1,x are_conjugated by A1,Th107;
thus con_class H1 c= con_class H2
proof
let y be object;
assume y in con_class H1;
then consider H3 being strict Subgroup of G such that
A4: H3 = y and
A5: H1,H3 are_conjugated by Def12;
A6: H2,x are_conjugated by A2,Th107;
x,H1 are_conjugated by A1,Th107;
then x,H3 are_conjugated by A5,Th105;
then H2,H3 are_conjugated by A6,Th105;
hence thesis by A4,Def12;
end;
let y be object;
assume y in con_class H2;
then consider H3 being strict Subgroup of G such that
A7: H3 = y and
A8: H2,H3 are_conjugated by Def12;
x,H2 are_conjugated by A2,Th107;
then x,H3 are_conjugated by A8,Th105;
then H1,H3 are_conjugated by A3,Th105;
hence thesis by A7,Def12;
end;
theorem
G is finite implies con_class H is finite by Th15,FINSET_1:1;
theorem Th113:
for H1 being strict Subgroup of G holds H1,H2 are_conjugated
iff carr H1,carr H2 are_conjugated
proof
let H1 be strict Subgroup of G;
thus H1,H2 are_conjugated implies carr H1,carr H2 are_conjugated
proof
given a such that
A1: the multMagma of H1 = H2 |^ a;
carr H1 = carr H2 |^ a by A1,Def6;
hence thesis;
end;
given a such that
A2: carr H1 = carr H2 |^ a;
H1 = H2 |^ a by A2,Def6;
hence thesis;
end;
definition
let G;
let IT be Subgroup of G;
attr IT is normal means :Def13:
for a holds IT |^ a = the multMagma of IT;
end;
registration
let G;
cluster strict normal for Subgroup of G;
existence
proof
for a holds (1).G |^ a = (1).G by Th67;
then (1).G is normal;
hence thesis;
end;
end;
reserve N2 for normal Subgroup of G;
theorem Th114:
(1).G is normal & (Omega).G is normal
by Th67,Th69;
theorem
for N1,N2 being strict normal Subgroup of G holds N1 /\ N2 is normal
proof
let N1,N2 be strict normal Subgroup of G;
let a;
thus (N1 /\ N2) |^ a = (N1 |^ a) /\ (N2 |^ a) by Th63
.= N1 /\ (N2 |^ a) by Def13
.= the multMagma of (N1 /\ N2) by Def13;
end;
theorem
for H being strict Subgroup of G holds G is commutative Group implies
H is normal by Th73;
theorem Th117:
H is normal Subgroup of G iff for a holds a * H = H * a
proof
thus H is normal Subgroup of G implies for a holds a * H = H * a
proof
assume
A1: H is normal Subgroup of G;
let a;
A2: carr(H |^ a) = a" * H * a by Th59;
carr(H |^ a) = the carrier of the multMagma of H by A1,Def13
.= carr H;
hence a * H = a * (a" * H) * a by A2,GROUP_2:33
.= a * a" * H * a by GROUP_2:105
.= 1_G * H * a by GROUP_1:def 5
.= H * a by GROUP_2:37;
end;
assume
A3: for a holds a * H = H * a;
H is normal
proof
let a;
the carrier of H |^ a = a" * H * a by Th59
.= H * a" * a by A3
.= H * (a" * a) by GROUP_2:107
.= H * 1_G by GROUP_1:def 5
.= the carrier of H by GROUP_2:109;
hence thesis by GROUP_2:59;
end;
hence thesis;
end;
theorem
for H being Subgroup of G holds
H is normal iff for a holds a * H c= H * a
proof
let H be Subgroup of G;
thus H is normal implies for a holds a * H c= H * a by Th117;
assume
A1: for a holds a * H c= H * a;
now
let a;
a" * H c= H * a" by A1;
then a * (a" * H) c= a * (H * a") by Th4;
then a * a" * H c= a * (H * a") by GROUP_2:105;
then 1_G * H c= a * (H * a") by GROUP_1:def 5;
then carr H c= a * (H * a") by GROUP_2:109;
then carr H c= a * H * a" by GROUP_2:106;
then carr H * a c= a * H * a" * a by Th4;
then H * a c= a * H * (a" * a) by GROUP_2:34;
then H * a c= a * H * 1_G by GROUP_1:def 5;
hence H * a c= a * H by GROUP_2:37;
end;
then for a holds a * H = H * a by A1;
hence thesis by Th117;
end;
theorem Th119:
for H being Subgroup of G holds
H is normal iff for a holds H * a c= a * H
proof
let H be Subgroup of G;
thus H is normal implies for a holds H * a c= a * H by Th117;
assume
A1: for a holds H * a c= a * H;
now
let a;
H * a" c= a" * H by A1;
then a * (H * a") c= a * (a" * H) by Th4;
then a * (H * a") c= a * a" * H by GROUP_2:105;
then a * (H * a") c= 1_G * H by GROUP_1:def 5;
then a * (H * a") c= carr H by GROUP_2:109;
then a * H * a" c= carr H by GROUP_2:106;
then a * H * a" * a c= carr H * a by Th4;
then a * H * (a" * a) c= H * a by GROUP_2:34;
then a * H * 1_G c= H * a by GROUP_1:def 5;
hence a * H c= H * a by GROUP_2:37;
end;
then for a holds a * H = H * a by A1;
hence thesis by Th117;
end;
theorem
for H being Subgroup of G holds
H is normal iff for A holds A * H = H * A
proof
let H be Subgroup of G;
thus H is normal implies for A holds A * H = H * A
proof
assume
A1: H is normal;
let A;
thus A * H c= H * A
proof
let x be object;
assume x in A * H;
then consider a,h such that
A2: x = a * h and
A3: a in A and
A4: h in H by GROUP_2:94;
x in a * H by A2,A4,GROUP_2:103;
then x in H * a by A1,Th117;
then ex g st x = g * a & g in H by GROUP_2:104;
hence thesis by A3;
end;
let x be object;
assume x in H * A;
then consider h,a such that
A5: x = h * a & h in H and
A6: a in A by GROUP_2:95;
x in H * a by A5,GROUP_2:104;
then x in a * H by A1,Th117;
then ex g st x = a * g & g in H by GROUP_2:103;
hence thesis by A6;
end;
assume
A7: for A holds A * H = H * A;
now
let a;
thus a * H = {a} * H .= H * {a} by A7
.= H * a;
end;
hence thesis by Th117;
end;
theorem
for H being strict Subgroup of G holds
H is normal iff for a holds H is Subgroup of H |^ a
proof
let H be strict Subgroup of G;
thus H is normal implies for a holds H is Subgroup of H |^ a
proof
assume
A1: H is normal;
let a;
H |^ a = the multMagma of H by A1;
hence thesis by GROUP_2:54;
end;
assume
A2: for a holds H is Subgroup of H |^ a;
now
let a;
A3: H |^ a" * a = a"" * H * a" * a by Th59
.= a"" * H * (a" * a) by GROUP_2:34
.= a"" * H * 1_G by GROUP_1:def 5
.= a"" * H by GROUP_2:37
.= a * H;
H is Subgroup of H |^ a" by A2;
hence H * a c= a * H by A3,Th6;
end;
hence thesis by Th119;
end;
ThN1:
for G being Group
for H being Subgroup of G holds
H is normal iff for g,h being Element of G st h in H holds h |^ g in H
proof
let G be Group, H be Subgroup of G;
hereby assume H is normal; then
A1: for a being Element of G holds H |^ a = the multMagma of H;
thus for g,h being Element of G st h in H holds h |^ g in H
proof
let g,h be Element of G;
assume h in H;
then g" * (h * g) in g" * (H * g) by GROUP_2:104,GROUP_2:27;
then g" * h * g in g" * (H * g) by GROUP_1:def 3;
then g" * h * g in g" * H * g by GROUP_2:106;
then g" * h * g in H |^ g by Th59;
then g" * h * g in H by A1;
hence thesis;
end;
end;
assume B: for g,h being Element of G st h in H holds h |^ g in H;
now let a be Element of G;
B2: now let o be object;
assume o in the carrier of (H |^ a); then
o in H |^ a; then
consider b being Element of G such that
B3: o = b |^ a & b in H by Th58;
b |^ a in H by B,B3;
hence o in the carrier of H by B3;
end;
now let o be object;
assume C1: o in the carrier of H;
the carrier of H c= the carrier of G by GROUP_2:def 5; then
reconsider b = o as Element of G by C1;
b in H by C1; then
b |^ (a") in H by B; then
a"" * b * a" in H; then
(a * b * a") * a in H * a by GROUP_2:104; then
(a * b) * (a" * a) in H * a by GROUP_1:def 3; then
(a * b) * (1_G) in H * a by GROUP_1:def 5; then
a * b in H * a by GROUP_1:def 4; then
a" * (a * b) in a" * (H * a) by GROUP_2:27; then
(a" * a) * b in a" * (H * a) by GROUP_1:def 3; then
(1_G) * b in a" * (H * a) by GROUP_1:def 5; then
b in a" * (H * a) by GROUP_1:def 4; then
b in a" * H * a by GROUP_2:106;
hence o in the carrier of (H |^ a) by Th59;
end;
hence H |^ a = the multMagma of H by B2,TARSKI:2,GROUP_2:59;
end;
hence H is normal;
end;
theorem
for G being Group
for H being Subgroup of G holds
H is normal iff
for g being Element of G holds H |^ g is Subgroup of H
proof
let G be Group, H be Subgroup of G;
hereby assume A1: H is normal;
thus for g being Element of G holds H |^ g is Subgroup of H
proof
let g be Element of G;
the carrier of (H|^g) c= the carrier of H
proof let o be object;
assume o in the carrier of (H|^g); then
o in H |^ g; then
consider b being Element of G such that
A4: o = b |^ g & b in H by Th58;
b |^ g in H by A4,A1,ThN1;
hence o in the carrier of H by A4;
end;
hence H |^ g is Subgroup of H by GROUP_2:57;
end;
end;
assume B: for g being Element of G holds H |^ g is Subgroup of H;
now let g,h be Element of G;
H |^ g is Subgroup of H by B; then
B1: the carrier of (H|^g) c= the carrier of H by GROUP_2:def 5;
assume h in H;
then h |^ g in H |^ g by Th58;
hence h |^ g in H by B1;
end;
hence H is normal by ThN1;
end;
theorem
for H being strict Subgroup of G holds
H is normal iff con_class H = {H}
proof
let H be strict Subgroup of G;
thus H is normal implies con_class H = {H}
proof
assume
A1: H is normal;
thus con_class H c= {H}
proof
let x be object;
assume x in con_class H;
then consider H1 being strict Subgroup of G such that
A2: x = H1 and
A3: H,H1 are_conjugated by Def12;
ex g st H1 = H |^ g by A3,Th102;
then x = H by A1,A2;
hence thesis by TARSKI:def 1;
end;
H in con_class H by Th109;
hence thesis by ZFMISC_1:31;
end;
assume
A4: con_class H = {H};
H is normal
proof
let a;
H |^ a in con_class H by Th108;
hence thesis by A4,TARSKI:def 1;
end;
hence thesis;
end;
theorem
for H being strict Subgroup of G holds H is normal Subgroup of G iff
for a st a in H holds con_class a c= carr H
proof
let H be strict Subgroup of G;
thus H is normal Subgroup of G implies
for a st a in H holds con_class a c= carr H
proof
assume
A1: H is normal Subgroup of G;
let a;
assume
A2: a in H;
let x be object;
assume x in con_class a;
then consider b such that
A3: x = b and
A4: a,b are_conjugated by Th80;
consider c such that
A5: b = a |^ c by A4,Th74;
x in H |^ c by A2,A3,A5,Th58;
then x in H by A1,Def13;
hence thesis;
end;
assume
A6: for a st a in H holds con_class a c= carr H;
H is normal
proof
let a;
H |^ a = H
proof
let b;
thus b in H |^ a implies b in H
proof
assume b in H |^ a;
then consider c such that
A7: b = c |^ a & c in H by Th58;
b in con_class c & con_class c c= carr H by A6,A7,Th82;
hence thesis;
end;
assume b in H; then
A8: con_class b c= carr H by A6;
b |^ a" in con_class b by Th82;
then b |^ a" in H by A8;
then b |^ a" |^ a in H |^ a by Th58;
hence thesis by Th25;
end;
hence thesis;
end;
hence thesis;
end;
Lm5: for N1 being strict normal Subgroup of G holds
carr N1 * carr N2 c= carr N2 * carr N1
proof
let N1 be strict normal Subgroup of G;
let x be object;
assume x in carr N1 * carr N2;
then consider a,b such that
A1: x = a * b and
A2: a in carr N1 and
A3: b in carr N2;
a in N1 by A2;
then a |^ b in N1 |^ b by Th58;
then a |^ b in the multMagma of N1 by Def13;
then
A4: a |^ b in carr N1;
b * (a |^ b) = b * (b" * (a * b)) by GROUP_1:def 3
.= a * b by Th1;
hence thesis by A1,A3,A4;
end;
theorem Th125:
for N1,N2 being strict normal Subgroup of G holds
carr N1 * carr N2 = carr N2 * carr N1 by Lm5;
theorem
for N1,N2 being strict normal Subgroup of G
ex N being strict normal Subgroup of G st
the carrier of N = carr N1 * carr N2
proof
let N1,N2 be strict normal Subgroup of G;
set A = carr N1 * carr N2;
set B = carr N1;
set C = carr N2;
carr N1 * carr N2 = carr N2 * carr N1 by Th125;
then consider H being strict Subgroup of G such that
A1: the carrier of H = A by GROUP_2:78;
now
let a;
thus a * H = a * N1 * C by A1,GROUP_2:29
.= N1 * a * C by Th117
.= B * (a * N2) by GROUP_2:30
.= B * (N2 * a) by Th117
.= H * a by A1,GROUP_2:31;
end;
then H is normal Subgroup of G by Th117;
hence thesis by A1;
end;
theorem
for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N
proof
let N be normal Subgroup of G;
thus Left_Cosets N c= Right_Cosets N
proof
let x be object;
assume x in Left_Cosets N;
then consider a such that
A1: x = a * N by GROUP_2:def 15;
x = N * a by A1,Th117;
hence thesis by GROUP_2:def 16;
end;
let x be object;
assume x in Right_Cosets N;
then consider a such that
A2: x = N * a by GROUP_2:def 16;
x = a * N by A2,Th117;
hence thesis by GROUP_2:def 15;
end;
theorem
for H being Subgroup of G holds Left_Cosets H is finite & index H = 2
implies H is normal Subgroup of G
proof
let H be Subgroup of G;
assume that
A1: Left_Cosets H is finite and
A2: index H = 2;
ex B being finite set st B = Left_Cosets H & index H = card B by A1,
GROUP_2:146;
then consider x,y being object such that
A3: x <> y and
A4: Left_Cosets H = {x,y} by A2,CARD_2:60;
carr H in Left_Cosets H by GROUP_2:135;
then {x,y} = {x,carr H} or {x,y} = {carr H,y} by A4,TARSKI:def 2;
then consider z3 being object such that
A5: {x,y} = {carr H,z3};
reconsider z3 as set by TARSKI:1;
A6: carr H misses z3
proof
z3 in Left_Cosets H by A4,A5,TARSKI:def 2;
then
A7: ex a st z3 = a * H by GROUP_2:def 15;
A8: carr H = 1_G * H by GROUP_2:109;
assume not thesis;
then carr H = z3 by A7,A8,GROUP_2:115;
then
A9: {x,y} = {carr H} by A5,ENUMSET1:29;
then x = carr H by ZFMISC_1:4;
hence thesis by A3,A9,ZFMISC_1:4;
end;
union Left_Cosets H = the carrier of G & union Left_Cosets H = carr H
\/ z3 by A4,A5,GROUP_2:137,ZFMISC_1:75;
then
A10: union Right_Cosets H = the carrier of G & z3 = (the carrier of G) \
carr H by A6,GROUP_2:137,XBOOLE_1:88;
ex C being finite set st C = Right_Cosets H & index H = card C by A1,
GROUP_2:146;
then consider z1,z2 being object such that
A11: z1 <> z2 and
A12: Right_Cosets H = {z1,z2} by A2,CARD_2:60;
carr H in Right_Cosets H by GROUP_2:135;
then {z1,z2} = {z1,carr H} or {z1,z2} = {carr H,z2} by A12,TARSKI:def 2;
then consider z4 being object such that
A13: {z1,z2} = {carr H,z4};
reconsider z4 as set by TARSKI:1;
A14: carr H misses z4
proof
z4 in Right_Cosets H by A12,A13,TARSKI:def 2;
then
A15: ex a st z4 = H * a by GROUP_2:def 16;
A16: carr H = H * 1_G by GROUP_2:109;
assume not thesis;
then carr H = z4 by A15,A16,GROUP_2:121;
then
A17: {z1,z2} = {carr H} by A13,ENUMSET1:29;
then z1 = carr H by ZFMISC_1:4;
hence thesis by A11,A17,ZFMISC_1:4;
end;
A18: union Right_Cosets H = carr H \/ z4 by A12,A13,ZFMISC_1:75;
now
let c;
now
per cases;
suppose
A19: c * H = carr H;
then c in H by GROUP_2:113;
hence c * H = H * c by A19,GROUP_2:119;
end;
suppose
A20: c * H <> carr H;
then not c in H by GROUP_2:113;
then
A21: H * c <> carr H by GROUP_2:119;
c * H in Left_Cosets H by GROUP_2:def 15;
then
A22: c * H = z3 by A4,A5,A20,TARSKI:def 2;
H * c in Right_Cosets H by GROUP_2:def 16;
then H * c = z4 by A12,A13,A21,TARSKI:def 2;
hence c * H = H * c by A10,A18,A14,A22,XBOOLE_1:88;
end;
end;
hence c * H = H * c;
end;
hence thesis by Th117;
end;
definition
let G;
let A;
func Normalizer A -> strict Subgroup of G means :Def14:
the carrier of it = {h : A |^ h = A};
existence
proof
set X = {h : A |^ h = A};
X c= the carrier of G
proof
let x be object;
assume x in X;
then ex h st x = h & A |^ h = A;
hence thesis;
end;
then reconsider X as Subset of G;
A1: now
let a,b;
assume a in X & b in X;
then ( ex g st a = g & A |^ g = A)& ex h st b = h & A |^ h = A;
then A |^ (a * b) = A by Th47;
hence a * b in X;
end;
A2: now
let a;
assume a in X;
then ex b st a = b & A |^ b = A;
then A = A |^ a" by Th54;
hence a" in X;
end;
A |^ 1_G = A by Th52;
then 1_G in X;
hence thesis by A1,A2,GROUP_2:52;
end;
uniqueness by GROUP_2:59;
end;
theorem Th129:
x in Normalizer A iff ex h st x = h & A |^ h = A
proof
thus x in Normalizer A implies ex h st x = h & A |^ h = A
proof
assume x in Normalizer A;
then x in the carrier of Normalizer A;
then x in {h : A |^ h = A} by Def14;
hence thesis;
end;
given h such that
A1: x = h & A |^ h = A;
x in {b : A |^ b = A} by A1;
then x in the carrier of Normalizer A by Def14;
hence thesis;
end;
theorem Th130:
card con_class A = Index Normalizer A
proof
defpred P[object,object] means
ex a st $1 = A |^ a & $2 = Normalizer A * a;
A1: for x being object st x in con_class A ex y being object st P[x,y]
proof
let x be object;
assume x in con_class A;
then consider B such that
A2: x = B and
A3: A,B are_conjugated;
consider g such that
A4: B = A |^ g by A3,Th88;
reconsider y = Normalizer A * g as set;
take y;
take g;
thus thesis by A2,A4;
end;
consider f being Function such that
A5: dom f = con_class A and
A6: for x being object st x in con_class A holds P[x,f.x]
from CLASSES1:sch 1(A1);
A7: for x,y1,y2 st x in con_class A & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2;
assume x in con_class A;
given a such that
A8: x = A |^ a and
A9: y1 = Normalizer A * a;
given b such that
A10: x = A |^ b and
A11: y2 = Normalizer A * b;
A = A |^ b |^ a" by A8,A10,Th54
.= A |^ (b * a") by Th47;
then b * a" in Normalizer A by Th129;
hence thesis by A9,A11,GROUP_2:120;
end;
A12: rng f = Right_Cosets Normalizer A
proof
thus rng f c= Right_Cosets Normalizer A
proof
let x be object;
assume x in rng f;
then consider y being object such that
A13: y in dom f & f.y = x by FUNCT_1:def 3;
ex a st y = A |^ a & x = Normalizer A * a by A5,A6,A13;
hence thesis by GROUP_2:def 16;
end;
let x be object;
assume x in Right_Cosets Normalizer A;
then consider a such that
A14: x = Normalizer A * a by GROUP_2:def 16;
set y = A |^ a;
A,A |^ a are_conjugated by Th88;
then
A15: y in con_class A;
then ex b st y = A |^ b & f.y = Normalizer A * b by A6;
then x = f.y by A7,A14,A15;
hence thesis by A5,A15,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A16: x in dom f and
A17: y in dom f and
A18: f.x = f.y;
consider b such that
A19: y = A |^ b and
A20: f.y = Normalizer A * b by A5,A6,A17;
consider a such that
A21: x = A |^ a and
A22: f.x = Normalizer A * a by A5,A6,A16;
b * a" in Normalizer A by A18,A22,A20,GROUP_2:120;
then ex h st b * a" = h & A |^ h = A by Th129;
then A = A |^ b |^ a" by Th47;
hence thesis by A21,A19,Th54;
end;
then con_class A,Right_Cosets Normalizer A are_equipotent by A5,A12,
WELLORD2:def 4;
hence card con_class A = card Right_Cosets Normalizer A by CARD_1:5
.= Index Normalizer A by GROUP_2:145;
end;
theorem
con_class A is finite or Left_Cosets Normalizer A is finite implies
ex C being finite set st C = con_class A & card C = index Normalizer A
proof
A1: card con_class A = Index Normalizer A by Th130
.= card Left_Cosets Normalizer A;
then
A2: con_class A,Left_Cosets Normalizer A are_equipotent by CARD_1:5;
assume
A3: con_class A is finite or Left_Cosets Normalizer A is finite;
then reconsider C = con_class A as finite set by A2,CARD_1:38;
take C;
thus C = con_class A;
Left_Cosets Normalizer A is finite by A3,A2,CARD_1:38;
hence thesis by A1,GROUP_2:def 18;
end;
theorem Th132:
card con_class a = Index Normalizer{a}
proof
deffunc F(object) = {$1};
consider f being Function such that
A1: dom f = con_class a and
A2: for x being object st x in con_class a holds f.x = F(x)
from FUNCT_1:sch 3;
A3: rng f = con_class{a}
proof
thus rng f c= con_class{a}
proof
let x be object;
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: f.y = x by FUNCT_1:def 3;
reconsider y as Element of G by A1,A4;
f.y = {y} by A1,A2,A4;
then x in {{d} : d in con_class a} by A1,A4,A5;
hence thesis by Th100;
end;
let x be object;
assume x in con_class{a};
then x in {{b} : b in con_class a} by Th100;
then consider b such that
A6: x = {b} and
A7: b in con_class a;
f.b = {b} by A2,A7;
hence thesis by A1,A6,A7,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A8: x in dom f & y in dom f and
A9: f.x = f.y;
f.x = {x} & f.y = {y} by A1,A2,A8;
hence thesis by A9,ZFMISC_1:3;
end;
then con_class a,con_class{a} are_equipotent by A1,A3,WELLORD2:def 4;
hence card con_class a = card con_class{a} by CARD_1:5
.= Index Normalizer{a} by Th130;
end;
theorem
con_class a is finite or Left_Cosets Normalizer{a} is finite implies
ex C being finite set st C = con_class a & card C = index Normalizer{a}
proof
A1: card con_class a = Index Normalizer {a} by Th132
.= card Left_Cosets Normalizer {a};
then
A2: con_class a,Left_Cosets Normalizer {a} are_equipotent by CARD_1:5;
assume
A3: con_class a is finite or Left_Cosets Normalizer {a} is finite;
then reconsider C = con_class a as finite set by A2,CARD_1:38;
take C;
thus C = con_class a;
Left_Cosets Normalizer {a} is finite by A3,A2,CARD_1:38;
hence thesis by A1,GROUP_2:def 18;
end;
definition
let G;
let H;
func Normalizer H -> strict Subgroup of G equals
Normalizer carr H;
correctness;
end;
theorem Th134:
for H being strict Subgroup of G holds
x in Normalizer H iff ex h st x = h & H |^ h = H
proof
let H be strict Subgroup of G;
thus x in Normalizer H implies ex h st x = h & H |^ h = H
proof
assume x in Normalizer H;
then consider a such that
A1: x = a and
A2: carr H |^ a = carr H by Th129;
H |^ a = H by A2,Def6;
hence thesis by A1;
end;
given h such that
A3: x = h and
A4: H |^ h = H;
carr H |^ h = carr H by A4,Def6;
hence thesis by A3,Th129;
end;
theorem Th135:
for H being strict Subgroup of G holds
card con_class H = Index Normalizer H
proof
let H be strict Subgroup of G;
defpred P[object,object] means
ex H1 being strict Subgroup of G st $1 = H1 & $2 = carr H1;
A1: for x being object st x in con_class H ex y being object st P[x,y]
proof
let x be object;
assume x in con_class H;
then reconsider H = x as strict Subgroup of G by Def1;
reconsider y = carr H as set;
take y;
take H;
thus thesis;
end;
consider f being Function such that
A2: dom f = con_class H and
A3: for x being object st x in con_class H holds P[x,f.x]
from CLASSES1:sch 1(A1);
A4: rng f = con_class carr H
proof
thus rng f c= con_class carr H
proof
let x be object;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: f.y = x by FUNCT_1:def 3;
consider H1 being strict Subgroup of G such that
A7: y = H1 and
A8: x = carr H1 by A2,A3,A5,A6;
H1,H are_conjugated by A2,A5,A7,Th107;
then carr H1,carr H are_conjugated by Th113;
hence thesis by A8;
end;
let x be object;
assume x in con_class carr H;
then consider B such that
A9: B = x and
A10: carr H,B are_conjugated;
consider H1 being strict Subgroup of G such that
A11: the carrier of H1 = B by A10,Th93;
B = carr H1 by A11;
then H1,H are_conjugated by A10,Th113;
then
A12: H1 in con_class H by Th107;
then ex H2 being strict Subgroup of G st H1 = H2 & f.H1 = carr H2 by A3;
hence thesis by A2,A9,A11,A12,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A13: x in dom f & y in dom f and
A14: f.x = f.y;
(ex H1 being strict Subgroup of G st x = H1 & f.x = carr H1 )& ex H2
being strict Subgroup of G st y = H2 & f.y = carr H2 by A2,A3,A13;
hence thesis by A14,GROUP_2:59;
end;
then con_class H,con_class carr H are_equipotent by A2,A4,WELLORD2:def 4;
hence card con_class H = card con_class carr H by CARD_1:5
.= Index Normalizer H by Th130;
end;
theorem
for H being strict Subgroup of G holds
con_class H is finite or Left_Cosets Normalizer H is finite
implies ex C being finite set st
C = con_class H & card C = index Normalizer H
proof
let H be strict Subgroup of G;
A1: card con_class H = Index Normalizer H by Th135
.= card Left_Cosets Normalizer H;
then
A2: con_class H,Left_Cosets Normalizer H are_equipotent by CARD_1:5;
assume
A3: con_class H is finite or Left_Cosets Normalizer H is finite;
then reconsider C = con_class H as finite set by A2,CARD_1:38;
take C;
thus C = con_class H;
Left_Cosets Normalizer H is finite by A3,A2,CARD_1:38;
hence thesis by A1,GROUP_2:def 18;
end;
theorem Th137:
for G being strict Group, H being strict Subgroup of G holds
H is normal iff Normalizer H = G
proof
let G be strict Group, H be strict Subgroup of G;
thus H is normal implies Normalizer H = G
proof
assume
A1: H is normal;
now
let a be Element of G;
H |^ a = H by A1;
hence a in Normalizer H by Th134;
end;
hence thesis by GROUP_2:62;
end;
assume
A2: Normalizer H = G;
let a be Element of G;
a in Normalizer H by A2;
then ex b being Element of G st b = a & H |^ b = H by Th134;
hence thesis;
end;
theorem
for G being strict Group holds Normalizer (1).G = G
proof
let G be strict Group;
(1).G is normal Subgroup of G by Th114;
hence thesis by Th137;
end;
theorem
for G being strict Group holds Normalizer (Omega).G = G
proof
let G be strict Group;
(Omega).G is normal Subgroup of G by Th114;
hence thesis by Th137;
end;