group_2.miz
begin
reserve x for
object;
reserve G for non
empty
1-sorted;
reserve A for
Subset of G;
Lm1: x
in A implies x is
Element of G;
theorem ::
GROUP_2:1
G is
finite implies A is
finite;
reserve y,y1,y2,Y,Z for
set;
reserve k for
Nat;
reserve G for
Group;
reserve a,g,h for
Element of G;
reserve A for
Subset of G;
definition
let G, A;
::
GROUP_2:def1
func A
" ->
Subset of G equals { (g
" ) : g
in A };
coherence
proof
set F = { (g
" ) : g
in A };
F
c= the
carrier of G
proof
let x be
object;
assume x
in F;
then ex g st x
= (g
" ) & g
in A;
hence thesis;
end;
hence thesis;
end;
involutiveness
proof
let R,B be
Subset of G;
assume
A1: R
= { (g
" ) : g
in B };
thus B
c= { (g
" ) : g
in R }
proof
let a be
object;
assume
A2: a
in B;
then
reconsider a as
Element of G;
((a
" )
" )
= a & (a
" )
in R by
A1,
A2;
hence thesis;
end;
let a be
object;
assume a
in { (g
" ) : g
in R };
then
consider g such that
A3: a
= (g
" ) and
A4: g
in R;
ex h st g
= (h
" ) & h
in B by
A1,
A4;
hence thesis by
A3;
end;
end
theorem ::
GROUP_2:2
Th2: x
in (A
" ) iff ex g st x
= (g
" ) & g
in A;
theorem ::
GROUP_2:3
(
{g}
" )
=
{(g
" )}
proof
thus (
{g}
" )
c=
{(g
" )}
proof
let x be
object;
assume x
in (
{g}
" );
then
consider h such that
A1: x
= (h
" ) and
A2: h
in
{g};
h
= g by
A2,
TARSKI:def 1;
hence thesis by
A1,
TARSKI:def 1;
end;
let x be
object;
assume x
in
{(g
" )};
then
A3: x
= (g
" ) by
TARSKI:def 1;
g
in
{g} by
TARSKI:def 1;
hence thesis by
A3;
end;
theorem ::
GROUP_2:4
(
{g, h}
" )
=
{(g
" ), (h
" )}
proof
thus (
{g, h}
" )
c=
{(g
" ), (h
" )}
proof
let x be
object;
assume x
in (
{g, h}
" );
then
consider a such that
A1: x
= (a
" ) and
A2: a
in
{g, h};
a
= g or a
= h by
A2,
TARSKI:def 2;
hence thesis by
A1,
TARSKI:def 2;
end;
let x be
object;
assume x
in
{(g
" ), (h
" )};
then
A3: x
= (g
" ) or x
= (h
" ) by
TARSKI:def 2;
g
in
{g, h} & h
in
{g, h} by
TARSKI:def 2;
hence thesis by
A3;
end;
theorem ::
GROUP_2:5
((
{} the
carrier of G)
" )
=
{}
proof
thus ((
{} the
carrier of G)
" )
c=
{}
proof
let x be
object;
assume x
in ((
{} the
carrier of G)
" );
then ex a st x
= (a
" ) & a
in (
{} the
carrier of G);
hence thesis;
end;
thus thesis;
end;
theorem ::
GROUP_2:6
((
[#] the
carrier of G)
" )
= the
carrier of G
proof
thus ((
[#] the
carrier of G)
" )
c= the
carrier of G;
let x be
object;
assume x
in the
carrier of G;
then
reconsider a = x as
Element of G;
((a
" )
" )
in ((
[#] the
carrier of G)
" );
hence thesis;
end;
theorem ::
GROUP_2:7
Th7: A
<>
{} iff (A
" )
<>
{}
proof
set x = the
Element of (A
" );
thus A
<>
{} implies (A
" )
<>
{}
proof
set x = the
Element of A;
assume
A1: A
<>
{} ;
then
reconsider x as
Element of G by
Lm1;
(x
" )
in (A
" ) by
A1;
hence thesis;
end;
assume (A
" )
<>
{} ;
then ex a st x
= (a
" ) & a
in A by
Th2;
hence thesis;
end;
registration
let G;
let A be
empty
Subset of G;
cluster (A
" ) ->
empty;
coherence by
Th7;
end
registration
let G;
let A be non
empty
Subset of G;
cluster (A
" ) -> non
empty;
coherence by
Th7;
end
reserve G for non
empty
multMagma,
A,B,C for
Subset of G;
reserve a,b,g,g1,g2,h,h1,h2 for
Element of G;
definition
let G;
let A, B;
::
GROUP_2:def2
func A
* B ->
Subset of G equals { (g
* h) : g
in A & h
in B };
coherence
proof
set S = { (g
* h) : g
in A & h
in B };
S
c= the
carrier of G
proof
let x be
object;
assume x
in S;
then ex g, h st x
= (g
* h) & g
in A & h
in B;
hence thesis;
end;
hence thesis;
end;
end
definition
let G be
commutative non
empty
multMagma;
let A,B be
Subset of G;
:: original:
*
redefine
func A
* B;
commutativity
proof
let A,B be
Subset of G;
thus (A
* B)
c= (B
* A)
proof
let x be
object;
assume x
in (A
* B);
then ex g,h be
Element of G st x
= (g
* h) & g
in A & h
in B;
hence thesis;
end;
let x be
object;
assume x
in (B
* A);
then ex g,h be
Element of G st x
= (g
* h) & g
in B & h
in A;
hence thesis;
end;
end
theorem ::
GROUP_2:8
Th8: x
in (A
* B) iff ex g, h st x
= (g
* h) & g
in A & h
in B;
theorem ::
GROUP_2:9
Th9: A
<>
{} & B
<>
{} iff (A
* B)
<>
{}
proof
thus A
<>
{} & B
<>
{} implies (A
* B)
<>
{}
proof
assume
A1: A
<>
{} ;
then
reconsider x = the
Element of A as
Element of G by
TARSKI:def 3;
assume
A2: B
<>
{} ;
then
reconsider y = the
Element of B as
Element of G by
TARSKI:def 3;
(x
* y)
in (A
* B) by
A1,
A2;
hence thesis;
end;
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
Th8;
hence thesis;
end;
theorem ::
GROUP_2:10
Th10: G is
associative implies ((A
* B)
* C)
= (A
* (B
* C))
proof
assume
A1: G is
associative;
thus ((A
* B)
* C)
c= (A
* (B
* C))
proof
let x be
object;
assume x
in ((A
* B)
* C);
then
consider g, h such that
A2: x
= (g
* h) and
A3: g
in (A
* B) and
A4: h
in C;
consider g1, g2 such that
A5: g
= (g1
* g2) and
A6: g1
in A and
A7: g2
in B by
A3;
x
= (g1
* (g2
* h)) & (g2
* h)
in (B
* C) by
A1,
A2,
A4,
A5,
A7;
hence thesis by
A6;
end;
let x be
object;
assume x
in (A
* (B
* C));
then
consider g, h such that
A8: x
= (g
* h) and
A9: g
in A and
A10: h
in (B
* C);
consider g1, g2 such that
A11: h
= (g1
* g2) and
A12: g1
in B and
A13: g2
in C by
A10;
A14: (g
* g1)
in (A
* B) by
A9,
A12;
x
= ((g
* g1)
* g2) by
A1,
A8,
A11;
hence thesis by
A13,
A14;
end;
theorem ::
GROUP_2:11
for G be
Group, A,B be
Subset of G holds ((A
* B)
" )
= ((B
" )
* (A
" ))
proof
let G be
Group, A,B be
Subset of G;
thus ((A
* B)
" )
c= ((B
" )
* (A
" ))
proof
let x be
object;
assume x
in ((A
* B)
" );
then
consider g be
Element of G such that
A1: x
= (g
" ) and
A2: g
in (A
* B);
consider g1,g2 be
Element of G such that
A3: g
= (g1
* g2) and
A4: g1
in A & g2
in B by
A2;
A5: (g1
" )
in (A
" ) & (g2
" )
in (B
" ) by
A4;
x
= ((g2
" )
* (g1
" )) by
A1,
A3,
GROUP_1: 17;
hence thesis by
A5;
end;
let x be
object;
assume x
in ((B
" )
* (A
" ));
then
consider g1,g2 be
Element of G such that
A6: x
= (g1
* g2) and
A7: g1
in (B
" ) and
A8: g2
in (A
" );
consider b be
Element of G such that
A9: g2
= (b
" ) and
A10: b
in A by
A8;
consider a be
Element of G such that
A11: g1
= (a
" ) and
A12: a
in B by
A7;
A13: (b
* a)
in (A
* B) by
A12,
A10;
x
= ((b
* a)
" ) by
A6,
A11,
A9,
GROUP_1: 17;
hence thesis by
A13;
end;
theorem ::
GROUP_2:12
(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 g1, g2 such that
A1: x
= (g1
* g2) & g1
in A and
A2: g2
in (B
\/ C);
g2
in B or g2
in C by
A2,
XBOOLE_0:def 3;
then x
in (A
* B) or x
in (A
* C) by
A1;
hence thesis by
XBOOLE_0:def 3;
end;
let x be
object;
assume
A3: x
in ((A
* B)
\/ (A
* C));
now
per cases by
A3,
XBOOLE_0:def 3;
suppose x
in (A
* B);
then
consider g1, g2 such that
A4: x
= (g1
* g2) & g1
in A and
A5: g2
in B;
g2
in (B
\/ C) by
A5,
XBOOLE_0:def 3;
hence thesis by
A4;
end;
suppose x
in (A
* C);
then
consider g1, g2 such that
A6: x
= (g1
* g2) & g1
in A and
A7: g2
in C;
g2
in (B
\/ C) by
A7,
XBOOLE_0:def 3;
hence thesis by
A6;
end;
end;
hence thesis;
end;
theorem ::
GROUP_2:13
((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 g1, g2 such that
A1: x
= (g1
* g2) and
A2: g1
in (A
\/ B) and
A3: g2
in C;
g1
in A or g1
in B by
A2,
XBOOLE_0:def 3;
then x
in (A
* C) or x
in (B
* C) by
A1,
A3;
hence thesis by
XBOOLE_0:def 3;
end;
let x be
object;
assume
A4: x
in ((A
* C)
\/ (B
* C));
now
per cases by
A4,
XBOOLE_0:def 3;
suppose x
in (A
* C);
then
consider g1, g2 such that
A5: x
= (g1
* g2) and
A6: g1
in A and
A7: g2
in C;
g1
in (A
\/ B) by
A6,
XBOOLE_0:def 3;
hence thesis by
A5,
A7;
end;
suppose x
in (B
* C);
then
consider g1, g2 such that
A8: x
= (g1
* g2) and
A9: g1
in B and
A10: g2
in C;
g1
in (A
\/ B) by
A9,
XBOOLE_0:def 3;
hence thesis by
A8,
A10;
end;
end;
hence thesis;
end;
theorem ::
GROUP_2:14
(A
* (B
/\ C))
c= ((A
* B)
/\ (A
* C))
proof
let x be
object;
assume x
in (A
* (B
/\ C));
then
consider g1, g2 such that
A1: x
= (g1
* g2) & g1
in A and
A2: g2
in (B
/\ C);
g2
in C by
A2,
XBOOLE_0:def 4;
then
A3: x
in (A
* C) by
A1;
g2
in B by
A2,
XBOOLE_0:def 4;
then x
in (A
* B) by
A1;
hence thesis by
A3,
XBOOLE_0:def 4;
end;
theorem ::
GROUP_2:15
((A
/\ B)
* C)
c= ((A
* C)
/\ (B
* C))
proof
let x be
object;
assume x
in ((A
/\ B)
* C);
then
consider g1, g2 such that
A1: x
= (g1
* g2) and
A2: g1
in (A
/\ B) and
A3: g2
in C;
g1
in B by
A2,
XBOOLE_0:def 4;
then
A4: x
in (B
* C) by
A1,
A3;
g1
in A by
A2,
XBOOLE_0:def 4;
then x
in (A
* C) by
A1,
A3;
hence thesis by
A4,
XBOOLE_0:def 4;
end;
theorem ::
GROUP_2:16
Th16: ((
{} the
carrier of G)
* A)
=
{} & (A
* (
{} the
carrier of G))
=
{}
proof
A1:
now
set x = the
Element of (A
* (
{} the
carrier of G));
assume (A
* (
{} the
carrier of G))
<>
{} ;
then ex g1, g2 st x
= (g1
* g2) & g1
in A & g2
in (
{} the
carrier of G) by
Th8;
hence contradiction;
end;
now
set x = the
Element of ((
{} the
carrier of G)
* A);
assume ((
{} the
carrier of G)
* A)
<>
{} ;
then ex g1, g2 st x
= (g1
* g2) & g1
in (
{} the
carrier of G) & g2
in A by
Th8;
hence contradiction;
end;
hence thesis by
A1;
end;
theorem ::
GROUP_2:17
Th17: for G be
Group, A be
Subset of G holds A
<>
{} implies ((
[#] the
carrier of G)
* A)
= the
carrier of G & (A
* (
[#] the
carrier of G))
= the
carrier of G
proof
let G be
Group, A be
Subset of G;
set y = the
Element of A;
assume
A1: A
<>
{} ;
then
reconsider y as
Element of G by
Lm1;
thus ((
[#] the
carrier of G)
* A)
= the
carrier of G
proof
set y = the
Element of A;
reconsider y as
Element of G by
A1,
Lm1;
thus ((
[#] the
carrier of G)
* A)
c= the
carrier of G;
let x be
object;
assume x
in the
carrier of G;
then
reconsider a = x as
Element of G;
((a
* (y
" ))
* y)
= (a
* ((y
" )
* y)) by
GROUP_1:def 3
.= (a
* (
1_ G)) by
GROUP_1:def 5
.= a by
GROUP_1:def 4;
hence thesis by
A1;
end;
thus (A
* (
[#] the
carrier of G))
c= the
carrier of G;
let x be
object;
assume x
in the
carrier of G;
then
reconsider a = x as
Element of G;
(y
* ((y
" )
* a))
= ((y
* (y
" ))
* a) by
GROUP_1:def 3
.= ((
1_ G)
* a) by
GROUP_1:def 5
.= a by
GROUP_1:def 4;
hence thesis by
A1;
end;
theorem ::
GROUP_2:18
Th18: (
{g}
*
{h})
=
{(g
* h)}
proof
thus (
{g}
*
{h})
c=
{(g
* h)}
proof
let x be
object;
assume x
in (
{g}
*
{h});
then
consider g1, g2 such that
A1: x
= (g1
* g2) and
A2: g1
in
{g} & g2
in
{h};
g1
= g & g2
= h by
A2,
TARSKI:def 1;
hence thesis by
A1,
TARSKI:def 1;
end;
let x be
object;
assume x
in
{(g
* h)};
then
A3: x
= (g
* h) by
TARSKI:def 1;
g
in
{g} & h
in
{h} by
TARSKI:def 1;
hence thesis by
A3;
end;
theorem ::
GROUP_2:19
(
{g}
*
{g1, g2})
=
{(g
* g1), (g
* g2)}
proof
thus (
{g}
*
{g1, g2})
c=
{(g
* g1), (g
* g2)}
proof
let x be
object;
assume x
in (
{g}
*
{g1, g2});
then
consider h1, h2 such that
A1: x
= (h1
* h2) and
A2: h1
in
{g} and
A3: h2
in
{g1, g2};
A4: h2
= g1 or h2
= g2 by
A3,
TARSKI:def 2;
h1
= g by
A2,
TARSKI:def 1;
hence thesis by
A1,
A4,
TARSKI:def 2;
end;
let x be
object;
A5: g2
in
{g1, g2} by
TARSKI:def 2;
assume x
in
{(g
* g1), (g
* g2)};
then
A6: x
= (g
* g1) or x
= (g
* g2) by
TARSKI:def 2;
g
in
{g} & g1
in
{g1, g2} by
TARSKI:def 1,
TARSKI:def 2;
hence thesis by
A6,
A5;
end;
theorem ::
GROUP_2:20
(
{g1, g2}
*
{g})
=
{(g1
* g), (g2
* g)}
proof
thus (
{g1, g2}
*
{g})
c=
{(g1
* g), (g2
* g)}
proof
let x be
object;
assume x
in (
{g1, g2}
*
{g});
then
consider h1, h2 such that
A1: x
= (h1
* h2) and
A2: h1
in
{g1, g2} and
A3: h2
in
{g};
A4: h1
= g1 or h1
= g2 by
A2,
TARSKI:def 2;
h2
= g by
A3,
TARSKI:def 1;
hence thesis by
A1,
A4,
TARSKI:def 2;
end;
let x be
object;
A5: g2
in
{g1, g2} by
TARSKI:def 2;
assume x
in
{(g1
* g), (g2
* g)};
then
A6: x
= (g1
* g) or x
= (g2
* g) by
TARSKI:def 2;
g
in
{g} & g1
in
{g1, g2} by
TARSKI:def 1,
TARSKI:def 2;
hence thesis by
A6,
A5;
end;
theorem ::
GROUP_2:21
(
{g, h}
*
{g1, g2})
=
{(g
* g1), (g
* g2), (h
* g1), (h
* g2)}
proof
set A = (
{g, h}
*
{g1, g2});
set B =
{(g
* g1), (g
* g2), (h
* g1), (h
* g2)};
thus A
c= B
proof
let x be
object;
assume x
in A;
then
consider h1, h2 such that
A1: x
= (h1
* h2) and
A2: h1
in
{g, h} and
A3: h2
in
{g1, g2};
A4: h2
= g1 or h2
= g2 by
A3,
TARSKI:def 2;
h1
= g or h1
= h by
A2,
TARSKI:def 2;
hence thesis by
A1,
A4,
ENUMSET1:def 2;
end;
let x be
object;
A5: g1
in
{g1, g2} & g2
in
{g1, g2} by
TARSKI:def 2;
assume x
in B;
then
A6: x
= (g
* g1) or x
= (g
* g2) or x
= (h
* g1) or x
= (h
* g2) by
ENUMSET1:def 2;
g
in
{g, h} & h
in
{g, h} by
TARSKI:def 2;
hence thesis by
A6,
A5;
end;
theorem ::
GROUP_2:22
Th22: for G be
Group, A be
Subset of G holds (for g1,g2 be
Element of G st g1
in A & g2
in A holds (g1
* g2)
in A) & (for g be
Element of G st g
in A holds (g
" )
in A) implies (A
* A)
= A
proof
let G be
Group, A be
Subset of G such that
A1: for g1,g2 be
Element of G st g1
in A & g2
in A holds (g1
* g2)
in A and
A2: for g be
Element of G st g
in A holds (g
" )
in A;
thus (A
* A)
c= A
proof
let x be
object;
assume x
in (A
* A);
then ex g1,g2 be
Element of G st x
= (g1
* g2) & g1
in A & g2
in A;
hence thesis by
A1;
end;
let x be
object;
assume
A3: x
in A;
then
reconsider a = x as
Element of G;
(a
" )
in A by
A2,
A3;
then ((a
" )
* a)
in A by
A1,
A3;
then
A4: (
1_ G)
in A by
GROUP_1:def 5;
((
1_ G)
* a)
= a by
GROUP_1:def 4;
hence thesis by
A3,
A4;
end;
theorem ::
GROUP_2:23
Th23: for G be
Group, A be
Subset of G holds (for g be
Element of G st g
in A holds (g
" )
in A) implies (A
" )
= A
proof
let G be
Group, A be
Subset of G;
assume
A1: for g be
Element of G st g
in A holds (g
" )
in A;
thus (A
" )
c= A
proof
let x be
object;
assume x
in (A
" );
then ex g be
Element of G st x
= (g
" ) & g
in A;
hence thesis by
A1;
end;
let x be
object;
assume
A2: x
in A;
then
reconsider a = x as
Element of G;
A3: x
= ((a
" )
" );
(a
" )
in A by
A1,
A2;
hence thesis by
A3;
end;
theorem ::
GROUP_2:24
(for a, b st a
in A & b
in B holds (a
* b)
= (b
* a)) implies (A
* B)
= (B
* A)
proof
assume
A1: for a, b st a
in A & b
in B holds (a
* b)
= (b
* a);
thus (A
* B)
c= (B
* A)
proof
let x be
object;
assume x
in (A
* B);
then
consider a, b such that
A2: x
= (a
* b) and
A3: a
in A & b
in B;
x
= (b
* a) by
A1,
A2,
A3;
hence thesis by
A3;
end;
let x be
object;
assume x
in (B
* A);
then
consider b, a such that
A4: x
= (b
* a) and
A5: b
in B & a
in A;
x
= (a
* b) by
A1,
A4,
A5;
hence thesis by
A5;
end;
Lm2: for A be
commutative
Group, a,b be
Element of A holds (a
* b)
= (b
* a);
theorem ::
GROUP_2:25
Th25: G is
commutative
Group implies (A
* B)
= (B
* A)
proof
assume
A1: G is
commutative
Group;
thus (A
* B)
c= (B
* A)
proof
let x be
object;
assume x
in (A
* B);
then
consider g, h such that
A2: x
= (g
* h) and
A3: g
in A & h
in B;
x
= (h
* g) by
A1,
A2,
Lm2;
hence thesis by
A3;
end;
let x be
object;
assume x
in (B
* A);
then
consider g, h such that
A4: x
= (g
* h) and
A5: g
in B & h
in A;
x
= (h
* g) by
A1,
A4,
Lm2;
hence thesis by
A5;
end;
theorem ::
GROUP_2:26
for G be
commutative
Group, A,B be
Subset of G holds ((A
* B)
" )
= ((A
" )
* (B
" ))
proof
let G be
commutative
Group, A,B be
Subset of G;
thus ((A
* B)
" )
c= ((A
" )
* (B
" ))
proof
let x be
object;
assume x
in ((A
* B)
" );
then
consider g be
Element of G such that
A1: x
= (g
" ) and
A2: g
in (A
* B);
consider g1,g2 be
Element of G such that
A3: g
= (g1
* g2) and
A4: g1
in A & g2
in B by
A2;
A5: (g1
" )
in (A
" ) & (g2
" )
in (B
" ) by
A4;
x
= ((g1
" )
* (g2
" )) by
A1,
A3,
GROUP_1: 47;
hence thesis by
A5;
end;
let x be
object;
assume x
in ((A
" )
* (B
" ));
then
consider g1,g2 be
Element of G such that
A6: x
= (g1
* g2) and
A7: g1
in (A
" ) and
A8: g2
in (B
" );
consider b be
Element of G such that
A9: g2
= (b
" ) and
A10: b
in B by
A8;
consider a be
Element of G such that
A11: g1
= (a
" ) and
A12: a
in A by
A7;
A13: (a
* b)
in (A
* B) by
A12,
A10;
x
= ((a
* b)
" ) by
A6,
A11,
A9,
GROUP_1: 47;
hence thesis by
A13;
end;
definition
let G, g, A;
::
GROUP_2:def3
func g
* A ->
Subset of G equals (
{g}
* A);
correctness ;
::
GROUP_2:def4
func A
* g ->
Subset of G equals (A
*
{g});
correctness ;
end
theorem ::
GROUP_2:27
Th27: 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 g1, g2 such that
A1: x
= (g1
* g2) and
A2: g1
in
{g} and
A3: g2
in A;
g1
= 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_2:28
Th28: 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 g1, g2 such that
A1: x
= (g1
* g2) & g1
in A and
A2: g2
in
{g};
g2
= 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_2:29
G is
associative implies ((g
* A)
* B)
= (g
* (A
* B)) by
Th10;
theorem ::
GROUP_2:30
G is
associative implies ((A
* g)
* B)
= (A
* (g
* B)) by
Th10;
theorem ::
GROUP_2:31
G is
associative implies ((A
* B)
* g)
= (A
* (B
* g)) by
Th10;
theorem ::
GROUP_2:32
Th32: G is
associative implies ((g
* h)
* A)
= (g
* (h
* A))
proof
assume
A1: G is
associative;
thus ((g
* h)
* A)
= ((
{g}
*
{h})
* A) by
Th18
.= (g
* (h
* A)) by
A1,
Th10;
end;
theorem ::
GROUP_2:33
G is
associative implies ((g
* A)
* h)
= (g
* (A
* h)) by
Th10;
theorem ::
GROUP_2:34
Th34: G is
associative implies ((A
* g)
* h)
= (A
* (g
* h))
proof
assume G is
associative;
hence ((A
* g)
* h)
= (A
* (
{g}
*
{h})) by
Th10
.= (A
* (g
* h)) by
Th18;
end;
theorem ::
GROUP_2:35
((
{} the
carrier of G)
* a)
=
{} & (a
* (
{} the
carrier of G))
=
{} by
Th16;
reserve G for
Group-like non
empty
multMagma;
reserve h,g,g1,g2 for
Element of G;
reserve A for
Subset of G;
theorem ::
GROUP_2:36
for G be
Group, a be
Element of G holds ((
[#] the
carrier of G)
* a)
= the
carrier of G & (a
* (
[#] the
carrier of G))
= the
carrier of G by
Th17;
theorem ::
GROUP_2:37
Th37: ((
1_ G)
* A)
= A & (A
* (
1_ G))
= A
proof
thus ((
1_ G)
* A)
= A
proof
thus ((
1_ G)
* A)
c= A
proof
let x be
object;
assume x
in ((
1_ G)
* A);
then ex h st x
= ((
1_ G)
* h) & h
in A by
Th27;
hence thesis by
GROUP_1:def 4;
end;
let x be
object;
assume
A1: x
in A;
then
reconsider a = x as
Element of G;
((
1_ G)
* a)
= a by
GROUP_1:def 4;
hence thesis by
A1,
Th27;
end;
thus (A
* (
1_ G))
c= A
proof
let x be
object;
assume x
in (A
* (
1_ G));
then ex h st x
= (h
* (
1_ G)) & h
in A by
Th28;
hence thesis by
GROUP_1:def 4;
end;
let x be
object;
assume
A2: x
in A;
then
reconsider a = x as
Element of G;
(a
* (
1_ G))
= a by
GROUP_1:def 4;
hence thesis by
A2,
Th28;
end;
theorem ::
GROUP_2:38
G is
commutative
Group implies (g
* A)
= (A
* g) by
Th25;
definition
let G be
Group-like non
empty
multMagma;
::
GROUP_2:def5
mode
Subgroup of G ->
Group-like non
empty
multMagma means
:
Def5: the
carrier of it
c= the
carrier of G & the
multF of it
= (the
multF of G
|| the
carrier of it );
existence
proof
take G;
(
dom the
multF of G)
=
[:the
carrier of G, the
carrier of G:] by
FUNCT_2:def 1;
hence thesis by
RELAT_1: 68;
end;
end
reserve H for
Subgroup of G;
reserve h,h1,h2 for
Element of H;
theorem ::
GROUP_2:39
Th39: G is
finite implies H is
finite
proof
assume
A1: G is
finite;
the
carrier of H
c= the
carrier of G by
Def5;
hence the
carrier of H is
finite by
A1;
end;
theorem ::
GROUP_2:40
Th40: x
in H implies x
in G
proof
assume x
in H;
then
A1: x
in the
carrier of H;
the
carrier of H
c= the
carrier of G by
Def5;
hence thesis by
A1;
end;
theorem ::
GROUP_2:41
Th41: h
in G by
Th40,
STRUCT_0:def 5;
theorem ::
GROUP_2:42
Th42: h is
Element of G by
Th41,
STRUCT_0:def 5;
theorem ::
GROUP_2:43
Th43: h1
= g1 & h2
= g2 implies (h1
* h2)
= (g1
* g2)
proof
assume
A1: h1
= g1 & h2
= g2;
(h1
* h2)
= ((the
multF of G
|| the
carrier of H)
.
[h1, h2]) by
Def5;
hence thesis by
A1,
FUNCT_1: 49;
end;
registration
let G be
Group;
cluster ->
associative for
Subgroup of G;
coherence
proof
let H be
Subgroup of G;
let x,y,z be
Element of H;
(y
* z)
in the
carrier of H & the
carrier of H
c= the
carrier of G by
Def5;
then
reconsider a = x, b = y, c = z, ab = (x
* y), bc = (y
* z) as
Element of G;
thus ((x
* y)
* z)
= (ab
* c) by
Th43
.= ((a
* b)
* c) by
Th43
.= (a
* (b
* c)) by
GROUP_1:def 3
.= (a
* bc) by
Th43
.= (x
* (y
* z)) by
Th43;
end;
end
reserve G,G1,G2,G3 for
Group;
reserve a,a1,a2,b,b1,b2,g,g1,g2 for
Element of G;
reserve A,B for
Subset of G;
reserve H,H1,H2,H3 for
Subgroup of G;
reserve h,h1,h2 for
Element of H;
theorem ::
GROUP_2:44
Th44: (
1_ H)
= (
1_ G)
proof
set h = the
Element of H;
reconsider g = h, g9 = (
1_ H) as
Element of G by
Th42;
(h
* (
1_ H))
= h by
GROUP_1:def 4;
then (g
* g9)
= g by
Th43;
hence thesis by
GROUP_1: 7;
end;
theorem ::
GROUP_2:45
(
1_ H1)
= (
1_ H2)
proof
thus (
1_ H1)
= (
1_ G) by
Th44
.= (
1_ H2) by
Th44;
end;
theorem ::
GROUP_2:46
Th46: (
1_ G)
in H
proof
(
1_ H)
in H;
hence thesis by
Th44;
end;
theorem ::
GROUP_2:47
(
1_ H1)
in H2
proof
(
1_ H1)
= (
1_ G) by
Th44;
hence thesis by
Th46;
end;
theorem ::
GROUP_2:48
Th48: h
= g implies (h
" )
= (g
" )
proof
reconsider g9 = (h
" ) as
Element of G by
Th42;
A1: (h
* (h
" ))
= (
1_ H) by
GROUP_1:def 5;
assume h
= g;
then (g
* g9)
= (
1_ H) by
A1,
Th43
.= (
1_ G) by
Th44;
hence thesis by
GROUP_1: 12;
end;
theorem ::
GROUP_2:49
(
inverse_op H)
= ((
inverse_op G)
| the
carrier of H)
proof
the
carrier of H
c= the
carrier of G by
Def5;
then
A1: (the
carrier of G
/\ the
carrier of H)
= the
carrier of H by
XBOOLE_1: 28;
A2:
now
let x be
object;
assume x
in (
dom (
inverse_op H));
then
reconsider a = x as
Element of H;
reconsider b = a as
Element of G by
Th42;
thus ((
inverse_op H)
. x)
= (a
" ) by
GROUP_1:def 6
.= (b
" ) by
Th48
.= ((
inverse_op G)
. x) by
GROUP_1:def 6;
end;
(
dom (
inverse_op H))
= the
carrier of H & (
dom (
inverse_op G))
= the
carrier of G by
FUNCT_2:def 1;
hence thesis by
A1,
A2,
FUNCT_1: 46;
end;
theorem ::
GROUP_2:50
Th50: g1
in H & g2
in H implies (g1
* g2)
in H
proof
assume g1
in H & g2
in H;
then
reconsider h1 = g1, h2 = g2 as
Element of H;
(h1
* h2)
in H;
hence thesis by
Th43;
end;
theorem ::
GROUP_2:51
Th51: g
in H implies (g
" )
in H
proof
assume g
in H;
then
reconsider h = g as
Element of H;
(h
" )
in H;
hence thesis by
Th48;
end;
registration
let G;
cluster
strict for
Subgroup of G;
existence
proof
set H =
multMagma (# the
carrier of G, the
multF of G #);
H is
Group-like
proof
reconsider t = (
1_ G) as
Element of H;
take t;
let a be
Element of H;
reconsider x = a as
Element of G;
thus (a
* t)
= (x
* (
1_ G))
.= a by
GROUP_1:def 4;
thus (t
* a)
= ((
1_ G)
* x)
.= a by
GROUP_1:def 4;
reconsider s = (x
" ) as
Element of H;
take s;
thus (a
* s)
= (x
* (x
" ))
.= t by
GROUP_1:def 5;
thus (s
* a)
= ((x
" )
* x)
.= t by
GROUP_1:def 5;
end;
then
reconsider H as
Group-like non
empty
multMagma;
the
multF of H
= (the
multF of G
|| the
carrier of H) by
RELSET_1: 19;
then H is
Subgroup of G by
Def5;
hence thesis;
end;
end
theorem ::
GROUP_2:52
Th52: A
<>
{} & (for g1, g2 st g1
in A & g2
in A holds (g1
* g2)
in A) & (for g st g
in A holds (g
" )
in A) implies ex H be
strict
Subgroup of G st the
carrier of H
= A
proof
assume that
A1: A
<>
{} and
A2: for g1, g2 st g1
in A & g2
in A holds (g1
* g2)
in A and
A3: for g st g
in A holds (g
" )
in A;
reconsider D = A as non
empty
set by
A1;
set o = (the
multF of G
|| A);
A4: (
dom o)
= ((
dom the
multF of G)
/\
[:A, A:]) by
RELAT_1: 61;
(
dom the
multF of G)
=
[:the
carrier of G, the
carrier of G:] by
FUNCT_2:def 1;
then
A5: (
dom o)
=
[:A, A:] by
A4,
XBOOLE_1: 28;
(
rng o)
c= A
proof
let x be
object;
assume x
in (
rng o);
then
consider y be
object such that
A6: y
in (
dom o) and
A7: (o
. y)
= x by
FUNCT_1:def 3;
consider y1,y2 be
object such that
A8:
[y1, y2]
= y by
A4,
A6,
RELAT_1:def 1;
A9: y1
in A & y2
in A by
A5,
A6,
A8,
ZFMISC_1: 87;
reconsider y1, y2 as
Element of G by
A4,
A6,
A8,
ZFMISC_1: 87;
x
= (y1
* y2) by
A6,
A7,
A8,
FUNCT_1: 47;
hence thesis by
A2,
A9;
end;
then
reconsider o as
BinOp of D by
A5,
FUNCT_2:def 1,
RELSET_1: 4;
set H =
multMagma (# D, o #);
A10:
now
let g1, g2;
let h1,h2 be
Element of H;
A11: (h1
* h2)
= ((the
multF of G
|| A)
.
[h1, h2]);
assume g1
= h1 & g2
= h2;
hence (g1
* g2)
= (h1
* h2) by
A11,
FUNCT_1: 49;
end;
H is
Group-like
proof
set a = the
Element of H;
reconsider x = a as
Element of G by
Lm1;
(x
" )
in A by
A3;
then (x
* (x
" ))
in A by
A2;
then
reconsider t = (
1_ G) as
Element of H by
GROUP_1:def 5;
take t;
let a be
Element of H;
reconsider x = a as
Element of G by
Lm1;
thus (a
* t)
= (x
* (
1_ G)) by
A10
.= a by
GROUP_1:def 4;
thus (t
* a)
= ((
1_ G)
* x) by
A10
.= a by
GROUP_1:def 4;
reconsider s = (x
" ) as
Element of H by
A3;
take s;
thus (a
* s)
= (x
* (x
" )) by
A10
.= t by
GROUP_1:def 5;
thus (s
* a)
= ((x
" )
* x) by
A10
.= t by
GROUP_1:def 5;
end;
then
reconsider H as
Group-like non
empty
multMagma;
reconsider H as
strict
Subgroup of G by
Def5;
take H;
thus thesis;
end;
theorem ::
GROUP_2:53
Th53: G is
commutative
Group implies H is
commutative
proof
assume
A1: G is
commutative
Group;
thus for h1, h2 holds (h1
* h2)
= (h2
* h1)
proof
let h1, h2;
reconsider g1 = h1, g2 = h2 as
Element of G by
Th42;
thus (h1
* h2)
= (g1
* g2) by
Th43
.= (g2
* g1) by
A1,
Lm2
.= (h2
* h1) by
Th43;
end;
end;
registration
let G be
commutative
Group;
cluster ->
commutative for
Subgroup of G;
coherence by
Th53;
end
theorem ::
GROUP_2:54
Th54: G is
Subgroup of G
proof
(
dom the
multF of G)
=
[:the
carrier of G, the
carrier of G:] by
FUNCT_2:def 1;
hence the
carrier of G
c= the
carrier of G & the
multF of G
= (the
multF of G
|| the
carrier of G) by
RELAT_1: 68;
end;
theorem ::
GROUP_2:55
Th55: G1 is
Subgroup of G2 & G2 is
Subgroup of G1 implies the multMagma of G1
= the multMagma of G2
proof
assume that
A1: G1 is
Subgroup of G2 and
A2: G2 is
Subgroup of G1;
set g = the
multF of G2;
set f = the
multF of G1;
set B = the
carrier of G2;
set A = the
carrier of G1;
A3: A
c= B & B
c= A by
A1,
A2,
Def5;
then
A4: A
= B;
f
= (g
|| A) by
A1,
Def5
.= ((f
|| B)
|| A) by
A2,
Def5
.= (f
|| B) by
A4,
RELAT_1: 72
.= g by
A2,
Def5;
hence thesis by
A3,
XBOOLE_0:def 10;
end;
theorem ::
GROUP_2:56
Th56: G1 is
Subgroup of G2 & G2 is
Subgroup of G3 implies G1 is
Subgroup of G3
proof
assume that
A1: G1 is
Subgroup of G2 and
A2: G2 is
Subgroup of G3;
set h = the
multF of G3;
set C = the
carrier of G3;
set B = the
carrier of G2;
set A = the
carrier of G1;
A3: A
c= B by
A1,
Def5;
then
A4:
[:A, A:]
c=
[:B, B:] by
ZFMISC_1: 96;
B
c= C by
A2,
Def5;
then
A5: A
c= C by
A3;
the
multF of G1
= (the
multF of G2
|| A) by
A1,
Def5
.= ((h
|| B)
|| A) by
A2,
Def5
.= (h
|| A) by
A4,
FUNCT_1: 51;
hence thesis by
A5,
Def5;
end;
theorem ::
GROUP_2:57
Th57: the
carrier of H1
c= the
carrier of H2 implies H1 is
Subgroup of H2
proof
set A = the
carrier of H1;
set B = the
carrier of H2;
set h = the
multF of G;
assume
A1: the
carrier of H1
c= the
carrier of H2;
hence the
carrier of H1
c= the
carrier of H2;
A2:
[:A, A:]
c=
[:B, B:] by
A1,
ZFMISC_1: 96;
the
multF of H1
= (h
|| A) & the
multF of H2
= (h
|| B) by
Def5;
hence thesis by
A2,
FUNCT_1: 51;
end;
theorem ::
GROUP_2:58
Th58: (for g st g
in H1 holds g
in H2) implies H1 is
Subgroup of H2
proof
assume
A1: for g st g
in H1 holds g
in H2;
the
carrier of H1
c= the
carrier of H2
proof
let x be
object;
assume x
in the
carrier of H1;
then
reconsider g = x as
Element of H1;
reconsider g as
Element of G by
Th42;
g
in H1;
then g
in H2 by
A1;
hence thesis;
end;
hence thesis by
Th57;
end;
theorem ::
GROUP_2:59
Th59: the
carrier of H1
= the
carrier of H2 implies the multMagma of H1
= the multMagma of H2
proof
assume the
carrier of H1
= the
carrier of H2;
then H1 is
Subgroup of H2 & H2 is
Subgroup of H1 by
Th57;
hence thesis by
Th55;
end;
theorem ::
GROUP_2:60
Th60: (for g holds g
in H1 iff g
in H2) implies the multMagma of H1
= the multMagma of H2
proof
assume for g holds g
in H1 iff g
in H2;
then H1 is
Subgroup of H2 & H2 is
Subgroup of H1 by
Th58;
hence thesis by
Th55;
end;
definition
let G;
let H1,H2 be
strict
Subgroup of G;
:: original:
=
redefine
::
GROUP_2:def6
pred H1
= H2 means for g holds g
in H1 iff g
in H2;
compatibility by
Th60;
end
theorem ::
GROUP_2:61
Th61: for G be
Group, H be
Subgroup of G st the
carrier of G
c= the
carrier of H holds the multMagma of H
= the multMagma of G
proof
let G be
Group, H be
Subgroup of G;
assume
A1: the
carrier of G
c= the
carrier of H;
A2: G is
Subgroup of G by
Th54;
the
carrier of H
c= the
carrier of G by
Def5;
then the
carrier of G
= the
carrier of H by
A1;
hence thesis by
A2,
Th59;
end;
theorem ::
GROUP_2:62
Th62: (for g be
Element of G holds g
in H) implies the multMagma of H
= the multMagma of G
proof
assume for g be
Element of G holds g
in H;
then
A1: for g be
Element of G holds (g
in H implies g
in G) & (g
in G implies g
in H);
G is
Subgroup of G by
Th54;
hence thesis by
A1,
Th60;
end;
definition
let G;
::
GROUP_2:def7
func
(1). G ->
strict
Subgroup of G means
:
Def7: the
carrier of it
=
{(
1_ G)};
existence
proof
A1:
now
let g;
assume g
in
{(
1_ G)};
then g
= (
1_ G) by
TARSKI:def 1;
then (g
" )
= (
1_ G) by
GROUP_1: 8;
hence (g
" )
in
{(
1_ G)} by
TARSKI:def 1;
end;
now
let g1, g2;
assume g1
in
{(
1_ G)} & g2
in
{(
1_ G)};
then g1
= (
1_ G) & g2
= (
1_ G) by
TARSKI:def 1;
then (g1
* g2)
= (
1_ G) by
GROUP_1:def 4;
hence (g1
* g2)
in
{(
1_ G)} by
TARSKI:def 1;
end;
hence thesis by
A1,
Th52;
end;
uniqueness by
Th59;
end
definition
let G;
::
GROUP_2:def8
func
(Omega). G ->
strict
Subgroup of G equals the multMagma of G;
coherence
proof
set H = the multMagma of G;
H is
Group-like
proof
consider e9 be
Element of G such that
A1: for h be
Element of G holds (h
* e9)
= h & (e9
* h)
= h & ex g be
Element of G st (h
* g)
= e9 & (g
* h)
= e9 by
GROUP_1:def 2;
reconsider e = e9 as
Element of H;
take e;
let h be
Element of H;
reconsider h9 = h as
Element of G;
consider g9 be
Element of G such that
A2: (h9
* g9)
= e9 & (g9
* h9)
= e9 by
A1;
(h9
* e9)
= h9 & (e9
* h9)
= h9 by
A1;
hence (h
* e)
= h & (e
* h)
= h;
reconsider g = g9 as
Element of H;
take g;
thus thesis by
A2;
end;
then
reconsider H as
Group-like non
empty
multMagma;
(
dom the
multF of G)
=
[:the
carrier of G, the
carrier of G:] by
FUNCT_2:def 1;
then the
multF of H
= (the
multF of G
|| the
carrier of H) by
RELAT_1: 68;
hence thesis by
Def5;
end;
projectivity ;
end
theorem ::
GROUP_2:63
Th63: (
(1). H)
= (
(1). G)
proof
A1: (
1_ H)
= (
1_ G) by
Th44;
(
(1). H) is
Subgroup of G & the
carrier of (
(1). H)
=
{(
1_ H)} by
Def7,
Th56;
hence thesis by
A1,
Def7;
end;
theorem ::
GROUP_2:64
(
(1). H1)
= (
(1). H2)
proof
thus (
(1). H1)
= (
(1). G) by
Th63
.= (
(1). H2) by
Th63;
end;
theorem ::
GROUP_2:65
Th65: (
(1). G) is
Subgroup of H
proof
(
(1). G)
= (
(1). H) by
Th63;
hence thesis;
end;
theorem ::
GROUP_2:66
for G be
strict
Group, H be
Subgroup of G holds H is
Subgroup of (
(Omega). G);
theorem ::
GROUP_2:67
for G be
strict
Group holds G is
Subgroup of (
(Omega). G);
theorem ::
GROUP_2:68
Th68: (
(1). G) is
finite
proof
the
carrier of (
(1). G)
=
{(
1_ G)} by
Def7;
hence thesis;
end;
registration
let G;
cluster (
(1). G) ->
finite;
coherence by
Th68;
cluster
strict
finite for
Subgroup of G;
existence
proof
take (
(1). G);
thus thesis;
end;
end
registration
cluster
strict
finite for
Group;
existence
proof
set G = the
Group;
take (
(1). G);
thus thesis;
end;
end
registration
let G be
finite
Group;
cluster ->
finite for
Subgroup of G;
coherence by
Th39;
end
theorem ::
GROUP_2:69
Th69: (
card (
(1). G))
= 1
proof
the
carrier of (
(1). G)
=
{(
1_ G)} by
Def7;
hence thesis by
CARD_1: 30;
end;
theorem ::
GROUP_2:70
Th70: for H be
strict
finite
Subgroup of G holds (
card H)
= 1 implies H
= (
(1). G)
proof
let H be
strict
finite
Subgroup of G;
assume (
card H)
= 1;
then
consider x be
object such that
A1: the
carrier of H
=
{x} by
CARD_2: 42;
(
1_ G)
in H by
Th46;
then (
1_ G)
in the
carrier of H;
then x
= (
1_ G) by
A1,
TARSKI:def 1;
hence thesis by
A1,
Def7;
end;
theorem ::
GROUP_2:71
(
card H)
c= (
card G) by
Def5,
CARD_1: 11;
theorem ::
GROUP_2:72
for G be
finite
Group, H be
Subgroup of G holds (
card H)
<= (
card G) by
Def5,
NAT_1: 43;
theorem ::
GROUP_2:73
for G be
finite
Group, H be
Subgroup of G holds (
card G)
= (
card H) implies the multMagma of H
= the multMagma of G
proof
let G be
finite
Group, H be
Subgroup of G;
assume
A1: (
card G)
= (
card H);
A2: the
carrier of H
c= the
carrier of G by
Def5;
the
carrier of H
= the
carrier of G
proof
assume the
carrier of H
<> the
carrier of G;
then the
carrier of H
c< the
carrier of G by
A2;
hence thesis by
A1,
CARD_2: 48;
end;
hence thesis by
Th61;
end;
definition
let G, H;
::
GROUP_2:def9
func
carr (H) ->
Subset of G equals the
carrier of H;
coherence by
Def5;
end
theorem ::
GROUP_2:74
Th74: g1
in (
carr H) & g2
in (
carr H) implies (g1
* g2)
in (
carr H)
proof
assume g1
in (
carr H) & g2
in (
carr H);
then g1
in H & g2
in H;
then (g1
* g2)
in H by
Th50;
hence thesis;
end;
theorem ::
GROUP_2:75
Th75: g
in (
carr H) implies (g
" )
in (
carr H)
proof
assume g
in (
carr H);
then g
in H;
then (g
" )
in H by
Th51;
hence thesis;
end;
theorem ::
GROUP_2:76
((
carr H)
* (
carr H))
= (
carr H)
proof
A1: g
in (
carr H) implies (g
" )
in (
carr H) by
Th75;
g1
in (
carr H) & g2
in (
carr H) implies (g1
* g2)
in (
carr H) by
Th74;
hence thesis by
A1,
Th22;
end;
theorem ::
GROUP_2:77
((
carr H)
" )
= (
carr H)
proof
g
in (
carr H) implies (g
" )
in (
carr H) by
Th75;
hence thesis by
Th23;
end;
theorem ::
GROUP_2:78
Th78: (((
carr H1)
* (
carr H2))
= ((
carr H2)
* (
carr H1)) implies ex H be
strict
Subgroup of G st the
carrier of H
= ((
carr H1)
* (
carr H2))) & ((ex H st the
carrier of H
= ((
carr H1)
* (
carr H2))) implies ((
carr H1)
* (
carr H2))
= ((
carr H2)
* (
carr H1)))
proof
thus ((
carr H1)
* (
carr H2))
= ((
carr H2)
* (
carr H1)) implies ex H be
strict
Subgroup of G st the
carrier of H
= ((
carr H1)
* (
carr H2))
proof
assume
A1: ((
carr H1)
* (
carr H2))
= ((
carr H2)
* (
carr H1));
A2:
now
let g;
assume
A3: g
in ((
carr H1)
* (
carr H2));
then
consider a, b such that
A4: g
= (a
* b) and a
in (
carr H1) and b
in (
carr H2);
consider b1, a1 such that
A5: (a
* b)
= (b1
* a1) and
A6: b1
in (
carr H2) & a1
in (
carr H1) by
A1,
A3,
A4;
A7: (a1
" )
in (
carr H1) & (b1
" )
in (
carr H2) by
A6,
Th75;
(g
" )
= ((a1
" )
* (b1
" )) by
A4,
A5,
GROUP_1: 17;
hence (g
" )
in ((
carr H1)
* (
carr H2)) by
A7;
end;
A8:
now
let g1, g2;
assume that
A9: g1
in ((
carr H1)
* (
carr H2)) and
A10: g2
in ((
carr H1)
* (
carr H2));
consider a1, b1 such that
A11: g1
= (a1
* b1) and
A12: a1
in (
carr H1) and
A13: b1
in (
carr H2) by
A9;
consider a2, b2 such that
A14: g2
= (a2
* b2) and
A15: a2
in (
carr H1) and
A16: b2
in (
carr H2) by
A10;
(b1
* a2)
in ((
carr H1)
* (
carr H2)) by
A1,
A13,
A15;
then
consider a, b such that
A17: (b1
* a2)
= (a
* b) and
A18: a
in (
carr H1) and
A19: b
in (
carr H2);
A20: (b
* b2)
in (
carr H2) by
A16,
A19,
Th74;
(g1
* g2)
= (((a1
* b1)
* a2)
* b2) by
A11,
A14,
GROUP_1:def 3
.= ((a1
* (b1
* a2))
* b2) by
GROUP_1:def 3;
then
A21: (g1
* g2)
= (((a1
* a)
* b)
* b2) by
A17,
GROUP_1:def 3
.= ((a1
* a)
* (b
* b2)) by
GROUP_1:def 3;
(a1
* a)
in (
carr H1) by
A12,
A18,
Th74;
hence (g1
* g2)
in ((
carr H1)
* (
carr H2)) by
A21,
A20;
end;
((
carr H1)
* (
carr H2))
<>
{} by
Th9;
hence thesis by
A8,
A2,
Th52;
end;
given H such that
A22: the
carrier of H
= ((
carr H1)
* (
carr H2));
thus ((
carr H1)
* (
carr H2))
c= ((
carr H2)
* (
carr H1))
proof
let x be
object;
assume
A23: x
in ((
carr H1)
* (
carr H2));
then
reconsider y = x as
Element of G;
(y
" )
in (
carr H) by
A22,
A23,
Th75;
then
consider a, b such that
A24: (y
" )
= (a
* b) and
A25: a
in (
carr H1) & b
in (
carr H2) by
A22;
A26: y
= ((y
" )
" )
.= ((b
" )
* (a
" )) by
A24,
GROUP_1: 17;
(a
" )
in (
carr H1) & (b
" )
in (
carr H2) by
A25,
Th75;
hence thesis by
A26;
end;
let x be
object;
assume
A27: x
in ((
carr H2)
* (
carr H1));
then
reconsider y = x as
Element of G;
consider a, b such that
A28: x
= (a
* b) & a
in (
carr H2) and
A29: b
in (
carr H1) by
A27;
now
A30: (b
" )
in (
carr H1) by
A29,
Th75;
assume
A31: not (y
" )
in (
carr H);
(y
" )
= ((b
" )
* (a
" )) & (a
" )
in (
carr H2) by
A28,
Th75,
GROUP_1: 17;
hence contradiction by
A22,
A31,
A30;
end;
then ((y
" )
" )
in (
carr H) by
Th75;
hence thesis by
A22;
end;
theorem ::
GROUP_2:79
G is
commutative
Group implies ex H be
strict
Subgroup of G st the
carrier of H
= ((
carr H1)
* (
carr H2))
proof
assume G is
commutative
Group;
then ((
carr H1)
* (
carr H2))
= ((
carr H2)
* (
carr H1)) by
Th25;
hence thesis by
Th78;
end;
definition
let G, H1, H2;
::
GROUP_2:def10
func H1
/\ H2 ->
strict
Subgroup of G means
:
Def10: the
carrier of it
= ((
carr H1)
/\ (
carr H2));
existence
proof
set A = ((
carr H1)
/\ (
carr H2));
(
1_ G)
in H2 by
Th46;
then
A1: (
1_ G)
in the
carrier of H2;
A2:
now
let g1, g2;
assume
A3: g1
in A & g2
in A;
then g1
in (
carr H2) & g2
in (
carr H2) by
XBOOLE_0:def 4;
then
A4: (g1
* g2)
in (
carr H2) by
Th74;
g1
in (
carr H1) & g2
in (
carr H1) by
A3,
XBOOLE_0:def 4;
then (g1
* g2)
in (
carr H1) by
Th74;
hence (g1
* g2)
in A by
A4,
XBOOLE_0:def 4;
end;
A5:
now
let g;
assume
A6: g
in A;
then g
in (
carr H2) by
XBOOLE_0:def 4;
then
A7: (g
" )
in (
carr H2) by
Th75;
g
in (
carr H1) by
A6,
XBOOLE_0:def 4;
then (g
" )
in (
carr H1) by
Th75;
hence (g
" )
in A by
A7,
XBOOLE_0:def 4;
end;
(
1_ G)
in H1 by
Th46;
then (
1_ G)
in the
carrier of H1;
then A
<>
{} by
A1,
XBOOLE_0:def 4;
hence thesis by
A2,
A5,
Th52;
end;
uniqueness by
Th59;
end
theorem ::
GROUP_2:80
Th80: (for H be
Subgroup of G st H
= (H1
/\ H2) holds the
carrier of H
= (the
carrier of H1
/\ the
carrier of H2)) & for H be
strict
Subgroup of G holds the
carrier of H
= (the
carrier of H1
/\ the
carrier of H2) implies H
= (H1
/\ H2)
proof
A1: the
carrier of H1
= (
carr H1) & the
carrier of H2
= (
carr H2);
thus for H be
Subgroup of G st H
= (H1
/\ H2) holds the
carrier of H
= (the
carrier of H1
/\ the
carrier of H2)
proof
let H be
Subgroup of G;
assume H
= (H1
/\ H2);
hence the
carrier of H
= ((
carr H1)
/\ (
carr H2)) by
Def10
.= (the
carrier of H1
/\ the
carrier of H2);
end;
let H be
strict
Subgroup of G;
assume the
carrier of H
= (the
carrier of H1
/\ the
carrier of H2);
hence thesis by
A1,
Def10;
end;
theorem ::
GROUP_2:81
(
carr (H1
/\ H2))
= ((
carr H1)
/\ (
carr H2)) by
Def10;
theorem ::
GROUP_2:82
Th82: x
in (H1
/\ H2) iff x
in H1 & x
in H2
proof
thus x
in (H1
/\ H2) implies x
in H1 & x
in H2
proof
assume x
in (H1
/\ H2);
then x
in the
carrier of (H1
/\ H2);
then x
in ((
carr H1)
/\ (
carr H2)) by
Def10;
then x
in (
carr H1) & x
in (
carr H2) by
XBOOLE_0:def 4;
hence thesis;
end;
assume x
in H1 & x
in H2;
then x
in (
carr H2) & x
in (
carr H1);
then x
in ((
carr H1)
/\ (
carr H2)) by
XBOOLE_0:def 4;
then x
in (
carr (H1
/\ H2)) by
Def10;
hence thesis;
end;
theorem ::
GROUP_2:83
for H be
strict
Subgroup of G holds (H
/\ H)
= H
proof
let H be
strict
Subgroup of G;
the
carrier of (H
/\ H)
= ((
carr H)
/\ (
carr H)) by
Def10
.= the
carrier of H;
hence thesis by
Th59;
end;
definition
let G, H1, H2;
:: original:
/\
redefine
func H1
/\ H2;
commutativity
proof
let H1, H2;
the
carrier of (H1
/\ H2)
= ((
carr H2)
/\ (
carr H1)) by
Def10
.= the
carrier of (H2
/\ H1) by
Def10;
hence thesis by
Th59;
end;
end
theorem ::
GROUP_2:84
((H1
/\ H2)
/\ H3)
= (H1
/\ (H2
/\ H3))
proof
the
carrier of ((H1
/\ H2)
/\ H3)
= ((
carr (H1
/\ H2))
/\ (
carr H3)) by
Def10
.= (((
carr H1)
/\ (
carr H2))
/\ (
carr H3)) by
Def10
.= ((
carr H1)
/\ ((
carr H2)
/\ (
carr H3))) by
XBOOLE_1: 16
.= ((
carr H1)
/\ (
carr (H2
/\ H3))) by
Def10
.= the
carrier of (H1
/\ (H2
/\ H3)) by
Def10;
hence thesis by
Th59;
end;
Lm3: for H1 be
Subgroup of G holds H1 is
Subgroup of H2 iff the multMagma of (H1
/\ H2)
= the multMagma of H1
proof
let H1 be
Subgroup of G;
thus H1 is
Subgroup of H2 implies the multMagma of (H1
/\ H2)
= the multMagma of H1
proof
assume H1 is
Subgroup of H2;
then
A1: the
carrier of H1
c= the
carrier of H2 by
Def5;
the
carrier of (H1
/\ H2)
= ((
carr H1)
/\ (
carr H2)) by
Def10;
hence thesis by
A1,
Th59,
XBOOLE_1: 28;
end;
assume the multMagma of (H1
/\ H2)
= the multMagma of H1;
then the
carrier of H1
= ((
carr H1)
/\ (
carr H2)) by
Def10
.= (the
carrier of H1
/\ the
carrier of H2);
hence thesis by
Th57,
XBOOLE_1: 17;
end;
theorem ::
GROUP_2:85
((
(1). G)
/\ H)
= (
(1). G) & (H
/\ (
(1). G))
= (
(1). G)
proof
A1: (
(1). G) is
Subgroup of H by
Th65;
hence ((
(1). G)
/\ H)
= (
(1). G) by
Lm3;
thus thesis by
A1,
Lm3;
end;
theorem ::
GROUP_2:86
for G be
strict
Group, H be
strict
Subgroup of G holds (H
/\ (
(Omega). G))
= H & ((
(Omega). G)
/\ H)
= H by
Lm3;
theorem ::
GROUP_2:87
for G be
strict
Group holds ((
(Omega). G)
/\ (
(Omega). G))
= G by
Lm3;
Lm4: (H1
/\ H2) is
Subgroup of H1
proof
the
carrier of (H1
/\ H2)
= (the
carrier of H1
/\ the
carrier of H2) by
Th80;
hence thesis by
Th57,
XBOOLE_1: 17;
end;
theorem ::
GROUP_2:88
(H1
/\ H2) is
Subgroup of H1 & (H1
/\ H2) is
Subgroup of H2 by
Lm4;
theorem ::
GROUP_2:89
for H1 be
Subgroup of G holds H1 is
Subgroup of H2 iff the multMagma of (H1
/\ H2)
= the multMagma of H1 by
Lm3;
theorem ::
GROUP_2:90
H1 is
Subgroup of H2 implies (H1
/\ H3) is
Subgroup of H2
proof
assume
A1: H1 is
Subgroup of H2;
(H1
/\ H3) is
Subgroup of H1 by
Lm4;
hence thesis by
A1,
Th56;
end;
theorem ::
GROUP_2:91
H1 is
Subgroup of H2 & H1 is
Subgroup of H3 implies H1 is
Subgroup of (H2
/\ H3)
proof
assume
A1: H1 is
Subgroup of H2 & H1 is
Subgroup of H3;
now
let g;
assume g
in H1;
then g
in H2 & g
in H3 by
A1,
Th40;
hence g
in (H2
/\ H3) by
Th82;
end;
hence thesis by
Th58;
end;
theorem ::
GROUP_2:92
H1 is
Subgroup of H2 implies (H1
/\ H3) is
Subgroup of (H2
/\ H3)
proof
assume H1 is
Subgroup of H2;
then the
carrier of H1
c= the
carrier of H2 by
Def5;
then (the
carrier of H1
/\ the
carrier of H3)
c= (the
carrier of H2
/\ the
carrier of H3) by
XBOOLE_1: 26;
then the
carrier of (H1
/\ H3)
c= (the
carrier of H2
/\ the
carrier of H3) by
Th80;
then the
carrier of (H1
/\ H3)
c= the
carrier of (H2
/\ H3) by
Th80;
hence thesis by
Th57;
end;
theorem ::
GROUP_2:93
H1 is
finite or H2 is
finite implies (H1
/\ H2) is
finite
proof
assume
A1: H1 is
finite or H2 is
finite;
(H1
/\ H2) is
Subgroup of H1 & (H1
/\ H2) is
Subgroup of H2 by
Lm4;
hence thesis by
A1;
end;
definition
let G, H, A;
::
GROUP_2:def11
func A
* H ->
Subset of G equals (A
* (
carr H));
correctness ;
::
GROUP_2:def12
func H
* A ->
Subset of G equals ((
carr H)
* A);
correctness ;
end
theorem ::
GROUP_2:94
x
in (A
* H) iff ex g1, g2 st x
= (g1
* g2) & g1
in A & g2
in H
proof
thus x
in (A
* H) implies ex g1, g2 st x
= (g1
* g2) & g1
in A & g2
in H
proof
assume x
in (A
* H);
then
consider g1, g2 such that
A1: x
= (g1
* g2) & g1
in A and
A2: g2
in (
carr H);
g2
in H by
A2;
hence thesis by
A1;
end;
given g1, g2 such that
A3: x
= (g1
* g2) & g1
in A and
A4: g2
in H;
g2
in (
carr H) by
A4;
hence thesis by
A3;
end;
theorem ::
GROUP_2:95
x
in (H
* A) iff ex g1, g2 st x
= (g1
* g2) & g1
in H & g2
in A
proof
thus x
in (H
* A) implies ex g1, g2 st x
= (g1
* g2) & g1
in H & g2
in A
proof
assume x
in (H
* A);
then
consider g1, g2 such that
A1: x
= (g1
* g2) and
A2: g1
in (
carr H) and
A3: g2
in A;
g1
in H by
A2;
hence thesis by
A1,
A3;
end;
given g1, g2 such that
A4: x
= (g1
* g2) and
A5: g1
in H and
A6: g2
in A;
g1
in (
carr H) by
A5;
hence thesis by
A4,
A6;
end;
theorem ::
GROUP_2:96
((A
* B)
* H)
= (A
* (B
* H)) by
Th10;
theorem ::
GROUP_2:97
((A
* H)
* B)
= (A
* (H
* B)) by
Th10;
theorem ::
GROUP_2:98
((H
* A)
* B)
= (H
* (A
* B)) by
Th10;
theorem ::
GROUP_2:99
((A
* H1)
* H2)
= (A
* (H1
* (
carr H2))) by
Th10;
theorem ::
GROUP_2:100
((H1
* A)
* H2)
= (H1
* (A
* H2)) by
Th10;
theorem ::
GROUP_2:101
((H1
* (
carr H2))
* A)
= (H1
* (H2
* A)) by
Th10;
theorem ::
GROUP_2:102
G is
commutative
Group implies (A
* H)
= (H
* A) by
Th25;
definition
let G, H, a;
::
GROUP_2:def13
func a
* H ->
Subset of G equals (a
* (
carr H));
correctness ;
::
GROUP_2:def14
func H
* a ->
Subset of G equals ((
carr H)
* a);
correctness ;
end
theorem ::
GROUP_2:103
Th103: x
in (a
* H) iff ex g st x
= (a
* g) & g
in H
proof
thus x
in (a
* H) implies ex g st x
= (a
* g) & g
in H
proof
assume x
in (a
* H);
then
consider g such that
A1: x
= (a
* g) & g
in (
carr H) by
Th27;
take g;
thus thesis by
A1;
end;
given g such that
A2: x
= (a
* g) and
A3: g
in H;
g
in (
carr H) by
A3;
hence thesis by
A2,
Th27;
end;
theorem ::
GROUP_2:104
Th104: 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
consider g such that
A1: x
= (g
* a) & g
in (
carr H) by
Th28;
take g;
thus thesis by
A1;
end;
given g such that
A2: x
= (g
* a) and
A3: g
in H;
g
in (
carr H) by
A3;
hence thesis by
A2,
Th28;
end;
theorem ::
GROUP_2:105
((a
* b)
* H)
= (a
* (b
* H)) by
Th32;
theorem ::
GROUP_2:106
((a
* H)
* b)
= (a
* (H
* b)) by
Th10;
theorem ::
GROUP_2:107
((H
* a)
* b)
= (H
* (a
* b)) by
Th34;
theorem ::
GROUP_2:108
Th108: a
in (a
* H) & a
in (H
* a)
proof
A1: ((
1_ G)
* a)
= a by
GROUP_1:def 4;
(
1_ G)
in H & (a
* (
1_ G))
= a by
Th46,
GROUP_1:def 4;
hence thesis by
A1,
Th103,
Th104;
end;
theorem ::
GROUP_2:109
((
1_ G)
* H)
= (
carr H) & (H
* (
1_ G))
= (
carr H) by
Th37;
theorem ::
GROUP_2:110
Th110: ((
(1). G)
* a)
=
{a} & (a
* (
(1). G))
=
{a}
proof
A1: the
carrier of (
(1). G)
=
{(
1_ G)} by
Def7;
hence ((
(1). G)
* a)
=
{((
1_ G)
* a)} by
Th18
.=
{a} by
GROUP_1:def 4;
thus (a
* (
(1). G))
=
{(a
* (
1_ G))} by
A1,
Th18
.=
{a} by
GROUP_1:def 4;
end;
theorem ::
GROUP_2:111
Th111: (a
* (
(Omega). G))
= the
carrier of G & ((
(Omega). G)
* a)
= the
carrier of G
proof
((
[#] the
carrier of G)
* a)
= the
carrier of G by
Th17;
hence thesis by
Th17;
end;
theorem ::
GROUP_2:112
G is
commutative
Group implies (a
* H)
= (H
* a) by
Th25;
theorem ::
GROUP_2:113
Th113: a
in H iff (a
* H)
= (
carr H)
proof
thus a
in H implies (a
* H)
= (
carr H)
proof
assume
A1: a
in H;
thus (a
* H)
c= (
carr H)
proof
let x be
object;
assume x
in (a
* H);
then
consider g such that
A2: x
= (a
* g) and
A3: g
in H by
Th103;
(a
* g)
in H by
A1,
A3,
Th50;
hence thesis by
A2;
end;
let x be
object;
assume
A4: x
in (
carr H);
then
A5: x
in H;
reconsider b = x as
Element of G by
A4;
A6: (a
* ((a
" )
* b))
= ((a
* (a
" ))
* b) by
GROUP_1:def 3
.= ((
1_ G)
* b) by
GROUP_1:def 5
.= x by
GROUP_1:def 4;
(a
" )
in H by
A1,
Th51;
then ((a
" )
* b)
in H by
A5,
Th50;
hence thesis by
A6,
Th103;
end;
assume
A7: (a
* H)
= (
carr H);
(a
* (
1_ G))
= a & (
1_ G)
in H by
Th46,
GROUP_1:def 4;
then a
in (
carr H) by
A7,
Th103;
hence thesis;
end;
theorem ::
GROUP_2:114
Th114: (a
* H)
= (b
* H) iff ((b
" )
* a)
in H
proof
thus (a
* H)
= (b
* H) implies ((b
" )
* a)
in H
proof
assume
A1: (a
* H)
= (b
* H);
(((b
" )
* a)
* H)
= ((b
" )
* (a
* H)) by
Th32
.= (((b
" )
* b)
* H) by
A1,
Th32
.= ((
1_ G)
* H) by
GROUP_1:def 5
.= (
carr H) by
Th37;
hence thesis by
Th113;
end;
assume
A2: ((b
" )
* a)
in H;
thus (a
* H)
= ((
1_ G)
* (a
* H)) by
Th37
.= (((
1_ G)
* a)
* H) by
Th32
.= (((b
* (b
" ))
* a)
* H) by
GROUP_1:def 5
.= ((b
* ((b
" )
* a))
* H) by
GROUP_1:def 3
.= (b
* (((b
" )
* a)
* H)) by
Th32
.= (b
* H) by
A2,
Th113;
end;
theorem ::
GROUP_2:115
Th115: (a
* H)
= (b
* H) iff (a
* H)
meets (b
* H)
proof
(a
* H)
<>
{} by
Th108;
hence (a
* H)
= (b
* H) implies (a
* H)
meets (b
* H);
assume (a
* H)
meets (b
* H);
then
consider x be
object such that
A1: x
in (a
* H) and
A2: x
in (b
* H) by
XBOOLE_0: 3;
reconsider x as
Element of G by
A2;
consider g such that
A3: x
= (a
* g) and
A4: g
in H by
A1,
Th103;
A5: (g
" )
in H by
A4,
Th51;
consider h be
Element of G such that
A6: x
= (b
* h) and
A7: h
in H by
A2,
Th103;
a
= ((b
* h)
* (g
" )) by
A3,
A6,
GROUP_1: 14
.= (b
* (h
* (g
" ))) by
GROUP_1:def 3;
then ((b
" )
* a)
= (h
* (g
" )) by
GROUP_1: 13;
then ((b
" )
* a)
in H by
A7,
A5,
Th50;
hence thesis by
Th114;
end;
theorem ::
GROUP_2:116
Th116: ((a
* b)
* H)
c= ((a
* H)
* (b
* H))
proof
let x be
object;
assume x
in ((a
* b)
* H);
then
consider g such that
A1: x
= ((a
* b)
* g) and
A2: g
in H by
Th103;
A3: x
= (((a
* (
1_ G))
* b)
* g) by
A1,
GROUP_1:def 4
.= ((a
* (
1_ G))
* (b
* g)) by
GROUP_1:def 3;
(
1_ G)
in H by
Th46;
then
A4: (a
* (
1_ G))
in (a
* H) by
Th103;
(b
* g)
in (b
* H) by
A2,
Th103;
hence thesis by
A3,
A4;
end;
theorem ::
GROUP_2:117
(
carr H)
c= ((a
* H)
* ((a
" )
* H)) & (
carr H)
c= (((a
" )
* H)
* (a
* H))
proof
A1: (((a
" )
* a)
* H)
= ((
1_ G)
* H) by
GROUP_1:def 5
.= (
carr H) by
Th37;
((a
* (a
" ))
* H)
= ((
1_ G)
* H) by
GROUP_1:def 5
.= (
carr H) by
Th37;
hence thesis by
A1,
Th116;
end;
theorem ::
GROUP_2:118
((a
|^ 2)
* H)
c= ((a
* H)
* (a
* H))
proof
((a
|^ 2)
* H)
= ((a
* a)
* H) by
GROUP_1: 27;
hence thesis by
Th116;
end;
theorem ::
GROUP_2:119
Th119: a
in H iff (H
* a)
= (
carr H)
proof
thus a
in H implies (H
* a)
= (
carr H)
proof
assume
A1: a
in H;
thus (H
* a)
c= (
carr H)
proof
let x be
object;
assume x
in (H
* a);
then
consider g such that
A2: x
= (g
* a) and
A3: g
in H by
Th104;
(g
* a)
in H by
A1,
A3,
Th50;
hence thesis by
A2;
end;
let x be
object;
assume
A4: x
in (
carr H);
then
A5: x
in H;
reconsider b = x as
Element of G by
A4;
A6: ((b
* (a
" ))
* a)
= (b
* ((a
" )
* a)) by
GROUP_1:def 3
.= (b
* (
1_ G)) by
GROUP_1:def 5
.= x by
GROUP_1:def 4;
(a
" )
in H by
A1,
Th51;
then (b
* (a
" ))
in H by
A5,
Th50;
hence thesis by
A6,
Th104;
end;
assume
A7: (H
* a)
= (
carr H);
((
1_ G)
* a)
= a & (
1_ G)
in H by
Th46,
GROUP_1:def 4;
then a
in (
carr H) by
A7,
Th104;
hence thesis;
end;
theorem ::
GROUP_2:120
Th120: (H
* a)
= (H
* b) iff (b
* (a
" ))
in H
proof
thus (H
* a)
= (H
* b) implies (b
* (a
" ))
in H
proof
assume
A1: (H
* a)
= (H
* b);
(
carr H)
= (H
* (
1_ G)) by
Th37
.= (H
* (a
* (a
" ))) by
GROUP_1:def 5
.= ((H
* b)
* (a
" )) by
A1,
Th34
.= (H
* (b
* (a
" ))) by
Th34;
hence thesis by
Th119;
end;
assume (b
* (a
" ))
in H;
hence (H
* a)
= ((H
* (b
* (a
" )))
* a) by
Th119
.= (H
* ((b
* (a
" ))
* a)) by
Th34
.= (H
* (b
* ((a
" )
* a))) by
GROUP_1:def 3
.= (H
* (b
* (
1_ G))) by
GROUP_1:def 5
.= (H
* b) by
GROUP_1:def 4;
end;
theorem ::
GROUP_2:121
(H
* a)
= (H
* b) iff (H
* a)
meets (H
* b)
proof
(H
* a)
<>
{} by
Th108;
hence (H
* a)
= (H
* b) implies (H
* a)
meets (H
* b);
assume (H
* a)
meets (H
* b);
then
consider x be
object such that
A1: x
in (H
* a) and
A2: x
in (H
* b) by
XBOOLE_0: 3;
reconsider x as
Element of G by
A2;
consider g such that
A3: x
= (g
* a) and
A4: g
in H by
A1,
Th104;
A5: (g
" )
in H by
A4,
Th51;
consider h be
Element of G such that
A6: x
= (h
* b) and
A7: h
in H by
A2,
Th104;
a
= ((g
" )
* (h
* b)) by
A3,
A6,
GROUP_1: 13
.= (((g
" )
* h)
* b) by
GROUP_1:def 3;
then (a
* (b
" ))
= ((g
" )
* h) by
GROUP_1: 14;
then (a
* (b
" ))
in H by
A7,
A5,
Th50;
hence thesis by
Th120;
end;
theorem ::
GROUP_2:122
Th122: ((H
* a)
* b)
c= ((H
* a)
* (H
* b))
proof
let x be
object;
(
1_ G)
in H by
Th46;
then
A1: ((
1_ G)
* b)
in (H
* b) by
Th104;
assume x
in ((H
* a)
* b);
then x
in (H
* (a
* b)) by
Th34;
then
consider g such that
A2: x
= (g
* (a
* b)) and
A3: g
in H by
Th104;
A4: x
= ((g
* a)
* b) by
A2,
GROUP_1:def 3
.= ((g
* a)
* ((
1_ G)
* b)) by
GROUP_1:def 4;
(g
* a)
in (H
* a) by
A3,
Th104;
hence thesis by
A1,
A4;
end;
theorem ::
GROUP_2:123
(
carr H)
c= ((H
* a)
* (H
* (a
" ))) & (
carr H)
c= ((H
* (a
" ))
* (H
* a))
proof
A1: ((H
* (a
" ))
* a)
= (H
* ((a
" )
* a)) by
Th34
.= (H
* (
1_ G)) by
GROUP_1:def 5
.= (
carr H) by
Th37;
((H
* a)
* (a
" ))
= (H
* (a
* (a
" ))) by
Th34
.= (H
* (
1_ G)) by
GROUP_1:def 5
.= (
carr H) by
Th37;
hence thesis by
A1,
Th122;
end;
theorem ::
GROUP_2:124
(H
* (a
|^ 2))
c= ((H
* a)
* (H
* a))
proof
(a
|^ 2)
= (a
* a) & ((H
* a)
* a)
= (H
* (a
* a)) by
Th34,
GROUP_1: 27;
hence thesis by
Th122;
end;
theorem ::
GROUP_2:125
(a
* (H1
/\ H2))
= ((a
* H1)
/\ (a
* H2))
proof
thus (a
* (H1
/\ H2))
c= ((a
* H1)
/\ (a
* H2))
proof
let x be
object;
assume x
in (a
* (H1
/\ H2));
then
consider g such that
A1: x
= (a
* g) and
A2: g
in (H1
/\ H2) by
Th103;
g
in H2 by
A2,
Th82;
then
A3: x
in (a
* H2) by
A1,
Th103;
g
in H1 by
A2,
Th82;
then x
in (a
* H1) by
A1,
Th103;
hence thesis by
A3,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A4: x
in ((a
* H1)
/\ (a
* H2));
then x
in (a
* H1) by
XBOOLE_0:def 4;
then
consider g such that
A5: x
= (a
* g) and
A6: g
in H1 by
Th103;
x
in (a
* H2) by
A4,
XBOOLE_0:def 4;
then
consider g1 such that
A7: x
= (a
* g1) and
A8: g1
in H2 by
Th103;
g
= g1 by
A5,
A7,
GROUP_1: 6;
then g
in (H1
/\ H2) by
A6,
A8,
Th82;
hence thesis by
A5,
Th103;
end;
theorem ::
GROUP_2:126
((H1
/\ H2)
* a)
= ((H1
* a)
/\ (H2
* a))
proof
thus ((H1
/\ H2)
* a)
c= ((H1
* a)
/\ (H2
* a))
proof
let x be
object;
assume x
in ((H1
/\ H2)
* a);
then
consider g such that
A1: x
= (g
* a) and
A2: g
in (H1
/\ H2) by
Th104;
g
in H2 by
A2,
Th82;
then
A3: x
in (H2
* a) by
A1,
Th104;
g
in H1 by
A2,
Th82;
then x
in (H1
* a) by
A1,
Th104;
hence thesis by
A3,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A4: x
in ((H1
* a)
/\ (H2
* a));
then x
in (H1
* a) by
XBOOLE_0:def 4;
then
consider g such that
A5: x
= (g
* a) and
A6: g
in H1 by
Th104;
x
in (H2
* a) by
A4,
XBOOLE_0:def 4;
then
consider g1 such that
A7: x
= (g1
* a) and
A8: g1
in H2 by
Th104;
g
= g1 by
A5,
A7,
GROUP_1: 6;
then g
in (H1
/\ H2) by
A6,
A8,
Th82;
hence thesis by
A5,
Th104;
end;
theorem ::
GROUP_2:127
ex H1 be
strict
Subgroup of G st the
carrier of H1
= ((a
* H2)
* (a
" ))
proof
set A = ((a
* H2)
* (a
" ));
set x = the
Element of (a
* H2);
A1: (a
* H2)
<>
{} by
Th108;
then
reconsider x as
Element of G by
Lm1;
A2:
now
let g;
assume g
in A;
then
consider g1 such that
A3: g
= (g1
* (a
" )) and
A4: g1
in (a
* H2) by
Th28;
consider g2 such that
A5: g1
= (a
* g2) and
A6: g2
in H2 by
A4,
Th103;
(g2
" )
in H2 by
A6,
Th51;
then
A7: ((g2
" )
* (a
" ))
in (H2
* (a
" )) by
Th104;
(g
" )
= (((a
" )
" )
* ((a
* g2)
" )) by
A3,
A5,
GROUP_1: 17
.= (a
* ((g2
" )
* (a
" ))) by
GROUP_1: 17;
then (g
" )
in (a
* (H2
* (a
" ))) by
A7,
Th27;
hence (g
" )
in A by
Th10;
end;
A8:
now
let g1, g2;
assume that
A9: g1
in A and
A10: g2
in A;
consider g such that
A11: g1
= (g
* (a
" )) and
A12: g
in (a
* H2) by
A9,
Th28;
consider h be
Element of G such that
A13: g
= (a
* h) and
A14: h
in H2 by
A12,
Th103;
A
= (a
* (H2
* (a
" ))) by
Th10;
then
consider b such that
A15: g2
= (a
* b) and
A16: b
in (H2
* (a
" )) by
A10,
Th27;
consider c be
Element of G such that
A17: b
= (c
* (a
" )) and
A18: c
in H2 by
A16,
Th104;
(h
* c)
in H2 by
A14,
A18,
Th50;
then
A19: (a
* (h
* c))
in (a
* H2) by
Th103;
(g1
* g2)
= ((a
* h)
* ((a
" )
* (a
* (c
* (a
" ))))) by
A11,
A15,
A13,
A17,
GROUP_1:def 3
.= ((a
* h)
* (((a
" )
* a)
* (c
* (a
" )))) by
GROUP_1:def 3
.= ((a
* h)
* ((
1_ G)
* (c
* (a
" )))) by
GROUP_1:def 5
.= ((a
* h)
* (c
* (a
" ))) by
GROUP_1:def 4
.= (((a
* h)
* c)
* (a
" )) by
GROUP_1:def 3
.= ((a
* (h
* c))
* (a
" )) by
GROUP_1:def 3;
hence (g1
* g2)
in A by
A19,
Th28;
end;
(x
* (a
" ))
in A by
A1,
Th28;
hence thesis by
A8,
A2,
Th52;
end;
theorem ::
GROUP_2:128
Th128: ((a
* H),(b
* H))
are_equipotent
proof
defpred
P[
object,
object] means ex g1 st $1
= g1 & $2
= ((b
* (a
" ))
* g1);
A1: for x be
object st x
in (a
* H) holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in (a
* H);
then
reconsider g = x as
Element of G;
reconsider y = ((b
* (a
" ))
* g) as
set;
take y;
take g;
thus thesis;
end;
consider f be
Function such that
A2: (
dom f)
= (a
* H) and
A3: for x be
object st x
in (a
* H) holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A1);
A4: (
rng f)
= (b
* H)
proof
thus (
rng f)
c= (b
* 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 g such that
A7: y
= g and
A8: x
= ((b
* (a
" ))
* g) by
A2,
A3,
A5,
A6;
consider g1 such that
A9: g
= (a
* g1) and
A10: g1
in H by
A2,
A5,
A7,
Th103;
x
= (((b
* (a
" ))
* a)
* g1) by
A8,
A9,
GROUP_1:def 3
.= ((b
* ((a
" )
* a))
* g1) by
GROUP_1:def 3
.= ((b
* (
1_ G))
* g1) by
GROUP_1:def 5
.= (b
* g1) by
GROUP_1:def 4;
hence thesis by
A10,
Th103;
end;
let x be
object;
assume x
in (b
* H);
then
consider g such that
A11: x
= (b
* g) and
A12: g
in H by
Th103;
A13: (a
* g)
in (
dom f) by
A2,
A12,
Th103;
then ex g1 st g1
= (a
* g) & (f
. (a
* g))
= ((b
* (a
" ))
* g1) by
A2,
A3;
then (f
. (a
* g))
= (((b
* (a
" ))
* a)
* g) by
GROUP_1:def 3
.= ((b
* ((a
" )
* a))
* g) by
GROUP_1:def 3
.= ((b
* (
1_ G))
* g) by
GROUP_1:def 5
.= x by
A11,
GROUP_1:def 4;
hence thesis by
A13,
FUNCT_1:def 3;
end;
f is
one-to-one
proof
let x,y be
object;
assume that
A14: x
in (
dom f) & y
in (
dom f) and
A15: (f
. x)
= (f
. y);
(ex g1 st x
= g1 & (f
. x)
= ((b
* (a
" ))
* g1)) & ex g2 st y
= g2 & (f
. y)
= ((b
* (a
" ))
* g2) by
A2,
A3,
A14;
hence thesis by
A15,
GROUP_1: 6;
end;
hence thesis by
A2,
A4,
WELLORD2:def 4;
end;
theorem ::
GROUP_2:129
Th129: ((a
* H),(H
* b))
are_equipotent
proof
defpred
P[
object,
object] means ex g1 st $1
= g1 & $2
= (((a
" )
* g1)
* b);
A1: for x be
object st x
in (a
* H) holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in (a
* H);
then
reconsider g = x as
Element of G;
reconsider y = (((a
" )
* g)
* b) as
set;
take y;
take g;
thus thesis;
end;
consider f be
Function such that
A2: (
dom f)
= (a
* H) and
A3: for x be
object st x
in (a
* H) holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A1);
A4: (
rng f)
= (H
* b)
proof
thus (
rng f)
c= (H
* b)
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 g such that
A7: y
= g and
A8: x
= (((a
" )
* g)
* b) by
A2,
A3,
A5,
A6;
consider g1 such that
A9: g
= (a
* g1) and
A10: g1
in H by
A2,
A5,
A7,
Th103;
x
= ((((a
" )
* a)
* g1)
* b) by
A8,
A9,
GROUP_1:def 3
.= (((
1_ G)
* g1)
* b) by
GROUP_1:def 5
.= (g1
* b) by
GROUP_1:def 4;
hence thesis by
A10,
Th104;
end;
let x be
object;
assume x
in (H
* b);
then
consider g such that
A11: x
= (g
* b) and
A12: g
in H by
Th104;
A13: (a
* g)
in (
dom f) by
A2,
A12,
Th103;
then ex g1 st g1
= (a
* g) & (f
. (a
* g))
= (((a
" )
* g1)
* b) by
A2,
A3;
then (f
. (a
* g))
= ((((a
" )
* a)
* g)
* b) by
GROUP_1:def 3
.= (((
1_ G)
* g)
* b) by
GROUP_1:def 5
.= x by
A11,
GROUP_1:def 4;
hence thesis by
A13,
FUNCT_1:def 3;
end;
f is
one-to-one
proof
let x,y be
object;
assume that
A14: x
in (
dom f) and
A15: y
in (
dom f) and
A16: (f
. x)
= (f
. y);
consider g2 such that
A17: y
= g2 and
A18: (f
. y)
= (((a
" )
* g2)
* b) by
A2,
A3,
A15;
consider g1 such that
A19: x
= g1 and
A20: (f
. x)
= (((a
" )
* g1)
* b) by
A2,
A3,
A14;
((a
" )
* g1)
= ((a
" )
* g2) by
A16,
A20,
A18,
GROUP_1: 6;
hence thesis by
A19,
A17,
GROUP_1: 6;
end;
hence thesis by
A2,
A4,
WELLORD2:def 4;
end;
theorem ::
GROUP_2:130
Th130: ((H
* a),(H
* b))
are_equipotent
proof
((H
* a),(b
* H))
are_equipotent & ((b
* H),(H
* b))
are_equipotent by
Th129;
hence thesis by
WELLORD2: 15;
end;
theorem ::
GROUP_2:131
Th131: ((
carr H),(a
* H))
are_equipotent & ((
carr H),(H
* a))
are_equipotent
proof
(
carr H)
= ((
1_ G)
* H) & (
carr H)
= (H
* (
1_ G)) by
Th37;
hence thesis by
Th128,
Th130;
end;
theorem ::
GROUP_2:132
(
card H)
= (
card (a
* H)) & (
card H)
= (
card (H
* a)) by
Th131,
CARD_1: 5;
theorem ::
GROUP_2:133
Th133: for H be
finite
Subgroup of G holds ex B,C be
finite
set st B
= (a
* H) & C
= (H
* a) & (
card H)
= (
card B) & (
card H)
= (
card C)
proof
let H be
finite
Subgroup of G;
reconsider B = (a
* H), C = (H
* a) as
finite
set by
Th131,
CARD_1: 38;
take B, C;
((
carr H),(a
* H))
are_equipotent & ((
carr H),(H
* a))
are_equipotent by
Th131;
hence thesis by
CARD_1: 5;
end;
definition
let G, H;
::
GROUP_2:def15
func
Left_Cosets H ->
Subset-Family of G means
:
Def15: A
in it iff ex a st A
= (a
* H);
existence
proof
defpred
P[
set] means ex a st $1
= (a
* H);
ex F be
Subset-Family of G st for A be
Subset of G holds A
in F iff
P[A] from
SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
defpred
P[
set] means ex a st $1
= (a
* H);
let F1,F2 be
Subset-Family of G;
assume
A1: for A holds A
in F1 iff
P[A];
assume
A2: for A holds A
in F2 iff
P[A];
thus thesis from
SUBSET_1:sch 4(
A1,
A2);
end;
::
GROUP_2:def16
func
Right_Cosets H ->
Subset-Family of G means
:
Def16: A
in it iff ex a st A
= (H
* a);
existence
proof
defpred
P[
set] means ex a st $1
= (H
* a);
ex F be
Subset-Family of G st for A be
Subset of G holds A
in F iff
P[A] from
SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
defpred
P[
set] means ex a st $1
= (H
* a);
let F1,F2 be
Subset-Family of G;
assume
A3: for A holds A
in F1 iff
P[A];
assume
A4: for A holds A
in F2 iff
P[A];
thus thesis from
SUBSET_1:sch 4(
A3,
A4);
end;
end
theorem ::
GROUP_2:134
G is
finite implies (
Right_Cosets H) is
finite & (
Left_Cosets H) is
finite;
theorem ::
GROUP_2:135
(
carr H)
in (
Left_Cosets H) & (
carr H)
in (
Right_Cosets H)
proof
(
carr H)
= ((
1_ G)
* H) & (
carr H)
= (H
* (
1_ G)) by
Th37;
hence thesis by
Def15,
Def16;
end;
theorem ::
GROUP_2:136
Th136: ((
Left_Cosets H),(
Right_Cosets H))
are_equipotent
proof
defpred
P[
object,
object] means ex g st $1
= (g
* H) & $2
= (H
* (g
" ));
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 g such that
A2: x
= (g
* H) by
Def15;
reconsider y = (H
* (g
" )) as
set;
take y;
take g;
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: (
rng f)
= (
Right_Cosets H)
proof
thus (
rng f)
c= (
Right_Cosets H)
proof
let x be
object;
assume x
in (
rng f);
then
consider y be
object such that
A6: y
in (
dom f) and
A7: (f
. y)
= x by
FUNCT_1:def 3;
ex g st y
= (g
* H) & (f
. y)
= (H
* (g
" )) by
A3,
A4,
A6;
hence thesis by
A7,
Def16;
end;
let x be
object;
assume
A8: x
in (
Right_Cosets H);
then
reconsider A = x as
Subset of G;
consider g such that
A9: A
= (H
* g) by
A8,
Def16;
A10: ((g
" )
* H)
in (
Left_Cosets H) by
Def15;
then
A11: (f
. ((g
" )
* H))
in (
rng f) by
A3,
FUNCT_1:def 3;
consider a such that
A12: ((g
" )
* H)
= (a
* H) and
A13: (f
. ((g
" )
* H))
= (H
* (a
" )) by
A4,
A10;
((a
" )
* (g
" ))
in H by
A12,
Th114;
hence thesis by
A9,
A11,
A13,
Th120;
end;
f is
one-to-one
proof
let x,y be
object;
assume that
A14: x
in (
dom f) and
A15: y
in (
dom f) and
A16: (f
. x)
= (f
. y);
consider b such that
A17: y
= (b
* H) and
A18: (f
. y)
= (H
* (b
" )) by
A3,
A4,
A15;
consider a such that
A19: x
= (a
* H) and
A20: (f
. x)
= (H
* (a
" )) by
A3,
A4,
A14;
((b
" )
* ((a
" )
" ))
in H by
A16,
A20,
A18,
Th120;
hence thesis by
A19,
A17,
Th114;
end;
hence thesis by
A3,
A5,
WELLORD2:def 4;
end;
theorem ::
GROUP_2:137
Th137: (
union (
Left_Cosets H))
= the
carrier of G & (
union (
Right_Cosets H))
= the
carrier of G
proof
thus (
union (
Left_Cosets H))
= the
carrier of G
proof
set h = the
Element of H;
reconsider g = h as
Element of G by
Th42;
thus (
union (
Left_Cosets H))
c= the
carrier of G;
let x be
object;
assume x
in the
carrier of G;
then
reconsider a = x as
Element of G;
A1: a
= (a
* (
1_ G)) by
GROUP_1:def 4
.= (a
* ((g
" )
* g)) by
GROUP_1:def 5
.= ((a
* (g
" ))
* g) by
GROUP_1:def 3;
A2: ((a
* (g
" ))
* H)
in (
Left_Cosets H) by
Def15;
h
in H;
then a
in ((a
* (g
" ))
* H) by
A1,
Th103;
hence thesis by
A2,
TARSKI:def 4;
end;
set h = the
Element of H;
reconsider g = h as
Element of G by
Th42;
thus (
union (
Right_Cosets H))
c= the
carrier of G;
let x be
object;
assume x
in the
carrier of G;
then
reconsider a = x as
Element of G;
A3: a
= ((
1_ G)
* a) by
GROUP_1:def 4
.= ((g
* (g
" ))
* a) by
GROUP_1:def 5
.= (g
* ((g
" )
* a)) by
GROUP_1:def 3;
A4: (H
* ((g
" )
* a))
in (
Right_Cosets H) by
Def16;
h
in H;
then a
in (H
* ((g
" )
* a)) by
A3,
Th104;
hence thesis by
A4,
TARSKI:def 4;
end;
theorem ::
GROUP_2:138
Th138: (
Left_Cosets (
(1). G))
= the set of all
{a}
proof
set A = the set of all
{a};
thus (
Left_Cosets (
(1). G))
c= A
proof
let x be
object;
assume
A1: x
in (
Left_Cosets (
(1). G));
then
reconsider X = x as
Subset of G;
consider g such that
A2: X
= (g
* (
(1). G)) by
A1,
Def15;
x
=
{g} by
A2,
Th110;
hence thesis;
end;
let x be
object;
assume x
in A;
then
consider a such that
A3: x
=
{a};
(a
* (
(1). G))
=
{a} by
Th110;
hence thesis by
A3,
Def15;
end;
theorem ::
GROUP_2:139
(
Right_Cosets (
(1). G))
= the set of all
{a}
proof
set A = the set of all
{a};
thus (
Right_Cosets (
(1). G))
c= A
proof
let x be
object;
assume
A1: x
in (
Right_Cosets (
(1). G));
then
reconsider X = x as
Subset of G;
consider g such that
A2: X
= ((
(1). G)
* g) by
A1,
Def16;
x
=
{g} by
A2,
Th110;
hence thesis;
end;
let x be
object;
assume x
in A;
then
consider a such that
A3: x
=
{a};
((
(1). G)
* a)
=
{a} by
Th110;
hence thesis by
A3,
Def16;
end;
theorem ::
GROUP_2:140
for H be
strict
Subgroup of G holds (
Left_Cosets H)
= the set of all
{a} implies H
= (
(1). G)
proof
let H be
strict
Subgroup of G;
assume
A1: (
Left_Cosets H)
= the set of all
{a};
A2: the
carrier of H
c=
{(
1_ G)}
proof
set a = the
Element of G;
let x be
object;
assume x
in the
carrier of H;
then
reconsider h = x as
Element of H;
A3: h
in H;
reconsider h as
Element of G by
Th42;
(a
* H)
in (
Left_Cosets H) by
Def15;
then
consider b such that
A4: (a
* H)
=
{b} by
A1;
(a
* h)
in (a
* H) by
A3,
Th103;
then
A5: (a
* h)
= b by
A4,
TARSKI:def 1;
(
1_ G)
in H by
Th46;
then (a
* (
1_ G))
in (a
* H) by
Th103;
then (a
* (
1_ G))
= b by
A4,
TARSKI:def 1;
then h
= (
1_ G) by
A5,
GROUP_1: 6;
hence thesis by
TARSKI:def 1;
end;
(
1_ G)
in H by
Th46;
then (
1_ G)
in the
carrier of H;
then
{(
1_ G)}
c= the
carrier of H by
ZFMISC_1: 31;
then
{(
1_ G)}
= the
carrier of H by
A2;
hence thesis by
Def7;
end;
theorem ::
GROUP_2:141
for H be
strict
Subgroup of G holds (
Right_Cosets H)
= the set of all
{a} implies H
= (
(1). G)
proof
let H be
strict
Subgroup of G;
assume
A1: (
Right_Cosets H)
= the set of all
{a};
A2: the
carrier of H
c=
{(
1_ G)}
proof
set a = the
Element of G;
let x be
object;
assume x
in the
carrier of H;
then
reconsider h = x as
Element of H;
A3: h
in H;
reconsider h as
Element of G by
Th42;
(H
* a)
in (
Right_Cosets H) by
Def16;
then
consider b such that
A4: (H
* a)
=
{b} by
A1;
(h
* a)
in (H
* a) by
A3,
Th104;
then
A5: (h
* a)
= b by
A4,
TARSKI:def 1;
(
1_ G)
in H by
Th46;
then ((
1_ G)
* a)
in (H
* a) by
Th104;
then ((
1_ G)
* a)
= b by
A4,
TARSKI:def 1;
then h
= (
1_ G) by
A5,
GROUP_1: 6;
hence thesis by
TARSKI:def 1;
end;
(
1_ G)
in H by
Th46;
then (
1_ G)
in the
carrier of H;
then
{(
1_ G)}
c= the
carrier of H by
ZFMISC_1: 31;
then
{(
1_ G)}
= the
carrier of H by
A2;
hence thesis by
Def7;
end;
theorem ::
GROUP_2:142
Th142: (
Left_Cosets (
(Omega). G))
=
{the
carrier of G} & (
Right_Cosets (
(Omega). G))
=
{the
carrier of G}
proof
set a = the
Element of G;
A1: (
Left_Cosets (
(Omega). G))
c=
{the
carrier of G}
proof
let x be
object;
assume
A2: x
in (
Left_Cosets (
(Omega). G));
then
reconsider X = x as
Subset of G;
consider a such that
A3: X
= (a
* (
(Omega). G)) by
A2,
Def15;
(a
* (
(Omega). G))
= the
carrier of G by
Th111;
hence thesis by
A3,
TARSKI:def 1;
end;
A4: (
Right_Cosets (
(Omega). G))
c=
{the
carrier of G}
proof
let x be
object;
assume
A5: x
in (
Right_Cosets (
(Omega). G));
then
reconsider X = x as
Subset of G;
consider a such that
A6: X
= ((
(Omega). G)
* a) by
A5,
Def16;
((
(Omega). G)
* a)
= the
carrier of G by
Th111;
hence thesis by
A6,
TARSKI:def 1;
end;
((
(Omega). G)
* a)
= the
carrier of G by
Th111;
then the
carrier of G
in (
Right_Cosets (
(Omega). G)) by
Def16;
then
A7:
{the
carrier of G}
c= (
Right_Cosets (
(Omega). G)) by
ZFMISC_1: 31;
(a
* (
(Omega). G))
= the
carrier of G by
Th111;
then the
carrier of G
in (
Left_Cosets (
(Omega). G)) by
Def15;
then
{the
carrier of G}
c= (
Left_Cosets (
(Omega). G)) by
ZFMISC_1: 31;
hence thesis by
A7,
A1,
A4;
end;
theorem ::
GROUP_2:143
Th143: for G be
strict
Group, H be
strict
Subgroup of G holds (
Left_Cosets H)
=
{the
carrier of G} implies H
= G
proof
let G be
strict
Group, H be
strict
Subgroup of G;
assume (
Left_Cosets H)
=
{the
carrier of G};
then
A1: the
carrier of G
in (
Left_Cosets H) by
TARSKI:def 1;
then
reconsider T = the
carrier of G as
Subset of G;
consider a be
Element of G such that
A2: T
= (a
* H) by
A1,
Def15;
now
let g be
Element of G;
ex b be
Element of G st (a
* g)
= (a
* b) & b
in H by
A2,
Th103;
hence g
in H by
GROUP_1: 6;
end;
hence thesis by
Th62;
end;
theorem ::
GROUP_2:144
for G be
strict
Group, H be
strict
Subgroup of G holds (
Right_Cosets H)
=
{the
carrier of G} implies H
= G
proof
let G be
strict
Group, H be
strict
Subgroup of G;
assume (
Right_Cosets H)
=
{the
carrier of G};
then
A1: the
carrier of G
in (
Right_Cosets H) by
TARSKI:def 1;
then
reconsider T = the
carrier of G as
Subset of G;
consider a be
Element of G such that
A2: T
= (H
* a) by
A1,
Def16;
now
let g be
Element of G;
ex b be
Element of G st (g
* a)
= (b
* a) & b
in H by
A2,
Th104;
hence g
in H by
GROUP_1: 6;
end;
hence thesis by
Th62;
end;
definition
let G, H;
::
GROUP_2:def17
func
Index H ->
Cardinal equals (
card (
Left_Cosets H));
correctness ;
end
theorem ::
GROUP_2:145
(
Index H)
= (
card (
Left_Cosets H)) & (
Index H)
= (
card (
Right_Cosets H)) by
Th136,
CARD_1: 5;
definition
let G, H;
assume
A1: (
Left_Cosets H) is
finite;
::
GROUP_2:def18
func
index H ->
Element of
NAT means
:
Def18: ex B be
finite
set st B
= (
Left_Cosets H) & it
= (
card B);
existence
proof
reconsider B = (
Left_Cosets H) as
finite
set by
A1;
take (
card B), B;
thus thesis;
end;
uniqueness ;
end
theorem ::
GROUP_2:146
(
Left_Cosets H) is
finite implies (ex B be
finite
set st B
= (
Left_Cosets H) & (
index H)
= (
card B)) & ex C be
finite
set st C
= (
Right_Cosets H) & (
index H)
= (
card C)
proof
assume (
Left_Cosets H) is
finite;
then
reconsider B = (
Left_Cosets H) as
finite
set;
hereby
take B;
thus B
= (
Left_Cosets H) & (
index H)
= (
card B) by
Def18;
end;
then
reconsider C = (
Right_Cosets H) as
finite
set by
Th136,
CARD_1: 38;
take C;
(
index H)
= (
card B) & (B,C)
are_equipotent by
Def18,
Th136;
hence thesis by
CARD_1: 5;
end;
Lm5: for X be
finite
set st (for Y st Y
in X holds ex B be
finite
set st B
= Y & (
card B)
= k & for Z st Z
in X & Y
<> Z holds (Y,Z)
are_equipotent & Y
misses Z) holds ex C be
finite
set st C
= (
union X) & (
card C)
= (k
* (
card X))
proof
let X be
finite
set;
per cases ;
suppose
A1: X
=
{} ;
reconsider E =
{} as
finite
set;
assume for Y st Y
in X holds ex B be
finite
set st B
= Y & (
card B)
= k & for Z st Z
in X & Y
<> Z holds (Y,Z)
are_equipotent & Y
misses Z;
take E;
thus thesis by
A1,
CARD_1: 27,
ZFMISC_1: 2;
end;
suppose X
<>
{} ;
then
reconsider D = X as non
empty
set;
defpred
P[
Element of (
Fin D)] means (for Y st Y
in $1 holds ex B be
finite
set st B
= Y & (
card B)
= k & for Z st Z
in $1 & Y
<> Z holds (Y,Z)
are_equipotent & Y
misses Z) implies ex C be
finite
set st C
= (
union $1) & (
card C)
= (k
* (
card $1));
A2: for S be
Element of (
Fin D), s be
Element of D st
P[S] & not s
in S holds
P[(S
\/
{.s.})]
proof
let S be
Element of (
Fin D), s be
Element of D;
assume that
A3: (for Y st Y
in S holds ex B be
finite
set st B
= Y & (
card B)
= k & for Z st Z
in S & Y
<> Z holds (Y,Z)
are_equipotent & Y
misses Z) implies ex C be
finite
set st C
= (
union S) & (
card C)
= (k
* (
card S)) and
A4: not s
in S and
A5: for Y st Y
in (S
\/
{s}) holds ex B be
finite
set st B
= Y & (
card B)
= k & for Z st Z
in (S
\/
{s}) & Y
<> Z holds (Y,Z)
are_equipotent & Y
misses Z;
A6: (
card (S
\/
{s}))
= ((
card S)
+ 1) by
A4,
CARD_2: 41;
now
let Y;
assume Y
in S;
then Y
in (S
\/
{s}) by
XBOOLE_0:def 3;
then ex B be
finite
set st B
= Y & (
card B)
= k & for Z st Z
in (S
\/
{s}) & Y
<> Z holds (Y,Z)
are_equipotent & Y
misses Z by
A5;
hence Y is
finite;
end;
then
reconsider D1 = (
union S) as
finite
set by
FINSET_1: 7;
A7:
now
let Y, Z;
assume Y
in S;
then Y
in (S
\/
{s}) by
XBOOLE_0:def 3;
then
consider B be
finite
set such that
A8: B
= Y & (
card B)
= k and
A9: for Z st Z
in (S
\/
{s}) & Y
<> Z holds (Y,Z)
are_equipotent & Y
misses Z by
A5;
take B;
thus B
= Y & (
card B)
= k by
A8;
let Z;
assume that
A10: Z
in S and
A11: Y
<> Z;
Z
in (S
\/
{s}) by
A10,
XBOOLE_0:def 3;
hence (Y,Z)
are_equipotent & Y
misses Z by
A9,
A11;
end;
s
in
{s} by
TARSKI:def 1;
then s
in (S
\/
{s}) by
XBOOLE_0:def 3;
then
A12: ex B be
finite
set st B
= s & (
card B)
= k & for Z st Z
in (S
\/
{s}) & s
<> Z holds (s,Z)
are_equipotent & s
misses Z by
A5;
then
reconsider T = s as
finite
set;
A13: (
union
{s})
= s by
ZFMISC_1: 25;
then
A14: (
union (S
\/
{s}))
= (D1
\/ T) by
ZFMISC_1: 78;
then
reconsider D2 = (
union (S
\/
{s})) as
finite
set;
take D2;
thus D2
= (
union (S
\/
{s}));
now
assume (
union S)
meets (
union
{s});
then
consider x be
object such that
A15: x
in (
union S) and
A16: x
in (
union
{s}) by
XBOOLE_0: 3;
consider Y such that
A17: x
in Y and
A18: Y
in S by
A15,
TARSKI:def 4;
consider Z such that
A19: x
in Z and
A20: Z
in
{s} by
A16,
TARSKI:def 4;
A21: Z
in (S
\/
{s}) by
A20,
XBOOLE_0:def 3;
Y
in (S
\/
{s}) by
A18,
XBOOLE_0:def 3;
then
A22: ex B be
finite
set st B
= Y & (
card B)
= k & for Z st Z
in (S
\/
{s}) & Y
<> Z holds (Y,Z)
are_equipotent & Y
misses Z by
A5;
Z
<> Y by
A4,
A18,
A20,
TARSKI:def 1;
then Y
misses Z by
A21,
A22;
hence contradiction by
A17,
A19,
XBOOLE_0: 3;
end;
hence (
card D2)
= ((k
* (
card S))
+ (k
* 1)) by
A3,
A13,
A12,
A14,
A7,
CARD_2: 40
.= (k
* (
card (S
\/
{s}))) by
A6;
end;
A23: X is
Element of (
Fin D) by
FINSUB_1:def 5;
A24:
P[(
{}. D)] by
ZFMISC_1: 2;
for B be
Element of (
Fin D) holds
P[B] from
SETWISEO:sch 2(
A24,
A2);
hence thesis by
A23;
end;
end;
::$Notion-Name
theorem ::
GROUP_2:147
Th147: for G be
finite
Group, H be
Subgroup of G holds (
card G)
= ((
card H)
* (
index H))
proof
let G be
finite
Group, H be
Subgroup of G;
reconsider C = (
Left_Cosets H) as
finite
set;
now
let X be
set;
assume
A1: X
in C;
then
reconsider x = X as
Subset of G;
x is
finite;
then
reconsider B = X as
finite
set;
take B;
thus B
= X;
consider a be
Element of G such that
A2: x
= (a
* H) by
A1,
Def15;
ex B,C be
finite
set st B
= (a
* H) & C
= (H
* a) & (
card H)
= (
card B) & (
card H)
= (
card C) by
Th133;
hence (
card B)
= (
card H) by
A2;
let Y;
assume that
A3: Y
in C and
A4: X
<> Y;
reconsider y = Y as
Subset of G by
A3;
A5: ex b be
Element of G st y
= (b
* H) by
A3,
Def15;
hence (X,Y)
are_equipotent by
A2,
Th128;
thus X
misses Y by
A2,
A4,
A5,
Th115;
end;
then
A6: ex D be
finite
set st D
= (
union C) & (
card D)
= ((
card H)
* (
card C)) by
Lm5;
(
union (
Left_Cosets H))
= the
carrier of G by
Th137;
hence thesis by
A6,
Def18;
end;
theorem ::
GROUP_2:148
for G be
finite
Group, H be
Subgroup of G holds (
card H)
divides (
card G)
proof
let G be
finite
Group, H be
Subgroup of G;
(
card G)
= ((
card H)
* (
index H)) by
Th147;
hence thesis by
NAT_D:def 3;
end;
theorem ::
GROUP_2:149
for G be
finite
Group, I,H be
Subgroup of G, J be
Subgroup of H holds I
= J implies (
index I)
= ((
index J)
* (
index H))
proof
let G be
finite
Group, I,H be
Subgroup of G, J be
Subgroup of H;
assume
A1: I
= J;
(
card G)
= ((
card H)
* (
index H)) & (
card H)
= ((
card J)
* (
index J)) by
Th147;
then ((
card I)
* ((
index J)
* (
index H)))
= ((
card I)
* (
index I)) by
A1,
Th147;
hence thesis by
XCMPLX_1: 5;
end;
theorem ::
GROUP_2:150
(
index (
(Omega). G))
= 1
proof
(
Left_Cosets (
(Omega). G))
=
{the
carrier of G} by
Th142;
hence (
index (
(Omega). G))
= (
card
{the
carrier of G}) by
Def18
.= 1 by
CARD_1: 30;
end;
theorem ::
GROUP_2:151
for G be
strict
Group, H be
strict
Subgroup of G holds (
Left_Cosets H) is
finite & (
index H)
= 1 implies H
= G
proof
let G be
strict
Group, H be
strict
Subgroup of G;
assume that
A1: (
Left_Cosets H) is
finite and
A2: (
index H)
= 1;
reconsider B = (
Left_Cosets H) as
finite
set by
A1;
(
card B)
= 1 by
A2,
Def18;
then
consider x be
object such that
A3: (
Left_Cosets H)
=
{x} by
CARD_2: 42;
(
union
{x})
= x & (
union (
Left_Cosets H))
= the
carrier of G by
Th137,
ZFMISC_1: 25;
hence thesis by
A3,
Th143;
end;
theorem ::
GROUP_2:152
(
Index (
(1). G))
= (
card G)
proof
deffunc
F(
object) =
{$1};
consider f be
Function such that
A1: (
dom f)
= the
carrier of G and
A2: for x be
object st x
in the
carrier of G holds (f
. x)
=
F(x) from
FUNCT_1:sch 3;
A3: (
rng f)
= (
Left_Cosets (
(1). G))
proof
thus (
rng f)
c= (
Left_Cosets (
(1). G))
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;
x
=
{y} by
A2,
A5;
then x
in the set of all
{a};
hence thesis by
Th138;
end;
let x be
object;
assume x
in (
Left_Cosets (
(1). G));
then x
in the set of all
{a} by
Th138;
then
consider a such that
A6: x
=
{a};
(f
. a)
=
{a} by
A2;
hence thesis by
A1,
A6,
FUNCT_1:def 3;
end;
f is
one-to-one
proof
let x,y be
object;
assume that
A7: x
in (
dom f) & y
in (
dom f) and
A8: (f
. x)
= (f
. y);
(f
. y)
=
{y} & (f
. x)
=
{x} by
A1,
A2,
A7;
hence thesis by
A8,
ZFMISC_1: 3;
end;
then (the
carrier of G,(
Left_Cosets (
(1). G)))
are_equipotent by
A1,
A3,
WELLORD2:def 4;
hence thesis by
CARD_1: 5;
end;
theorem ::
GROUP_2:153
for G be
finite
Group holds (
index (
(1). G))
= (
card G)
proof
let G be
finite
Group;
thus (
card G)
= ((
card (
(1). G))
* (
index (
(1). G))) by
Th147
.= (1
* (
index (
(1). G))) by
Th69
.= (
index (
(1). G));
end;
theorem ::
GROUP_2:154
Th154: for G be
finite
Group, H be
strict
Subgroup of G holds (
index H)
= (
card G) implies H
= (
(1). G)
proof
let G be
finite
Group, H be
strict
Subgroup of G;
assume (
index H)
= (
card G);
then (1
* (
card G))
= ((
card H)
* (
card G)) by
Th147;
hence thesis by
Th70,
XCMPLX_1: 5;
end;
theorem ::
GROUP_2:155
for H be
strict
Subgroup of G holds (
Left_Cosets H) is
finite & (
Index H)
= (
card G) implies G is
finite & H
= (
(1). G)
proof
let H be
strict
Subgroup of G;
assume that
A1: (
Left_Cosets H) is
finite and
A2: (
Index H)
= (
card G);
thus
A3: G is
finite by
A1,
A2;
ex B be
finite
set st B
= (
Left_Cosets H) & (
index H)
= (
card B) by
A1,
Def18;
hence thesis by
A2,
A3,
Th154;
end;
theorem ::
GROUP_2:156
for X be
finite
set st (for Y st Y
in X holds ex B be
finite
set st B
= Y & (
card B)
= k & for Z st Z
in X & Y
<> Z holds (Y,Z)
are_equipotent & Y
misses Z) holds ex C be
finite
set st C
= (
union X) & (
card C)
= (k
* (
card X)) by
Lm5;