group_3.miz
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 ::
GROUP_3:1
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 ::
GROUP_3:2
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 ::
GROUP_3:3
(
(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 ::
GROUP_3:4
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 ::
GROUP_3:5
A
c= B implies (a
* A)
c= (a
* B) & (A
* a)
c= (B
* a) by
Th4;
theorem ::
GROUP_3:6
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 ::
GROUP_3:7
(a
* H)
= (
{a}
* H);
theorem ::
GROUP_3:8
(H
* a)
= (H
*
{a});
theorem ::
GROUP_3:9
Th9: ((A
* a)
* H)
= (A
* (a
* H))
proof
thus ((A
* a)
* H)
= (A
* (
{a}
* H)) by
GROUP_2: 96
.= (A
* (a
* H));
end;
theorem ::
GROUP_3:10
((a
* H)
* A)
= (a
* (H
* A))
proof
thus ((a
* H)
* A)
= ((
{a}
* H)
* A)
.= (a
* (H
* A)) by
GROUP_2: 97;
end;
theorem ::
GROUP_3:11
((A
* H)
* a)
= (A
* (H
* a))
proof
thus ((A
* H)
* a)
= (A
* (H
*
{a})) by
GROUP_2: 97
.= (A
* (H
* a));
end;
theorem ::
GROUP_3:12
((H
* a)
* A)
= (H
* (a
* A))
proof
thus ((H
* a)
* A)
= ((H
*
{a})
* A)
.= (H
* (a
* A)) by
GROUP_2: 98;
end;
theorem ::
GROUP_3:13
((H1
* a)
* H2)
= (H1
* (a
* H2)) by
Th9;
definition
let G;
::
GROUP_3:def1
func
Subgroups G ->
set means
:
Def1: for x be
object holds x
in it iff x is
strict
Subgroup of G;
existence
proof
defpred
P[
object,
object] means ex H be
strict
Subgroup of G st $2
= H & $1
= the
carrier of H;
defpred
P[
set] means ex H be
strict
Subgroup of G st $1
= the
carrier of H;
consider B be
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 be
object st
P[x, y1] &
P[x, y2] holds y1
= y2 by
GROUP_2: 59;
consider f be
Function such that
A3: for x,y be
object holds
[x, y]
in f iff x
in B &
P[x, y] from
FUNCT_1:sch 1(
A2);
for x be
object holds x
in B iff ex y be
object st
[x, y]
in f
proof
let x be
object;
thus x
in B implies ex y be
object st
[x, y]
in f
proof
assume
A4: x
in B;
then
consider H be
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 be
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 be
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 be
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 be
object holds x
in A1 iff
P[x];
assume
A11: for x be
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 ::
GROUP_3:14
for G be
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 ::
GROUP_3:15
Th15: G is
finite implies (
Subgroups G) is
finite
proof
defpred
P[
object,
object] means ex H be
strict
Subgroup of G st $1
= H & $2
= the
carrier of H;
assume
A1: G is
finite;
A2: for x be
object st x
in (
Subgroups G) holds ex y be
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 be
Function such that
A3: (
dom f)
= (
Subgroups G) and
A4: for x be
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 be
object such that
A6: y
in (
dom f) & (f
. y)
= x by
FUNCT_1:def 3;
consider H be
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 be
strict
Subgroup of G st x
= H1 & (f
. x)
= the
carrier of H1) & ex H2 be
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;
::
GROUP_3:def2
func a
|^ b ->
Element of G equals (((b
" )
* a)
* b);
correctness ;
end
theorem ::
GROUP_3:16
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 ::
GROUP_3:17
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 ::
GROUP_3:18
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 ::
GROUP_3:19
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 ::
GROUP_3:20
Th20: (a
|^ a)
= a
proof
thus (a
|^ a)
= ((
1_ G)
* a) by
GROUP_1:def 5
.= a by
GROUP_1:def 4;
end;
theorem ::
GROUP_3:21
(a
|^ (a
" ))
= a & ((a
" )
|^ a)
= (a
" ) by
Th1;
theorem ::
GROUP_3:22
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 ::
GROUP_3:23
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 ::
GROUP_3:24
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 ::
GROUP_3:25
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 ::
GROUP_3:26
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 ::
GROUP_3:27
((a
|^ n)
|^ b)
= ((a
|^ b)
|^ n) by
Lm4;
theorem ::
GROUP_3:28
((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 ::
GROUP_3:29
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 ::
GROUP_3:30
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;
::
GROUP_3:def3
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 ::
GROUP_3:31
Th31: x
in (A
|^ B) iff ex g, h st x
= (g
|^ h) & g
in A & h
in B;
theorem ::
GROUP_3:32
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 ::
GROUP_3:33
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 ::
GROUP_3:34
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 ::
GROUP_3:35
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 ::
GROUP_3:36
((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 ::
GROUP_3:37
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 ::
GROUP_3:38
(
{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,
TARSKI:def 2;
hence thesis by
A6,
A5;
end;
theorem ::
GROUP_3:39
(
{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 ::
GROUP_3:40
(
{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;
::
GROUP_3:def4
func A
|^ g ->
Subset of G equals (A
|^
{g});
correctness ;
::
GROUP_3:def5
func g
|^ A ->
Subset of G equals (
{g}
|^ A);
correctness ;
end
theorem ::
GROUP_3:41
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 ::
GROUP_3:42
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 ::
GROUP_3:43
(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 ::
GROUP_3:44
((A
|^ B)
|^ g)
= (A
|^ (B
* g)) by
Th35;
theorem ::
GROUP_3:45
((A
|^ g)
|^ B)
= (A
|^ (g
* B)) by
Th35;
theorem ::
GROUP_3:46
((g
|^ A)
|^ B)
= (g
|^ (A
* B)) by
Th35;
theorem ::
GROUP_3:47
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 ::
GROUP_3:48
((a
|^ A)
|^ b)
= (a
|^ (A
* b)) by
Th35;
theorem ::
GROUP_3:49
((a
|^ b)
|^ A)
= (a
|^ (b
* A))
proof
thus ((a
|^ b)
|^ A)
= ((
{a}
|^
{b})
|^ A) by
Th37
.= (a
|^ (b
* A)) by
Th35;
end;
theorem ::
GROUP_3:50
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 ::
GROUP_3:51
((A
* B)
|^ a)
c= ((A
|^ a)
* (B
|^ a)) by
Th34;
theorem ::
GROUP_3:52
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 ::
GROUP_3:53
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 ::
GROUP_3:54
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 ::
GROUP_3:55
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 ::
GROUP_3:56
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 ::
GROUP_3:57
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;
::
GROUP_3:def6
func H
|^ a ->
strict
Subgroup of G means
:
Def6: the
carrier of it
= ((
carr H)
|^ a);
existence
proof
consider H1 be
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 ::
GROUP_3:58
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 ::
GROUP_3:59
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 ::
GROUP_3:60
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 ::
GROUP_3:61
Th61: for H be
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 ::
GROUP_3:62
Th62: for H be
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 ::
GROUP_3:63
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 ::
GROUP_3:64
Th64: (
card H)
= (
card (H
|^ a))
proof
deffunc
F(
Element of G) = ($1
|^ a);
consider f be
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 be
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 ::
GROUP_3:65
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 ::
GROUP_3:66
for H be
finite
Subgroup of G holds (
card H)
= (
card (H
|^ a)) by
Th64;
theorem ::
GROUP_3:67
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 ::
GROUP_3:68
for H be
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 ::
GROUP_3:69
Th69: for G be
Group, a be
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 ::
GROUP_3:70
for H be
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 ::
GROUP_3:71
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 be
object st x
in (
Left_Cosets H) holds ex y be
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 be
Function such that
A3: (
dom f)
= (
Left_Cosets H) and
A4: for x be
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 be
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 ::
GROUP_3:72
(
Left_Cosets H) is
finite implies (
index H)
= (
index (H
|^ a))
proof
assume
A1: (
Left_Cosets H) is
finite;
then
A2: ex B be
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 ::
GROUP_3:73
Th73: G is
commutative
Group implies for H be
strict
Subgroup of G holds 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;
::
GROUP_3:def7
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 ::
GROUP_3:74
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 ::
GROUP_3:75
Th75: (a,a)
are_conjugated
proof
take (
1_ G);
thus thesis by
Th19;
end;
theorem ::
GROUP_3:76
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;
:: original:
are_conjugated
redefine
pred a,b
are_conjugated ;
reflexivity by
Th75;
symmetry by
Th76;
end
theorem ::
GROUP_3:77
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 ::
GROUP_3:78
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 ::
GROUP_3:79
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;
::
GROUP_3:def8
func
con_class a ->
Subset of G equals (a
|^ (
carr (
(Omega). G)));
correctness ;
end
theorem ::
GROUP_3:80
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 ::
GROUP_3:81
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 ::
GROUP_3:82
Th82: (a
|^ g)
in (
con_class a) by
Th80,
Th74;
theorem ::
GROUP_3:83
a
in (
con_class a) by
Th81;
theorem ::
GROUP_3:84
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 ::
GROUP_3:85
(
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 be
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 ::
GROUP_3:86
(
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 ::
GROUP_3:87
((
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;
::
GROUP_3:def9
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 ::
GROUP_3:88
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 ::
GROUP_3:89
Th89: (A,A)
are_conjugated
proof
take (
1_ G);
thus thesis by
Th52;
end;
theorem ::
GROUP_3:90
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;
:: original:
are_conjugated
redefine
pred A,B
are_conjugated ;
reflexivity by
Th89;
symmetry by
Th90;
end
theorem ::
GROUP_3:91
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 ::
GROUP_3:92
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 ::
GROUP_3:93
Th93: (A,(
carr H1))
are_conjugated implies ex H2 be
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;
::
GROUP_3:def10
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 ::
GROUP_3:94
x
in (
con_class A) iff ex B st x
= B & (A,B)
are_conjugated ;
theorem ::
GROUP_3:95
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 ::
GROUP_3:96
(A
|^ g)
in (
con_class A)
proof
(A,(A
|^ g))
are_conjugated by
Th88;
hence thesis;
end;
theorem ::
GROUP_3:97
A
in (
con_class A);
theorem ::
GROUP_3:98
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 ::
GROUP_3:99
(
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 be
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 ::
GROUP_3:100
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 ::
GROUP_3:101
G is
finite implies (
con_class A) is
finite;
definition
let G, H1, H2;
::
GROUP_3:def11
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 ::
GROUP_3:102
Th102: for H1,H2 be
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 ::
GROUP_3:103
Th103: for H1 be
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 ::
GROUP_3:104
Th104: for H1,H2 be
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;
:: original:
are_conjugated
redefine
pred H1,H2
are_conjugated ;
reflexivity by
Th103;
symmetry by
Th104;
end
theorem ::
GROUP_3:105
Th105: for H1,H2 be
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;
::
GROUP_3:def12
func
con_class H ->
Subset of (
Subgroups G) means
:
Def12: for x be
object holds x
in it iff ex H1 be
strict
Subgroup of G st x
= H1 & (H,H1)
are_conjugated ;
existence
proof
defpred
P[
set] means ex H1 be
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 be
strict
Subgroup of G st x
= H1 & (H,H1)
are_conjugated by
A1;
given H1 be
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 be
strict
Subgroup of G st $1
= H3 & (H,H3)
are_conjugated ;
let A1,A2 be
Subset of (
Subgroups G);
assume
A4: for x be
object holds x
in A1 iff
P[x];
assume
A5: for x be
object holds x
in A2 iff
P[x];
thus thesis from
XBOOLE_0:sch 2(
A4,
A5);
end;
end
theorem ::
GROUP_3:106
Th106: x
in (
con_class H) implies x is
strict
Subgroup of G
proof
assume x
in (
con_class H);
then ex H1 be
strict
Subgroup of G st x
= H1 & (H,H1)
are_conjugated by
Def12;
hence thesis;
end;
theorem ::
GROUP_3:107
Th107: for H1,H2 be
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 be
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 ::
GROUP_3:108
Th108: for H be
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 ::
GROUP_3:109
Th109: for H be
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 ::
GROUP_3:110
for H1,H2 be
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 ::
GROUP_3:111
for H1,H2 be
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 be
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 be
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 be
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 ::
GROUP_3:112
G is
finite implies (
con_class H) is
finite by
Th15,
FINSET_1: 1;
theorem ::
GROUP_3:113
Th113: for H1 be
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;
::
GROUP_3:def13
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 ::
GROUP_3:114
Th114: (
(1). G) is
normal & (
(Omega). G) is
normal by
Th67,
Th69;
theorem ::
GROUP_3:115
for N1,N2 be
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 ::
GROUP_3:116
for H be
strict
Subgroup of G holds G is
commutative
Group implies H is
normal by
Th73;
theorem ::
GROUP_3:117
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 ::
GROUP_3:118
Th118: for H be
Subgroup of G holds H is
normal
Subgroup of G iff for a holds (a
* H)
c= (H
* a)
proof
let H be
Subgroup of G;
thus H is
normal
Subgroup of G 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 ::
GROUP_3:119
Th119: for H be
Subgroup of G holds H is
normal
Subgroup of G iff for a holds (H
* a)
c= (a
* H)
proof
let H be
Subgroup of G;
thus H is
normal
Subgroup of G 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 ::
GROUP_3:120
for H be
Subgroup of G holds H is
normal
Subgroup of G iff for A holds (A
* H)
= (H
* A)
proof
let H be
Subgroup of G;
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;
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 ::
GROUP_3:121
for H be
strict
Subgroup of G holds H is
normal
Subgroup of G iff for a holds H is
Subgroup of (H
|^ a)
proof
let H be
strict
Subgroup of G;
thus H is
normal
Subgroup of G implies for a holds H is
Subgroup of (H
|^ a)
proof
assume
A1: H is
normal
Subgroup of G;
let a;
(H
|^ a)
= the multMagma of H by
A1,
Def13;
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;
theorem ::
GROUP_3:122
for H be
strict
Subgroup of G holds H is
normal
Subgroup of G iff for a holds (H
|^ a) is
Subgroup of H
proof
let H be
strict
Subgroup of G;
thus H is
normal
Subgroup of G implies for a holds (H
|^ a) is
Subgroup of H
proof
assume
A1: H is
normal
Subgroup of G;
let a;
(H
|^ a)
= the multMagma of H by
A1,
Def13;
hence thesis by
GROUP_2: 54;
end;
assume
A2: for a holds (H
|^ a) is
Subgroup of H;
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
|^ (a
" )) is
Subgroup of H by
A2;
hence (a
* H)
c= (H
* a) by
A3,
Th6;
end;
hence thesis by
Th118;
end;
theorem ::
GROUP_3:123
for H be
strict
Subgroup of G holds H is
normal
Subgroup of G iff (
con_class H)
=
{H}
proof
let H be
strict
Subgroup of G;
thus H is
normal
Subgroup of G implies (
con_class H)
=
{H}
proof
assume
A1: H is
normal
Subgroup of G;
thus (
con_class H)
c=
{H}
proof
let x be
object;
assume x
in (
con_class H);
then
consider H1 be
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,
Def13;
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 ::
GROUP_3:124
for H be
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 be
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 ::
GROUP_3:125
Th125: for N1,N2 be
strict
normal
Subgroup of G holds ((
carr N1)
* (
carr N2))
= ((
carr N2)
* (
carr N1)) by
Lm5;
theorem ::
GROUP_3:126
for N1,N2 be
strict
normal
Subgroup of G holds ex N be
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 be
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 ::
GROUP_3:127
for N be
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 ::
GROUP_3:128
for H be
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 be
finite
set st B
= (
Left_Cosets H) & (
index H)
= (
card B) by
A1,
GROUP_2: 146;
then
consider x,y be
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 be
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 be
finite
set st C
= (
Right_Cosets H) & (
index H)
= (
card C) by
A1,
GROUP_2: 146;
then
consider z1,z2 be
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 be
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;
::
GROUP_3:def14
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 ::
GROUP_3:129
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 ::
GROUP_3:130
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 be
object st x
in (
con_class A) holds ex y be
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 be
Function such that
A5: (
dom f)
= (
con_class A) and
A6: for x be
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 be
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 ::
GROUP_3:131
(
con_class A) is
finite or (
Left_Cosets (
Normalizer A)) is
finite implies ex C be
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 ::
GROUP_3:132
Th132: (
card (
con_class a))
= (
Index (
Normalizer
{a}))
proof
deffunc
F(
object) =
{$1};
consider f be
Function such that
A1: (
dom f)
= (
con_class a) and
A2: for x be
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 be
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 ::
GROUP_3:133
(
con_class a) is
finite or (
Left_Cosets (
Normalizer
{a})) is
finite implies ex C be
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;
::
GROUP_3:def15
func
Normalizer H ->
strict
Subgroup of G equals (
Normalizer (
carr H));
correctness ;
end
theorem ::
GROUP_3:134
Th134: for H be
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 ::
GROUP_3:135
Th135: for H be
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 be
strict
Subgroup of G st $1
= H1 & $2
= (
carr H1);
A1: for x be
object st x
in (
con_class H) holds ex y be
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 be
Function such that
A2: (
dom f)
= (
con_class H) and
A3: for x be
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 be
object such that
A5: y
in (
dom f) and
A6: (f
. y)
= x by
FUNCT_1:def 3;
consider H1 be
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 be
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 be
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 be
strict
Subgroup of G st x
= H1 & (f
. x)
= (
carr H1)) & ex H2 be
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 ::
GROUP_3:136
for H be
strict
Subgroup of G holds (
con_class H) is
finite or (
Left_Cosets (
Normalizer H)) is
finite implies ex C be
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 ::
GROUP_3:137
Th137: for G be
strict
Group, H be
strict
Subgroup of G holds H is
normal
Subgroup of G iff (
Normalizer H)
= G
proof
let G be
strict
Group, H be
strict
Subgroup of G;
thus H is
normal
Subgroup of G implies (
Normalizer H)
= G
proof
assume
A1: H is
normal
Subgroup of G;
now
let a be
Element of G;
(H
|^ a)
= H by
A1,
Def13;
hence a
in (
Normalizer H) by
Th134;
end;
hence thesis by
GROUP_2: 62;
end;
assume
A2: (
Normalizer H)
= G;
H is
normal
proof
let a be
Element of G;
a
in (
Normalizer H) by
A2;
then ex b be
Element of G st b
= a & (H
|^ b)
= H by
Th134;
hence thesis;
end;
hence thesis;
end;
theorem ::
GROUP_3:138
for G be
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 ::
GROUP_3:139
for G be
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;