Copyright (c) 1991 Association of Mizar Users
environ
vocabulary FUNCT_1, REALSET1, GROUP_2, GROUP_3, RLSUB_1, INT_1, BOOLE,
RELAT_1, GROUP_1, RCOMP_1, SUBSET_1, GROUP_4, GROUP_5, VECTSP_1,
NATTRA_1, FINSET_1, CARD_1, BINOP_1, QC_LANG1, ABSVALUE, WELLORD1,
LATTICES, GROUP_6;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, STRUCT_0, CARD_1, FINSET_1, BINOP_1, REALSET1, INT_1,
RLVECT_1, VECTSP_1, GROUP_1, GROUP_2, GROUP_3, NAT_1, GROUP_4, GROUP_5;
constructors DOMAIN_1, BINOP_1, REALSET1, NAT_1, GROUP_4, GROUP_5, MEMBERED,
PARTFUN1, RELAT_2, XBOOLE_0;
clusters FUNCT_1, FINSET_1, GROUP_1, GROUP_2, GROUP_3, STRUCT_0, RELSET_1,
INT_1, FUNCT_2, MEMBERED, ZFMISC_1, PARTFUN1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;
definitions XBOOLE_0, FUNCT_1, GROUP_1, GROUP_2, TARSKI, VECTSP_1, STRUCT_0;
theorems BINOP_1, CARD_1, CARD_2, FINSET_1, FUNCT_1, FUNCT_2, GROUP_1,
GROUP_2, GROUP_3, GROUP_4, GROUP_5, TARSKI, ZFMISC_1, RLVECT_1, REALSET1,
VECTSP_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1;
schemes BINOP_1, COMPLSP1, FUNCT_1, FUNCT_2, DOMAIN_1, NAT_1;
begin
theorem Th1:
for A,B being non empty set, f being Function of A,B holds
f is one-to-one iff
for a,b being Element of A st f.a = f.b holds a = b
proof
let A,B be non empty set;
let f be Function of A,B;
thus f is one-to-one implies
for a,b being Element of A st f.a = f.b holds a = b
by FUNCT_2:25;
assume for a,b being Element of A st f.a = f.b holds a = b;
then for a,b being set st a in A & b in A & f.a = f.b holds a = b;
hence thesis by FUNCT_2:25;
end;
definition let G be Group, A be Subgroup of G;
redefine mode Subgroup of A -> Subgroup of G;
coherence
proof
let H be Subgroup of A;
thus thesis by GROUP_2:65;
end;
end;
definition let G be Group;
cluster (1).G -> normal;
coherence by GROUP_3:137;
cluster (Omega).G -> normal;
coherence by GROUP_3:137;
end;
reserve n for Nat;
reserve i for Integer;
reserve G,H,I for Group;
reserve A,B for Subgroup of G;
reserve N for normal Subgroup of G;
reserve a,a1,a2,a3,b,b1 for Element of G;
reserve c,d for Element of H;
reserve f for Function of the carrier of G, the carrier of H;
reserve x,y,y1,y2,z for set;
reserve A1,A2 for Subset of G;
theorem Th2:
for X being Subgroup of A, x being Element of A st x = a holds
x * X = a * (X qua Subgroup of G) & X * x = (X qua Subgroup of G) * a
proof let X be Subgroup of A, x be Element of A;
assume A1: x = a;
set I = X qua Subgroup of G;
thus x * X c= a * I
proof let y;
assume y in x * X;
then consider g being Element of A such that
A2: y = x * g & g in X by GROUP_2:125;
reconsider h = g as Element of G by GROUP_2:51;
a * h = x * g by A1,GROUP_2:52;
hence thesis by A2,GROUP_2:125;
end;
thus a * I c= x * X
proof let y;
assume y in a * I;
then consider b such that A3: y = a * b & b in X by GROUP_2:125;
reconsider c = b as Element of X by A3,RLVECT_1:def 1;
reconsider c as Element of A by GROUP_2:51;
a * b = x * c by A1,GROUP_2:52;
hence thesis by A3,GROUP_2:125;
end;
thus X * x c= I * a
proof let y;
assume y in X * x;
then consider g being Element of A such that
A4: y = g * x & g in X by GROUP_2:126;
reconsider h = g as Element of G by GROUP_2:51;
h * a = g * x by A1,GROUP_2:52;
hence thesis by A4,GROUP_2:126;
end;
thus I * a c= X * x
proof let y;
assume y in I * a;
then consider b such that A5: y = b * a & b in X by GROUP_2:126;
reconsider c = b as Element of X by A5,RLVECT_1:def 1;
reconsider c as Element of A by GROUP_2:51;
b * a = c * x by A1,GROUP_2:52;
hence thesis by A5,GROUP_2:126;
end;
end;
theorem
for X,Y being Subgroup of A holds
(X qua Subgroup of G) /\ (Y qua Subgroup of G) = X /\ Y
proof let X,Y be Subgroup of A;
A1: the carrier of X /\ Y = (carr X) /\ (carr Y) &
the carrier of (X qua Subgroup of G) /\ (Y qua Subgroup of G) =
(carr (X qua Subgroup of G)) /\ (carr (Y qua Subgroup of G)) &
carr X = the carrier of X & the carrier of Y = carr Y &
carr (X qua Subgroup of G) = the carrier of X &
the carrier of Y = carr (Y qua Subgroup of G)
by GROUP_2:def 9,def 10;
reconsider Z = X /\ Y as Subgroup of G by GROUP_2:65;
(X qua Subgroup of G) /\ (Y qua Subgroup of G) = Z by A1,GROUP_2:97;
hence thesis;
end;
theorem Th4:
a * b * a" = b |^ a" & a * (b * a") = b |^ a"
proof
thus a * b * a" = a"" * b * a" by GROUP_1:19
.= b |^ a" by GROUP_3:def 2;
hence thesis by VECTSP_1:def 16;
end;
canceled;
theorem Th6:
a * A * A = a * A & a * (A * A) = a * A &
A * A * a = A * a & A * (A * a) = A *a
proof
thus a * A * A = a * (A * A) by GROUP_4:60
.= a * carr A by GROUP_4:58
.= a * A by GROUP_2:def 13;
hence a * (A * A) = a * A by GROUP_4:60;
thus A * A * a = carr A * a by GROUP_4:58
.= A * a by GROUP_2:def 14;
hence thesis by GROUP_4:61;
end;
theorem Th7:
for G being Group, A1 being Subset of G holds
A1 = {[.a,b.] where a is Element of G,
b is Element of G : not contradiction}
implies G` = gr A1
proof let G be Group, A1 be Subset of G;
assume A1: A1 =
{[.a,b.] where a is Element of G,
b is Element of G : not contradiction};
A1 = commutators G
proof
thus A1 c= commutators G
proof let x;
assume x in A1;
then ex a,b being Element of G st x = [.a,b.] by A1;
hence thesis by GROUP_5:65;
end;
let x;
assume x in commutators G;
then ex a,b being Element of G st x = [.a,b.]
by GROUP_5:65;
hence thesis by A1;
end;
hence thesis by GROUP_5:82;
end;
theorem Th8:
for G being strict Group, B being strict Subgroup of G holds
G` is Subgroup of B iff
for a,b being Element of G holds [.a,b.] in B
proof let G be strict Group, B be strict Subgroup of G;
thus G` is Subgroup of B implies
for a,b being Element of G holds [.a,b.] in B
proof assume A1: G` is Subgroup of B;
let a,b be Element of G;
[.a,b.] in G` by GROUP_5:84;
hence thesis by A1,GROUP_2:49;
end;
assume A2: for a,b being Element of G holds [.a,b.] in B;
defpred P[set,set] means not contradiction;
deffunc F(Element of G,Element of G) =
[.$1,$2.];
reconsider X =
{F(a,b) where a is Element of G,
b is Element of G : P[a,b]}
as Subset of G from SubsetFD2;
X c= the carrier of B
proof let x;
assume x in X;
then ex a,b being Element of G st x = [.a,b.];
then x in B by A2;
hence thesis by RLVECT_1:def 1;
end;
then gr X is Subgroup of B by GROUP_4:def 5;
hence thesis by Th7;
end;
theorem Th9:
for N being normal Subgroup of G holds
N is Subgroup of B implies N is normal Subgroup of B
proof let N be normal Subgroup of G;
assume N is Subgroup of B;
then reconsider N' = N as Subgroup of B;
now let n be Element of B;
thus n * N' c= N' * n
proof let x;
assume x in n * N';
then consider a being Element of B such that
A1: x = n * a and A2: a in N' by GROUP_2:125;
reconsider a' = a, n' = n as Element of G
by GROUP_2:51;
x = n' * a' by A1,GROUP_2:52;
then x in n' * N & n' * N c= N * n' by A2,GROUP_2:125,GROUP_3:141;
then consider a1 such that A3: x = a1 * n' and A4: a1 in N
by GROUP_2:126;
a1 in N' by A4;
then a1 in B by GROUP_2:49;
then reconsider a1' = a1 as Element of B
by RLVECT_1:def 1;
x = a1' * n by A3,GROUP_2:52;
hence thesis by A4,GROUP_2:126;
end;
end;
hence thesis by GROUP_3:141;
end;
definition let G,B; let M be normal Subgroup of G;
assume A1: the HGrStr of M is Subgroup of B;
func (B,M)`*` -> strict normal Subgroup of B equals
:Def1: the HGrStr of M;
coherence
proof
reconsider x = the HGrStr of M as Subgroup of G by A1;
now let a;
A2: carr x = the carrier of M by GROUP_2:def 9
.= carr M by GROUP_2:def 9;
thus a * x = a * carr x by GROUP_2:def 13
.= a * M by A2,GROUP_2:def 13
.= M * a by GROUP_3:140
.= carr(M) * a by GROUP_2:def 14
.= x * a by A2,GROUP_2:def 14;
end;
then x is normal Subgroup of G by GROUP_3:140;
hence thesis by A1,Th9;
end;
correctness;
end;
theorem Th10:
B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B
proof
thus
B /\ N is normal Subgroup of B
proof reconsider A = B /\ N as Subgroup of B by GROUP_2:106;
now let b be Element of B;
thus b * A c= A * b
proof let x;
assume x in b * A;
then consider a being Element of B such that
A1: x = b * a and
A2: a in A by GROUP_2:125;
A3: a in N by A2,GROUP_2:99;
reconsider a' = a, b' = b as Element of G
by GROUP_2:51;
x = b' * a' by A1,GROUP_2:52;
then x in b' * N & b' * N c= N * b' by A3,GROUP_2:125,GROUP_3:141;
then consider b1 such that A4: x = b1 * b' and A5: b1 in N
by GROUP_2:126;
reconsider x' = x as Element of B by A1;
reconsider x'' = x as Element of G by A4;
b1 = x'' * b'" & b'" = b" by A4,GROUP_1:22,GROUP_2:57;
then A6:b1 = x' * b" by GROUP_2:52;
then A7: b1 in B by RLVECT_1:def 1;
reconsider b1' = b1 as Element of B by A6;
b1' * b = x & b1' in A by A4,A5,A7,GROUP_2:52,99;
hence thesis by GROUP_2:126;
end;
end;
hence thesis by GROUP_3:141;
end;
hence thesis;
end;
definition let G,B; let N be normal Subgroup of G;
redefine func B /\ N -> strict normal Subgroup of B;
coherence by Th10;
end;
definition let G; let N be normal Subgroup of G; let B;
redefine func N /\ B -> strict normal Subgroup of B;
coherence by Th10;
end;
definition let G be non empty 1-sorted;
redefine attr G is trivial means :Def2:
ex x st the carrier of G = {x};
compatibility
proof
hereby assume A1: G is trivial;
consider y being Element of G;
for x holds x in the carrier of G iff x = y by A1,REALSET1:def 20;
then the carrier of G = {y} by TARSKI:def 1;
hence ex x st the carrier of G = {x};
end;
given x such that
A2: the carrier of G = {x};
now let a,b be Element of G;
thus a = x by A2,TARSKI:def 1 .= b by A2,TARSKI:def 1;
end;
hence thesis by REALSET1:def 20;
end;
end;
definition
cluster trivial Group;
existence
proof consider G;
take (1).G;
the carrier of (1).G = {1.G} by GROUP_2:def 7;
hence thesis by Def2;
end;
end;
theorem Th11:
(1).G is trivial
proof
the carrier of (1).G = {1.G} by GROUP_2:def 7;
hence thesis by Def2;
end;
theorem Th12:
G is trivial iff ord G = 1 & G is finite
proof
thus G is trivial implies ord G = 1 & G is finite
proof
given x such that A1: the carrier of G = {x};
G is finite by A1,GROUP_1:def 13;
then ex B being finite set st B = the carrier of G & ord G = card B
by GROUP_1:def 14;
hence thesis by A1,CARD_1:79,GROUP_1:def 13;
end;
assume
A2: ord G = 1 & G is finite;
then consider c being finite set such that
A3: c = the carrier of G & ord G = card c by GROUP_1:def 14;
thus ex x st the carrier of G = {x} by A2,A3,CARD_2:60;
end;
theorem Th13:
for G being strict Group holds
G is trivial implies (1).G = G
proof let G be strict Group;
assume G is trivial;
then A1: ord G = 1 & G is finite by Th12;
then ord G = ord (1).G by GROUP_2:81;
hence G = (1).G by A1,GROUP_2:85;
end;
definition let G,N;
func Cosets N -> set equals
:Def3: Left_Cosets N;
coherence;
end;
definition let G,N;
cluster Cosets N -> non empty;
coherence
proof
Cosets N = Left_Cosets N by Def3;
hence thesis by GROUP_2:165;
end;
end;
theorem Th14:
for N being normal Subgroup of G holds
Cosets N = Left_Cosets N & Cosets N = Right_Cosets N
proof let N be normal Subgroup of G;
thus Cosets N = Left_Cosets N by Def3;
hence thesis by GROUP_3:150;
end;
theorem Th15:
for N being normal Subgroup of G holds
x in Cosets N implies ex a st x = a * N & x = N * a
proof let N be normal Subgroup of G;
assume x in Cosets N;
then x in Left_Cosets N by Def3;
then consider a such that A1: x = a * N by GROUP_2:def 15;
x = N * a by A1,GROUP_3:140;
hence thesis by A1;
end;
theorem Th16:
for N being normal Subgroup of G holds
a * N in Cosets N & N * a in Cosets N
proof let N be normal Subgroup of G;
A1: a * N in Left_Cosets N by GROUP_2:def 15;
N * a in Right_Cosets N by GROUP_2:def 16;
hence thesis by A1,Th14;
end;
theorem Th17:
for N being normal Subgroup of G holds
x in Cosets N implies x is Subset of G
proof let N be normal Subgroup of G;
assume x in Cosets N;
then ex a st x = a * N & x = N * a by Th15;
hence thesis;
end;
theorem Th18:
for N being normal Subgroup of G holds
A1 in Cosets N & A2 in Cosets N implies A1 * A2 in Cosets N
proof let N be normal Subgroup of G;
assume A1: A1 in Cosets N & A2 in Cosets N;
then consider a such that A2: A1 = a * N & A1 = N * a by Th15;
consider b such that A3: A2 = b * N & A2 = N * b by A1,Th15;
A1 * A2 = a * (N * (b * N)) by A2,A3,GROUP_3:11
.= a * (b * N * N) by A3,GROUP_3:15
.= a * (b * (N * N)) by GROUP_4:60
.= a * (b * carr N) by GROUP_4:58
.= a * (b * N) by GROUP_2:def 13
.= a * b * N by GROUP_2:127;
then A1 * A2 in Left_Cosets N by GROUP_2:def 15;
hence thesis by Th14;
end;
definition let G; let N be normal Subgroup of G;
func CosOp N -> BinOp of Cosets N means
:Def4: for W1,W2 being Element of Cosets N
for A1,A2 st W1 = A1 & W2 = A2 holds it.(W1,W2) = A1 * A2;
existence
proof
defpred P[Element of Cosets N,Element of Cosets N,set] means
for A1,A2 st $1 = A1 & $2 = A2 holds $3 = A1 * A2;
A1: for W1,W2 being Element of Cosets N
ex V being Element of Cosets N st P[W1,W2,V]
proof let W1,W2 be Element of Cosets N;
reconsider A1 = W1, A2 = W2 as Subset of G by Th17;
reconsider C = A1 * A2 as Element of Cosets N by Th18;
take C;
thus thesis;
end;
thus ex B being BinOp of Cosets N st
for W1,W2 being Element of Cosets N holds
P[W1,W2,B.(W1,W2)] from BinOpEx(A1);
end;
uniqueness
proof let o1,o2 be BinOp of Cosets N;
assume A2: for W1,W2 being Element of Cosets N
for A1,A2 st W1 = A1 & W2 = A2 holds o1.(W1,W2) = A1 * A2;
assume A3: for W1,W2 being Element of Cosets N
for A1,A2 st W1 = A1 & W2 = A2 holds o2.(W1,W2) = A1 * A2;
now let x,y be set;
assume A4: x in Cosets N & y in Cosets N;
then reconsider W = x, V = y as Element of Cosets N;
reconsider A1 = x, A2 = y as Subset of G by A4,Th17;
o1.(W,V) = A1 * A2 & o2.(W,V) = A1 * A2 by A2,A3;
then o1.(x,y) = o2.(x,y) & o1. [x,y] = o1.(x,y) & o2. [x,y] = o2.(x,y)
by BINOP_1:def 1;
hence o1. [x,y] = o2. [x,y];
end;
hence thesis by FUNCT_2:118;
end;
end;
definition let G; let N be normal Subgroup of G;
func G./.N -> HGrStr equals
:Def5: HGrStr (# Cosets N, CosOp N #);
correctness;
end;
definition let G; let N be normal Subgroup of G;
cluster G./.N -> strict non empty;
coherence
proof
G./.N = HGrStr (# Cosets N, CosOp N #) by Def5;
hence G./.N is strict & the carrier of G./.N is non empty;
end;
end;
canceled 3;
theorem Th22:
for N being normal Subgroup of G holds
the carrier of G./.N = Cosets N
proof let N be normal Subgroup of G;
G./.N = HGrStr (# Cosets N, CosOp N #) by Def5;
hence thesis;
end;
theorem Th23:
for N being normal Subgroup of G holds
the mult of G./.N = CosOp N
proof let N be normal Subgroup of G;
G./.N = HGrStr (# Cosets N, CosOp N #) by Def5;
hence thesis;
end;
reserve N for normal Subgroup of G;
reserve S,T1,T2 for Element of G./.N;
definition
let G,N,S;
func @S -> Subset of G equals :Def6: S;
coherence
proof
S is Element of Cosets N by Th22;
hence thesis by Th17;
end;
end;
theorem Th24:
for N being normal Subgroup of G, T1,T2 being Element of G./.N
holds @T1 * @T2 = T1 * T2
proof
let N be normal Subgroup of G, T1,T2 be Element of G./.N;
reconsider S1 = T1 as Element of Cosets N by Th22;
reconsider S2 = T2 as Element of Cosets N by Th22;
S1 = @T1 & S2 = @T2 by Def6;
hence @T1 * @T2 = (CosOp N).(T1,T2) by Def4
.= (the mult of G./.N).(T1,T2) by Th23
.= T1 * T2 by VECTSP_1:def 10;
end;
theorem Th25:
@(T1 * T2) = @T1 * @T2
proof
thus @(T1 * T2) = T1 * T2 by Def6
.= @T1 * @T2 by Th24;
end;
definition let G; let N be normal Subgroup of G;
cluster G./.N -> associative Group-like;
coherence
proof A1: the carrier of G./.N = Cosets N by Th22;
G./.N is associative Group-like
proof
thus for f,g,h being Element of G./.N
holds f * (g * h) = f * g * h
proof let f,g,h be Element of G./.N;
consider a such that A2: f = a * N & f = N * a by A1,Th15;
consider c being Element of G such that
A3: h = c * N & h = N * c by A1,Th15;
A4: @f = f & @g = g & @h = h by Def6;
thus f * (g * h) = @f * @(g * h) by Th24
.= (a * N) * (@g * @h) by A2,A4,Th25
.= @f * @g * (c * N) by A2,A3,A4,GROUP_2:14
.= @(f * g) * @h by A3,A4,Th25
.= f * g * h by Th24;
end;
A5: carr N in Left_Cosets N & Cosets N = Left_Cosets N
by Th14,GROUP_2:165;
then reconsider e = carr N as Element of G./.N by Th22;
take e;
let h be Element of G./.N;
consider a such that A6: h = a * N & h = N * a by A1,Th15;
A7: @h = h & @e = e by Def6;
thus h * e = @h * @e by Th24
.= (a * N) * N by A6,A7,GROUP_2:def 11
.= a * (N * N) by GROUP_4:60
.= a * carr N by GROUP_4:58
.= h by A6,GROUP_2:def 13;
thus e * h = @e * @h by Th24
.= N * (N * a) by A6,A7,GROUP_2:def 12
.= N * N * a by GROUP_4:61
.= carr N * a by GROUP_4:58
.= h by A6,GROUP_2:def 14;
reconsider g = a" * N as Element of G./.N by A1,A5,GROUP_2:
def 15;
A8: @g = g by Def6;
take g;
thus h * g = N * a * (a" * N) by A6,A7,A8,Th24
.= N * a * a" * N by GROUP_3:10
.= N * (a * a") * N by GROUP_2:129
.= N * 1.G * N by GROUP_1:def 5
.= carr N * N by GROUP_2:132
.= carr N * carr N by GROUP_2:def 11
.= e by GROUP_2:91;
thus g * h = @g * @h by Th24
.= a" * N * a * N by A6,A7,A8,GROUP_3:10
.= a" * (N * a) * N by GROUP_2:128
.= a" * (a * N) * N by GROUP_3:140
.= a" * a * N * N by GROUP_2:127
.= 1.G * N * N by GROUP_1:def 5
.= 1.G * (N * N) by GROUP_4:60
.= 1.G * carr N by GROUP_4:58
.= e by GROUP_2:43;
end;
hence thesis;
end;
end;
theorem Th26:
for N being normal Subgroup of G, S being Element of G./.N
ex a st S = a * N & S = N * a
proof let N be normal Subgroup of G, S be Element of G./.N;
S in the carrier of G./.N & the carrier of G./.N = Cosets N by Th22;
hence thesis by Th15;
end;
theorem Th27:
N * a is Element of G./.N &
a * N is Element of G./.N &
carr N is Element of G./.N
proof N * a in Cosets N & a * N in
Cosets N & Cosets N = the carrier of G./.N &
carr N in Left_Cosets N & Cosets N = Left_Cosets N
by Th14,Th16,Th22,GROUP_2:165;
hence thesis;
end;
theorem Th28:
for N being normal Subgroup of G holds
x in G./.N iff ex a st x = a * N & x = N * a
proof let N be normal Subgroup of G;
thus x in G./.N implies ex a st x = a * N & x = N * a
proof assume x in G./.N;
then x is Element of G./.N by RLVECT_1:def 1;
hence thesis by Th26;
end;
given a such that A1: x = a * N & x = N * a;
x is Element of G./.N by A1,Th27;
hence thesis by RLVECT_1:def 1;
end;
theorem Th29:
for N being normal Subgroup of G holds
1.(G./.N) = carr N
proof let N be normal Subgroup of G;
reconsider e = carr N as Element of G./.N by Th27;
A1: the carrier of G./.N = Cosets N by Th22;
now let h be Element of G./.N;
consider a such that A2: h = a * N & h = N * a by A1,Th15;
A3: @h = h & @e = e by Def6;
thus h * e = @h * @e by Th24
.= (a * N) * N by A2,A3,GROUP_2:def 11
.= a * (N * N) by GROUP_4:60
.= a * carr N by GROUP_4:58
.= h by A2,GROUP_2:def 13;
thus e * h = @e * @h by Th24
.= N * (N * a) by A2,A3,GROUP_2:def 12
.= N * N * a by GROUP_4:61
.= carr N * a by GROUP_4:58
.= h by A2,GROUP_2:def 14;
end;
hence thesis by GROUP_1:10;
end;
theorem Th30:
for N being normal Subgroup of G, S being Element of G./.N
holds S = a * N implies S" = a" * N
proof let N be normal Subgroup of G, S be Element of G./.N;
assume A1: S = a * N;
reconsider g = a" * N as Element of G./.N by Th27;
A2: @g = g by Def6;
A3: @S = S by Def6;
A4: S * g = @S * @g by Th24
.= N * a * (a" * N) by A1,A2,A3,GROUP_3:140
.= N * a * a" * N by GROUP_3:10
.= N * (a * a") * N by GROUP_2:129
.= N * 1.G * N by GROUP_1:def 5
.= carr N * N by GROUP_2:132
.= carr N * carr N by GROUP_2:def 11
.= carr N by GROUP_2:91;
A5: g * S = @g * @S by Th24
.= a" * N * a * N by A1,A2,A3,GROUP_3:10
.= a" * (N * a) * N by GROUP_2:128
.= a" * (a * N) * N by GROUP_3:140
.= a" * a * N * N by GROUP_2:127
.= 1.G * N * N by GROUP_1:def 5
.= 1.G * (N * N) by GROUP_4:60
.= 1.G * carr N by GROUP_4:58
.= carr N by GROUP_2:43;
1.(G./.N) = carr N by Th29;
hence thesis by A4,A5,GROUP_1:def 5;
end;
theorem Th31:
for N being normal Subgroup of G holds
Left_Cosets N is finite implies G./.N is finite
proof let N be normal Subgroup of G;
assume Left_Cosets N is finite;
then Cosets N is finite by Th14;
then the carrier of G./.N is finite by Th22;
hence thesis by GROUP_1:def 13;
end;
theorem
for N being normal Subgroup of G holds
Ord(G./.N) = Index N
proof let N be normal Subgroup of G;
thus Ord(G./.N) = Card(the carrier of G./.N) by GROUP_1:def 12
.= Card Cosets N by Th22
.= Card Left_Cosets N by Th14
.= Index N by GROUP_2:175;
end;
theorem
for N being normal Subgroup of G holds
Left_Cosets N is finite implies ord(G./.N) = index N
proof let N be normal Subgroup of G;
assume A1: Left_Cosets N is finite;
then reconsider LC = Left_Cosets N as finite set;
A2: Cosets N = LC by Th14;
A3: G./.N is finite by A1,Th31;
then reconsider GN = the carrier of G./.N as finite set by GROUP_1:def 13;
thus ord(G./.N) = card GN by A3,GROUP_1:def 14
.= card LC by A2,Th22
.= index N by GROUP_2:def 18;
end;
theorem Th34:
for M being strict normal Subgroup of G holds
M is Subgroup of B implies B./.(B,M)`*` is Subgroup of G./.M
proof let M be strict normal Subgroup of G;
assume A1: M is Subgroup of B;
set I = B./.(B,M)`*`; set J = (B,M)`*`;
A2: the carrier of I c= the carrier of G./.M
proof let x;
assume A3: x in the carrier of I;
the carrier of I = Cosets((B,M)`*`) by Th22;
then consider a being Element of B such that
A4: x = a * J & x = J * a by A3,Th15;
reconsider b = a as Element of G by GROUP_2:51;
J = M by A1,Def1;
then a * J = b * M & J * a = M * b by Th2;
then x in Cosets M & the carrier of G./.M = Cosets M by A4,Th16,Th22
;
hence thesis;
end;
set g = the mult of I;
set f = the mult of G./.M;
set X = [: the carrier of I,the carrier of I :];
A5: dom g = X & dom f = [: the carrier of G./.M,the carrier of G./.M :] &
X c= [: the carrier of G./.M,the carrier of G./.M :]
by A2,FUNCT_2:def 1,ZFMISC_1:119;
then A6: dom g = dom f /\ X by XBOOLE_1:28;
now let x;
assume A7: x in dom g;
then consider y,z such that A8: [y,z] = x by A5,ZFMISC_1:102;
A9: y in the carrier of I & z in
the carrier of I by A5,A7,A8,ZFMISC_1:106;
A10: the carrier of I = Cosets((B,M)`*`) by Th22;
then consider a being Element of B such that
A11: y = a * J & y = J * a by A9,Th15;
consider b being Element of B such that
A12: z = b * J & z = J * b by A9,A10,Th15;
reconsider W1 = y, W2 = z as Element of Cosets J by A11,A12,Th16;
A13: the mult of I = CosOp J & the mult of G./.M = CosOp M by Th23;
A14: g.x = g.(W1,W2) by A8,BINOP_1:def 1
.= (a * J) * (J * b) by A11,A12,A13,Def4
.= a * J * J * b by GROUP_3:12
.= a * (J * J) * b by GROUP_4:60
.= a * carr J * b by GROUP_4:58
.= a * J * b by GROUP_2:def 13
.= a * (J * b) by GROUP_2:128
.= a * (b * J) by GROUP_3:140
.= a * b * J by GROUP_2:127;
reconsider a' = a, b' = b as Element of G
by GROUP_2:51;
A15: J = M by A1,Def1;
then A16: y = a' * M & y = M * a' & z = b' * M & z = M * b' by A11,
A12,Th2;
then reconsider V1 = y, V2 = z as Element of Cosets M by Th16;
A17: f.x = f.(V1,V2) by A8,BINOP_1:def 1
.= (a' * M) * (M * b') by A13,A16,Def4
.= a' * M * M * b' by GROUP_3:12
.= a' * (M * M) * b' by GROUP_4:60
.= a' * carr M * b' by GROUP_4:58
.= a' * M * b' by GROUP_2:def 13
.= a' * (M * b') by GROUP_2:128
.= a' * (b' * M) by GROUP_3:140
.= a' * b' * M by GROUP_2:127;
a' * b' = a * b by GROUP_2:52;
hence g.x = f.x by A14,A15,A17,Th2;
end;
then g = f | X by A6,FUNCT_1:68;
hence thesis by A2,GROUP_2:def 5;
end;
theorem
for N,M being strict normal Subgroup of G holds
M is Subgroup of N implies N./.(N,M)`*` is normal Subgroup of G./.M
proof let N,M be strict normal Subgroup of G;
assume A1: M is Subgroup of N;
then A2: (N,M)`*` = M by Def1;
reconsider J = N./.(N,M)`*` as Subgroup of G./.M by A1,Th34;
reconsider I = M as normal Subgroup of N by A2;
now let S be Element of G./.M;
thus S * J c= J * S
proof let x;
assume x in S * J;
then consider T being Element of G./.M such that
A3: x = S * T and A4: T in J by GROUP_2:125;
consider a such that A5: S = a * M & S = M * a by Th26;
consider c being Element of N such that
A6: T = c * I & T = I * c by A2,A4,Th28;
reconsider d = c as Element of G by GROUP_2:51;
set e = a * (d * a");
A7: c in N by RLVECT_1:def 1;
e = d |^ a" by Th4;
then e in N by A7,GROUP_5:3;
then reconsider f = e as Element of N
by RLVECT_1:def 1;
reconsider V = I * f as Element of J by A2,Th27;
A8: V in J by RLVECT_1:def 1;
reconsider V as Element of G./.M by GROUP_2:51;
A9: @S = S & @T = T & c * I = d * M & M * d = I * c & M * e = I * f &
@V = V by Def6,Th2;
then x = M * a * (M * d) by A3,A5,A6,Th24
.= M * a * (M * d * 1.G) by GROUP_2:43
.= M * a * (M * d * (a" * a)) by GROUP_1:def 5
.= M * a * (M * (d * (a" * a))) by GROUP_2:129
.= M * a * M * (d * (a" * a)) by GROUP_3:12
.= M * (a * M) * (d * (a" * a)) by GROUP_3:15
.= M * (M * a) * (d * (a" * a)) by GROUP_3:140
.= M * ((M * a) * (d * (a" * a))) by GROUP_3:14
.= M * (M * (a * (d * (a" * a)))) by GROUP_2:129
.= M * (M * (a * (d * a" * a))) by VECTSP_1:def 16
.= M * (M * (a * (d * a") * a)) by VECTSP_1:def 16
.= M * (M * e * a) by GROUP_2:129
.= M * (e * M * a) by GROUP_3:140
.= M * (e * (M * a)) by GROUP_2:128
.= M * e * (M * a) by GROUP_3:13
.= V * S by A5,A9,Th24;
hence x in J * S by A8,GROUP_2:126;
end;
end;
hence thesis by GROUP_3:141;
end;
theorem
for G being strict Group, N be strict normal Subgroup of G holds
G./.N is commutative Group iff G` is Subgroup of N
proof let G be strict Group, N be strict normal Subgroup of G;
thus G./.N is commutative Group implies G` is Subgroup of N
proof assume A1: G./.N is commutative Group;
now let a,b be Element of G;
reconsider S = a * N,T = b * N as Element of G./.N
by Th27;
S" = @(S") & T" = @(T") & S" = a" * N & T" = b" * N by Def6,Th30;
then A2: S" * T" = (a" * N) * (b" * N) by Th24;
S = @S & T = @T by Def6;
then A3: S * T = (a * N) * (b * N) by Th24;
A4: @(S" * T") = (S" * T") & @(S * T) = (S * T) by Def6;
[.S,T.] = (S" * T") * (S * T) by GROUP_5:19;
then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) &
[.S,T.] = 1.(G./.N) & 1.(G./.N) = carr N by A1,A2,A3,A4,Th24,Th29
,GROUP_5:40;
then carr N = (a" * N) * (b" * N) * (a * (N * (b * N))) by GROUP_3:11
.= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:15
.= (a" * N) * (b" * N) * (a * (b * N * N)) by GROUP_3:140
.= (a" * N) * (b" * N) * (a * (b * N)) by Th6
.= (a" * N) * (b" * N) * (a * b * N) by GROUP_2:127
.= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:11
.= a" * (N * b" * N) * (a * b * N) by GROUP_3:15
.= a" * (b" * N * N) * (a * b * N) by GROUP_3:140
.= a" * (b" * N) * (a * b * N) by Th6
.= (a" * b" * N) * (a * b * N) by GROUP_2:127
.= (a" * b") * (N * (a * b * N)) by GROUP_3:11
.= (a" * b") * (N * (a * b) * N) by GROUP_3:15
.= (a" * b") * ((a * b) * N * N) by GROUP_3:140
.= (a" * b") * ((a * b) * N) by Th6
.= (a" * b") * (a * b) * N by GROUP_2:127
.= [.a,b.] * N by GROUP_5:19;
hence [.a,b.] in N by GROUP_2:136;
end;
hence thesis by Th8;
end;
assume A5: G` is Subgroup of N;
now let S,T be Element of G./.N;
consider a being Element of G such that
A6: S = a * N & S = N * a by Th26;
consider b being Element of G such that
A7: T = b * N & T = N * b by Th26;
[.a,b.] in N by A5,Th8;
then A8: carr N = [.a,b.] * N by GROUP_2:136
.= (a" * b") * (a * b) * N by GROUP_5:19
.= (a" * b") * ((a * b) * N) by GROUP_2:127
.= (a" * b") * ((a * b) * N * N) by Th6
.= (a" * b") * (N * (a * b) * N) by GROUP_3:140
.= (a" * b") * (N * (a * b * N)) by GROUP_3:15
.= (a" * b" * N) * (a * b * N) by GROUP_3:11
.= a" * (b" * N) * (a * b * N) by GROUP_2:127
.= a" * (b" * N * N) * (a * b * N) by Th6
.= a" * (N * b" * N) * (a * b * N) by GROUP_3:140
.= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:15
.= (a" * N) * (b" * N) * (a * b * N) by GROUP_3:11
.= (a" * N) * (b" * N) * (a * (b * N)) by GROUP_2:127
.= (a" * N) * (b" * N) * (a * (b * N * N)) by Th6
.= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:140
.= (a" * N) * (b" * N) * (a * (N * (b * N))) by GROUP_3:15
.= (a" * N) * (b" * N) * (a * N * (b * N)) by GROUP_3:11;
S" = @(S") & T" = @(T") & S" = a" * N & T" = b" * N by A6,A7,Def6,
Th30
;
then A9: S" * T" = (a" * N) * (b" * N) by Th24;
S = @S & T = @T by Def6;
then A10: S * T = (a * N) * (b * N) by A6,A7,Th24;
A11: @(S" * T") = (S" * T") & @(S * T) = (S * T) by Def6;
[.S,T.] = (S" * T") * (S * T) by GROUP_5:19;
then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) &
1.(G./.N) = carr N by A9,A10,A11,Th24,Th29;
hence [.S,T.] = 1.(G./.N) by A8;
end;
hence thesis by GROUP_5:40;
end;
Lm1: (for a holds f.a = 1.H) implies f.(a * b) = f.a * f.b
proof
assume A1: for a holds f.a = 1.H;
hence f.(a * b) = 1.H
.= 1.H * 1.H by GROUP_1:def 4
.= f.a * 1.H by A1
.= f.a * f.b by A1;
end;
definition let G,H;
mode Homomorphism of G,H ->
Function of the carrier of G, the carrier of H means
:Def7: it.(a * b) = it.a * it.b;
existence
proof
deffunc F(Element of G) = 1.H;
consider f such that A1: for a holds f.a = F(a) from LambdaD;
take f;
thus thesis by A1,Lm1;
end;
end;
reserve g,h for Homomorphism of G,H;
reserve g1 for Homomorphism of H,G;
reserve h1 for Homomorphism of H,I;
canceled 3;
theorem Th40:
g.(1.G) = 1.H
proof g.(1.G) = g.(1.G * 1.G) by GROUP_1:def 4
.= g.(1.G) * g.(1.G) by Def7;
hence thesis by GROUP_1:15;
end;
theorem Th41:
g.(a") = (g.a)"
proof g.(a") * g.a = g.(a" * a) by Def7
.= g.(1.G) by GROUP_1:def 5
.= 1.H by Th40;
hence thesis by GROUP_1:20;
end;
theorem Th42:
g.(a |^ b) = (g.a) |^ (g.b)
proof
thus g.(a |^ b) = g.(b" * a * b) by GROUP_3:def 2
.= g.(b" * a) * g.b by Def7
.= g.(b") * g.a * g.b by Def7
.= (g.b)" * g.a * g.b by Th41
.= (g.a) |^ (g.b) by GROUP_3:def 2;
end;
theorem Th43:
g. [.a,b.] = [.g.a,g.b.]
proof
thus g. [.a,b.] = g.(a" * b" * a * b) by GROUP_5:19
.= g.(a" * b" * a) * g.b by Def7
.= g.(a" * b") * g.a * g.b by Def7
.= g.(a") * g.(b") * g.a * g.b by Def7
.= (g.a)" * g.(b") * g.a * g.b by Th41
.= (g.a)" * (g.b)" * g.a * g.b by Th41
.= [.g.a,g.b.] by GROUP_5:19;
end;
theorem
g. [.a1,a2,a3.] = [.g.a1,g.a2,g.a3.]
proof
thus g. [.a1,a2,a3.] = g. [.[.a1,a2.],a3.] by GROUP_5:def 3
.= [.g. [.a1,a2.],g.a3.] by Th43
.= [.[.g.a1,g.a2.],g.a3.] by Th43
.= [.g.a1,g.a2,g.a3.] by GROUP_5:def 3;
end;
theorem Th45:
g.(a |^ n) = (g.a) |^ n
proof
defpred Q[Nat] means g.(a |^ $1) = (g.a) |^ $1;
A1: Q[0]
proof
thus g.(a |^ 0) = g.(1.G) by GROUP_1:43
.= 1.H by Th40
.= (g.a) |^ 0 by GROUP_1:43;
end;
A2: for n st Q[n] holds Q[n + 1]
proof
let n;
assume A3: Q[n];
thus g.(a |^ (n + 1)) = g.(a |^ n * a) by GROUP_1:49
.= (g.a) |^ n * g.a by A3,Def7
.= (g.a) |^ (n + 1) by GROUP_1:49;
end;
for n holds Q[n] from Ind(A1,A2);
hence thesis;
end;
theorem
g.(a |^ i) = (g.a) |^ i
proof
now per cases;
suppose A1: i >= 0;
hence g.(a |^ i) = g.(a |^ abs( i )) by GROUP_1:55
.= (g.a) |^ abs( i ) by Th45
.= (g.a) |^ i by A1,GROUP_1:55;
suppose A2: i < 0;
hence g.(a |^ i) = g.(a |^ abs( i ))" by GROUP_1:56
.= (g.(a |^ abs( i )))" by Th41
.= ((g.a) |^ abs( i ))" by Th45
.= (g.a) |^ i by A2,GROUP_1:56;
end;
hence thesis;
end;
theorem Th47:
id the carrier of G is Homomorphism of G,G
proof
reconsider f = id the carrier of G
as Function of the carrier of G, the carrier of G;
now
let a,b;
thus f.(a * b) = a * b by FUNCT_1:35
.= f.a * b by FUNCT_1:35
.= f.a * f.b by FUNCT_1:35;
end;
hence thesis by Def7;
end;
theorem Th48:
h1 * h is Homomorphism of G,I
proof
reconsider f = h1 * h as
Function of the carrier of G, the carrier of I;
now
let a,b;
thus
f.(a * b) = h1.(h.(a * b)) by FUNCT_2:21
.= h1.(h.a * h.b) by Def7
.= (h1.(h.a)) * (h1.(h.b)) by Def7
.= f.a * (h1.(h.b)) by FUNCT_2:21
.= f.a * f.b by FUNCT_2:21;
end;
hence thesis by Def7;
end;
definition let G,H,I,h,h1;
redefine func h1 * h -> Homomorphism of G,I;
coherence by Th48;
end;
definition let G,H,g;
redefine func rng g -> Subset of H;
coherence by RELSET_1:12;
end;
definition let G,H;
func 1:(G,H) -> Homomorphism of G,H means
:Def8: for a holds it.a = 1.H;
existence
proof
deffunc F(Element of G) = 1.H;
consider f such that
A1: for a holds f.a = F(a) from LambdaD;
f.(a * b) = f.a * f.b by A1,Lm1;
then reconsider g = f as Homomorphism of G,H by Def7;
take g;
thus thesis by A1;
end;
uniqueness
proof
let g,h be Homomorphism of G,H such that
A2: for a holds g.a = 1.H and
A3: for a holds h.a = 1.H;
for a holds g.a = h.a
proof
let a;
g.a = 1.H & h.a = 1.H by A2,A3;
hence thesis;
end;
hence thesis by FUNCT_2:113;
end;
end;
theorem
h1 * 1:(G,H) = 1:(G,I) & 1:(H,I) * h = 1:(G,I)
proof
A1: now let a;
thus (h1 * 1:(G,H)).a = h1.(1:(G,H).a) by FUNCT_2:21
.= h1.(1.H) by Def8
.= 1.I by Th40;
end;
now let a;
thus (1:(H,I) * h).a = 1:(H,I).(h.a) by FUNCT_2:21
.= 1.I by Def8;
end;
hence thesis by A1,Def8;
end;
definition let G; let N be normal Subgroup of G;
func nat_hom N -> Homomorphism of G,G./.N means
:Def9: for a holds it.a = a * N;
existence
proof
defpred P[set,set] means ex a st $1 = a & $2 = a * N;
A1: for x,y1,y2 st x in the carrier of G & P[x,y1] & P[x,y2] holds
y1 = y2;
A2: for x st x in the carrier of G ex y st P[x,y]
proof let x;
assume x in the carrier of G;
then reconsider a = x as Element of G;
reconsider y = a * N as set;
take y;
take a;
thus thesis;
end;
consider f being Function such that A3: dom f = the carrier of G and
A4: for x st x in the carrier of G holds P[x,f.x] from FuncEx(A1,A2);
rng f c= the carrier of G./.N
proof let x;
assume x in rng f;
then consider y such that A5: y in
dom f and A6: f.y = x by FUNCT_1:def 5;
consider a such that A7: y = a & f.y = a * N by A3,A4,A5;
a * N = N * a by GROUP_3:140;
then x in G./.N by A6,A7,Th28;
hence thesis by RLVECT_1:def 1;
end;
then reconsider f as Function of the carrier of G, the carrier of G./.N
by A3,FUNCT_2:def 1,RELSET_1:11
;
now let a,b;
consider a1 such that A8: a = a1 & f.a = a1 * N by A4;
consider b1 such that A9: b = b1 & f.b = b1 * N by A4;
A10: ex c being Element of G
st c = a * b & f.(a * b) = c * N by A4;
A11: @(f.a) = f.a & @(f.b) = f.b by Def6;
thus f.a * f.b = @(f.a) * @(f.b) by Th24
.= (a1 * N) * b1 * N by A8,A9,A11,GROUP_3:10
.= a1 * (N * b1) * N by GROUP_2:128
.= a1 * (b1 * N) * N by GROUP_3:140
.= a1 * ((b1 * N) * N) by GROUP_3:9
.= a1 * (b1 * N) by Th6
.= f.(a * b) by A8,A9,A10,GROUP_2:127;
end;
then reconsider f as Homomorphism of G,G./.N by Def7;
take f;
let a;
ex b st a = b & f.a = b * N by A4;
hence thesis;
end;
uniqueness
proof let n1,n2 be Homomorphism of G,G./.N such that
A12: for a holds n1.a = a * N and
A13: for a holds n2.a = a * N;
now let a;
n1.a = a * N & n2.a = a * N by A12,A13;
hence n1.a = n2.a;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition let G,H,g;
func Ker g -> strict Subgroup of G means
:Def10: the carrier of it = {a : g.a = 1.H};
existence
proof
defpred P[set] means g.$1 = 1.H;
reconsider A = {a : P[a]} as Subset of G from SubsetD;
g.(1.G) = 1.H by Th40;
then A1: 1.G in A;
A2: now let a,b;
assume that A3: a in A and A4: b in A;
A5: ex a1 st a1 = a & g.a1 = 1.H by A3;
A6: ex b1 st b1 = b & g.b1 = 1.H by A4;
g.(a * b) = g.a * g.b by Def7
.= 1.H by A5,A6,GROUP_1:def 4;
hence a * b in A;
end;
now let a;
assume a in A;
then ex a1 st a1 = a & g.a1 = 1.H;
then g.(a") = (1.H)" by Th41
.= 1.H by GROUP_1:16;
hence a" in A;
end;
then consider B being strict Subgroup of G such that
A7: the carrier of B = A by A1,A2,GROUP_2:61;
reconsider B as strict Subgroup of G;
take B;
thus thesis by A7;
end;
uniqueness by GROUP_2:68;
end;
definition let G,H,g;
cluster Ker g -> normal;
coherence
proof
defpred P[set] means g.$1 = 1.H;
reconsider A = {a : P[a]} as Subset of G from SubsetD;
g.(1.G) = 1.H by Th40;
then A1: 1.G in A;
A2: now let a,b;
assume that A3: a in A and A4: b in A;
A5: ex a1 st a1 = a & g.a1 = 1.H by A3;
A6: ex b1 st b1 = b & g.b1 = 1.H by A4;
g.(a * b) = g.a * g.b by Def7
.= 1.H by A5,A6,GROUP_1:def 4;
hence a * b in A;
end;
now let a;
assume a in A;
then ex a1 st a1 = a & g.a1 = 1.H;
then g.(a") = (1.H)" by Th41
.= 1.H by GROUP_1:16;
hence a" in A;
end;
then consider B being strict Subgroup of G such that
A7: the carrier of B = A by A1,A2,GROUP_2:61;
now let a;
now let b;
assume b in B |^ a;
then consider c being Element of G such that
A8: b = c |^ a and A9: c in B by GROUP_3:70;
c in A by A7,A9,RLVECT_1:def 1;
then ex a1 st c = a1 & g.a1 = 1.H;
then g.b = (1.H) |^ (g.a) by A8,Th42
.= 1.H by GROUP_3:22;
then b in A;
hence b in B by A7,RLVECT_1:def 1;
end;
hence B |^ a is Subgroup of B by GROUP_2:67;
end;
then B is normal Subgroup of G by GROUP_3:145;
hence thesis by A7,Def10;
end;
end;
theorem Th50:
a in Ker h iff h.a = 1.H
proof
thus a in Ker h implies h.a = 1.H
proof
assume a in Ker h;
then a in the carrier of Ker h by RLVECT_1:def 1;
then a in {b : h.b = 1.H} by Def10;
then ex b st a = b & h.b = 1.H;
hence thesis;
end;
assume h.a = 1.H;
then a in {b : h.b = 1.H};
then a in the carrier of Ker h by Def10;
hence thesis by RLVECT_1:def 1;
end;
theorem
for G,H being strict Group holds
Ker 1:(G,H) = G
proof let G,H be strict Group;
now let a be Element of G;
1:(G,H).a = 1.H by Def8;
hence a in Ker 1:(G,H) by Th50;
end;
hence thesis by GROUP_2:71;
end;
theorem Th52:
for N being strict normal Subgroup of G holds
Ker nat_hom N = N
proof let N be strict normal Subgroup of G;
let a;
thus a in Ker nat_hom N implies a in N
proof assume a in Ker nat_hom N;
then (nat_hom N).a = 1.(G./.N) & (nat_hom N).a = a * N &
1.(G./.N) = carr N by Def9,Th29,Th50;
hence a in N by GROUP_2:136;
end;
assume a in N;
then a * N = carr N & (nat_hom N).a = a * N &
1.(G./.N) = carr N by Def9,Th29,GROUP_2:136;
hence thesis by Th50;
end;
definition let G,H,g;
func Image g -> strict Subgroup of H means
:Def11: the carrier of it = g .: (the carrier of G);
existence
proof
the carrier of G c= the carrier of G;
then reconsider X = the carrier of G as Subset of G;
set S = g .: X;
A1: dom g = the carrier of G & X /\ X = X & X <> {} by FUNCT_2:def 1;
then X meets X by XBOOLE_0:def 7;
then A2: S <> {} by A1,RELAT_1:151;
A3: now let c,d;
assume that A4: c in S and A5: d in S;
consider a such that a in X and A6: c = g.a by A4,FUNCT_2:116;
consider b such that b in X and A7: d = g.b by A5,FUNCT_2:116;
c * d = g.(a * b) & a * b in the carrier of G by A6,A7,Def7;
hence c * d in S by FUNCT_2:43;
end;
now let c;
assume c in S;
then consider a such that a in X and A8: c = g.a by FUNCT_2:116;
a" in the carrier of G & g.(a") = c" by A8,Th41;
hence c" in S by FUNCT_2:43;
end;
then consider D being strict Subgroup of H such that
A9: the carrier of D = S by A2,A3,GROUP_2:61;
take D;
thus thesis by A9;
end;
uniqueness by GROUP_2:68;
end;
theorem Th53:
rng g = the carrier of Image g
proof
the carrier of Image g = g .: (the carrier of G) by Def11
.= g .: (dom g) by FUNCT_2:def 1
.= rng g by RELAT_1:146;
hence thesis;
end;
theorem Th54:
x in Image g iff ex a st x = g.a
proof
thus x in Image g implies ex a st x = g.a
proof assume x in Image g;
then x in the carrier of Image g by RLVECT_1:def 1;
then x in g .: (the carrier of G) by Def11;
then consider y such that y in dom g and A1: y in the carrier of G and
A2: g.y = x by FUNCT_1:def 12;
reconsider y as Element of G by A1;
take y;
thus thesis by A2;
end;
given a such that A3: x = g.a;
a in the carrier of G & the carrier of G = dom g by FUNCT_2:def 1;
then x in g .: (the carrier of G) by A3,FUNCT_1:def 12;
then x in the carrier of Image g by Def11;
hence thesis by RLVECT_1:def 1;
end;
theorem
Image g = gr rng g
proof
rng g = the carrier of Image g & the carrier of Image g = carr Image g
by Th53,GROUP_2:def
9;
hence thesis by GROUP_4:40;
end;
theorem
Image 1:(G,H) = (1).H
proof set g = 1:(G,H);
1.H in Image g by GROUP_2:55;
then 1.H in the carrier of Image g by RLVECT_1:def 1;
then A1: {1.H} c= the carrier of Image g by ZFMISC_1:37;
the carrier of Image g c= {1.H}
proof let x;
assume x in the carrier of Image g;
then x in g .: (the carrier of G) by Def11;
then consider y such that y in dom g and A2: y in the carrier of G and
A3: g.y = x by FUNCT_1:def 12;
reconsider y as Element of G by A2;
g.y = 1.H by Def8;
hence thesis by A3,TARSKI:def 1;
end;
then the carrier of Image g = {1.H} by A1,XBOOLE_0:def 10;
hence thesis by GROUP_2:def 7;
end;
theorem Th57:
for N being normal Subgroup of G holds
Image nat_hom N = G./.N
proof let N be normal Subgroup of G;
now let S be Element of G./.N;
consider a such that A1: S = a * N & S = N * a by Th26;
(nat_hom N).a = a * N by Def9;
hence S in Image nat_hom N by A1,Th54;
end;
hence thesis by GROUP_2:71;
end;
theorem Th58:
h is Homomorphism of G,Image h
proof
h is Function of the carrier of G, the carrier of Image h
proof
A1: rng h = the carrier of Image h by Th53;
dom h = the carrier of G by FUNCT_2:def 1;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:11;
end;
then reconsider f' = h as
Function of the carrier of G, the carrier of Image h;
now
let a,b;
thus f'.a * f'.b = h.a * h.b by GROUP_2:52
.= f'.(a * b) by Def7;
end;
hence thesis by Def7;
end;
theorem Th59:
G is finite implies Image g is finite
proof
assume G is finite;
then the carrier of G is finite by GROUP_1:def 13;
then g .: (the carrier of G) is finite by FINSET_1:17;
then the carrier of Image g is finite by Def11;
hence thesis by GROUP_1:def 13;
end;
Lm2: for A be commutative Group, a, b be Element of A
holds a * b = b * a;
theorem
G is commutative Group implies Image g is commutative
proof assume A1: G is commutative Group;
let h1,h2 be Element of Image g;
reconsider c = h1, d = h2 as Element of H by GROUP_2:51;
h1 in Image g by RLVECT_1:def 1;
then consider a such that A2: h1 = g.a by Th54;
h2 in Image g by RLVECT_1:def 1;
then consider b such that A3: h2 = g.b by Th54;
thus h1 * h2 = c * d by GROUP_2:52
.= g.(a * b) by A2,A3,Def7
.= g.(b * a) by A1,Lm2
.= d * c by A2,A3,Def7
.= h2 * h1 by GROUP_2:52;
end;
theorem Th61:
Ord Image g <=` Ord G
proof
A1: Card (g .: (the carrier of G)) <=` Card (the carrier of G) by CARD_2:3;
Ord Image g = Card (the carrier of Image g) by GROUP_1:def 12
.= Card (g .: (the carrier of G)) by Def11;
hence thesis by A1,GROUP_1:def 12;
end;
theorem
G is finite implies ord Image g <= ord G
proof
assume A1: G is finite;
then A2: Image g is finite by Th59;
consider c being finite set such that
A3: c = the carrier of G & ord G = card c by A1,GROUP_1:def 14;
consider ci being finite set such that
A4: ci = the carrier of Image g & ord Image g = card ci by A2,GROUP_1:def 14;
Ord Image g <=` Ord G by Th61;
then Card (the carrier of Image g) <=` Ord G by GROUP_1:def 12;
then Card (the carrier of Image g) <=`
Card (the carrier of G) by GROUP_1:def 12;
hence thesis by A3,A4,CARD_2:57;
end;
definition
let G,H,h;
attr h is being_monomorphism means :Def12: h is one-to-one;
synonym h is_monomorphism;
attr h is being_epimorphism means :Def13: rng h = the carrier of H;
synonym h is_epimorphism;
end;
theorem
h is_monomorphism & c in Image h implies h.(h".c) = c
proof
assume that A1: h is_monomorphism and
A2: c in Image h;
reconsider h' = h as
Function of the carrier of G,the carrier of Image h by Th58;
A3: h' is one-to-one by A1,Def12;
h'.(h'".c) = c
proof
A4: rng h' = the carrier of Image h by Th53;
c in the carrier of Image h by A2,RLVECT_1:def 1;
hence thesis by A3,A4,FUNCT_1:57;
end;
hence thesis;
end;
theorem Th64:
h is_monomorphism implies h".(h.a) = a
proof
assume h is one-to-one;
hence thesis by FUNCT_2:32;
end;
theorem Th65:
h is_monomorphism implies h" is Homomorphism of Image h,G
proof
assume A1: h is one-to-one;
then A2: h is_monomorphism by Def12;
reconsider Imh = Image h as Group;
h" is Function of the carrier of Imh,the carrier of G
proof
A3: h is Function of the carrier of G,the carrier of Imh by Th58;
rng h = the carrier of Imh by Th53;
hence thesis by A1,A3,FUNCT_2:31;
end;
then reconsider h' = h" as Function of the carrier of Imh,
the carrier of G;
now
let a,b be Element of Imh;
reconsider a' = a as Element of H by GROUP_2:51;
reconsider b' = b as Element of H by GROUP_2:51;
A4: a' in Imh & b' in Imh by RLVECT_1:def 1;
then consider a1 being Element of G such that
A5: h.a1 = a' by Th54;
consider b1 being Element of G such that
A6: h.b1 = b' by A4,Th54;
thus h'.(a * b) = h'.(h.a1 * h.b1) by A5,A6,GROUP_2:52
.= h'.(h.(a1 * b1)) by Def7
.= a1 * b1 by A2,Th64
.= h'.a * b1 by A2,A5,Th64
.= h'.a * h'.b by A2,A6,Th64;
end;
hence thesis by Def7;
end;
theorem Th66:
h is_monomorphism iff Ker h = (1).G
proof
thus h is_monomorphism implies Ker h = (1).G
proof
assume A1: h is one-to-one;
now
let x;
thus x in the carrier of Ker h iff x = 1.G
proof
thus x in the carrier of Ker h implies x = 1.G
proof
assume A2: x in the carrier of Ker h;
then x in Ker h by RLVECT_1:def 1;
then x in G by GROUP_2:49;
then reconsider a = x as Element of G
by RLVECT_1:def 1;
a in Ker h by A2,RLVECT_1:def 1;
then h.a = 1.H by Th50
.= h.(1.G) by Th40;
hence thesis by A1,Th1;
end;
assume A3: x = 1.G;
then reconsider a = x as Element of G;
h.a = 1.H by A3,Th40;
then a in Ker h by Th50;
hence thesis by RLVECT_1:def 1;
end;
end;
then the carrier of Ker h = {1.G} by TARSKI:def 1;
hence thesis by GROUP_2:def 7;
end;
assume Ker h = (1).G;
then A4: the carrier of Ker h = {1.G} by GROUP_2:def 7;
now
let a,b;
assume that
A5: a <> b and
A6: h.a = h.b;
h.a * h.(a") = h.(a * a") by Def7
.= h.(1.G) by GROUP_1:def 5
.= 1.H by Th40;
then 1.H = h.(b * a") by A6,Def7;
then b * a" in Ker h by Th50;
then A7: b * a" in the carrier of Ker h by RLVECT_1:def 1;
a = 1.G * a by GROUP_1:def 4
.= b * a" * a by A4,A7,TARSKI:def 1
.= b * (a" * a) by VECTSP_1:def 16
.= b * 1.G by GROUP_1:def 5
.= b by GROUP_1:def 4;
hence contradiction by A5;
end;
then for a,b st h.a = h.b holds a = b;
then h is one-to-one by Th1;
hence thesis by Def12;
end;
theorem Th67:
for H being strict Group, h being Homomorphism of G,H holds
h is_epimorphism iff Image h = H
proof let H be strict Group, h be Homomorphism of G,H;
thus h is_epimorphism implies Image h = H
proof assume rng h = the carrier of H;
then the carrier of Image h = the carrier of H by Th53;
hence thesis by GROUP_2:70;
end;
assume A1: Image h = H;
the carrier of H c= rng h
proof let x;
assume x in the carrier of H;
then x in h .: (the carrier of G) by A1,Def11;
then ex y st y in dom h & y in the carrier of G &
h.y = x by FUNCT_1:def 12;
hence thesis by FUNCT_1:def 5;
end;
then rng h = the carrier of H by XBOOLE_0:def 10;
hence thesis by Def13;
end;
theorem Th68:
for H being strict Group, h being Homomorphism of G,H holds
h is_epimorphism implies
for c being Element of H ex a st h.a = c
proof let H be strict Group, h be Homomorphism of G,H;
assume h is_epimorphism;
then A1: Image h = H by Th67;
now
let c be Element of H;
c in Image h by A1,RLVECT_1:def 1;
hence ex a st h.a = c by Th54;
end;
hence thesis;
end;
theorem Th69:
for N being normal Subgroup of G holds
nat_hom N is_epimorphism
proof let N be normal Subgroup of G;
Image nat_hom N = G./.N by Th57;
hence thesis by Th67;
end;
definition
let G,H,h;
attr h is being_isomorphism
means :Def14: h is_epimorphism & h is_monomorphism;
synonym h is_isomorphism;
end;
theorem Th70:
h is_isomorphism iff rng h = the carrier of H & h is one-to-one
proof
thus h is_isomorphism implies
rng h = the carrier of H & h is one-to-one
proof
assume h is_epimorphism & h is_monomorphism;
hence thesis by Def12,Def13;
end;
assume rng h = the carrier of H & h is one-to-one;
hence h is_epimorphism & h is_monomorphism by Def12,Def13;
end;
theorem
h is_isomorphism implies dom h = the carrier of G & rng h = the carrier of H
proof
assume h is_isomorphism;
then h is_epimorphism by Def14;
hence thesis by Def13,FUNCT_2:def 1;
end;
theorem Th72:
for H being strict Group, h being Homomorphism of G,H holds
h is_isomorphism implies h" is Homomorphism of H,G
proof let H be strict Group, h be Homomorphism of G,H;
assume A1: h is_epimorphism & h is_monomorphism;
then H = Image h by Th67;
hence thesis by A1,Th65;
end;
theorem Th73:
h is_isomorphism & g1 = h" implies g1 is_isomorphism
proof
assume that A1: h is_isomorphism and
A2: g1 = h";
A3: h is one-to-one by A1,Th70;
then A4: g1 is one-to-one by A2,FUNCT_1:62;
A5: dom h = the carrier of G by FUNCT_2:def 1;
rng g1 = dom h by A2,A3,FUNCT_1:55;
hence thesis by A4,A5,Th70;
end;
theorem Th74:
h is_isomorphism & h1 is_isomorphism implies h1 * h is_isomorphism
proof
assume A1: h is_isomorphism & h1 is_isomorphism;
then A2: h is one-to-one & h1 is one-to-one by Th70;
A3: rng(h1 * h) = the carrier of I
proof
A4: dom h1 = the carrier of H by FUNCT_2:def 1;
rng h = the carrier of H by A1,Th70;
hence rng(h1 * h) = rng h1 by A4,RELAT_1:47
.= the carrier of I by A1,Th70;
end;
h1 * h is one-to-one by A2,FUNCT_1:46;
hence thesis by A3,Th70;
end;
theorem Th75:
for G being Group holds
nat_hom (1).G is_isomorphism
proof let G be Group;
set g = nat_hom (1).G;
Ker g = (1).G by Th52;
then g is_monomorphism & g is_epimorphism by Th66,Th69;
hence nat_hom (1).G is_isomorphism by Def14;
end;
definition
let G,H;
pred G,H are_isomorphic means :Def15: ex h st h is_isomorphism;
reflexivity
proof let G;
reconsider i = id the carrier of G as Homomorphism of G,G by Th47;
i is one-to-one & rng i = the carrier of G by FUNCT_2:def 3;
then i is_isomorphism by Th70;
hence thesis;
end;
end;
canceled;
theorem Th77:
for G,H being strict Group holds
G,H are_isomorphic implies H,G are_isomorphic
proof let G,H be strict Group;
assume G,H are_isomorphic;
then consider h being Homomorphism of G,H such that
A1: h is_isomorphism by Def15;
reconsider g = h" as Homomorphism of H,G by A1,Th72;
take g;
thus thesis by A1,Th73;
end;
theorem
G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic
proof
assume that
A1: G,H are_isomorphic and
A2: H,I are_isomorphic;
consider g such that A3: g is_isomorphism by A1,Def15;
consider h1 such that A4: h1 is_isomorphism by A2,Def15;
(h1 * g) is_isomorphism by A3,A4,Th74;
hence thesis by Def15;
end;
theorem
h is_monomorphism implies G,Image h are_isomorphic
proof
assume A1: h is one-to-one;
reconsider ih = h as Homomorphism of G,Image h by Th58;
take ih;
A2: ih is_monomorphism by A1,Def12;
now
the carrier of Image h = rng ih by Th53;
hence ih is_epimorphism by Def13;
end;
hence thesis by A2,Def14;
end;
theorem Th80:
for G,H being strict Group holds
G is trivial & H is trivial implies G,H are_isomorphic
proof let G,H be strict Group;
assume G is trivial & H is trivial;
then A1: G = (1).G & H = (1).H by Th13;
take 1:(G,H);
set h = 1:(G,H);
A2: h is_epimorphism
proof
the carrier of (1).G = {1.G} by GROUP_2:def 7;
then rng h = {h.(1.G)} by A1,FUNCT_2:62
.= {1.H} by Def8
.= the carrier of (1).H by GROUP_2:def 7;
hence thesis by A1,Def13;
end;
h is_monomorphism
proof
now
let a,b be Element of G;
assume h.a = h.b;
a in the carrier of (1).G & b in the carrier of (1).G by A1;
then a in {1.G} & b in {1.G} by GROUP_2:def 7;
then a = 1.G & b = 1.G by TARSKI:def 1;
hence a = b;
end;
then h is one-to-one by Th1;
hence thesis by Def12;
end;
hence thesis by A2,Def14;
end;
theorem
(1).G,(1).H are_isomorphic
proof
(1).G is trivial & (1).H is trivial by Th11;
hence thesis by Th80;
end;
theorem
for G being strict Group holds
G,G./.(1).G are_isomorphic & G./.(1).G,G are_isomorphic
proof let G be strict Group;
nat_hom (1).G is_isomorphism by Th75;
hence G,G./.(1).G are_isomorphic by Def15;
hence thesis by Th77;
end;
theorem
for G being Group holds
G./.(Omega).G is trivial
proof let G be Group;
the carrier of G./.(Omega).G = Cosets (Omega).G by Th22
.= Left_Cosets (Omega).G by Def3
.= {the carrier of G} by GROUP_2:172;
hence thesis by Def2;
end;
theorem Th84:
for G,H being strict Group, h being Homomorphism of G,H holds
G,H are_isomorphic implies Ord G = Ord H
proof let G,H be strict Group, h be Homomorphism of G,H;
assume A1: G,H are_isomorphic;
then consider h being Homomorphism of G,H such that
A2: h is_isomorphism by Def15;
H,G are_isomorphic by A1,Th77;
then consider g1 being Homomorphism of H,G such that
A3: g1 is_isomorphism by Def15;
h is_epimorphism by A2,Def14;
then Image h = H by Th67;
then A4: Ord H <=` Ord G by Th61;
g1 is_epimorphism by A3,Def14;
then Image g1 = G by Th67;
then Ord G <=` Ord H by Th61;
hence thesis by A4,XBOOLE_0:def 10;
end;
Lm3:
G,H are_isomorphic & G is finite implies H is finite
proof
assume that A1: G,H are_isomorphic and
A2: G is finite;
consider h such that A3: h is_isomorphism by A1,Def15;
h is_epimorphism by A3,Def14;
then A4: rng h = the carrier of H by Def13;
the carrier of G is finite by A2,GROUP_1:def 13;
then dom h is finite by FUNCT_2:def 1;
then the carrier of H is finite by A4,FINSET_1:26;
hence thesis by GROUP_1:def 13;
end;
Lm4:
for G,H being strict Group holds
G,H are_isomorphic & H is finite implies G is finite
proof let G,H be strict Group;
assume that A1: G,H are_isomorphic and
A2: H is finite;
H,G are_isomorphic by A1,Th77;
hence thesis by A2,Lm3;
end;
theorem
for G,H being strict Group holds
G,H are_isomorphic & (G is finite or H is finite) implies
(G is finite & H is finite) by Lm3,Lm4;
theorem Th86:
for G,H being strict Group holds
G,H are_isomorphic & (G is finite or H is finite) implies ord G = ord H
proof let G,H be strict Group;
assume that A1: G,H are_isomorphic and
A2: G is finite or H is finite;
Ord G = Ord H by A1,Th84;
then A3: Card (the carrier of G) = Ord H by GROUP_1:def 12
.= Card (the carrier of H) by GROUP_1:def 12
;
A4: H is finite & G is finite by A1,A2,Lm3,Lm4;
then consider cH being finite set such that
A5: cH = the carrier of H & ord H = card cH by GROUP_1:def 14;
consider cG being finite set such that
A6: cG = the carrier of G & ord G = card cG by A4,GROUP_1:def 14;
thus thesis by A3,A5,A6;
end;
theorem
for G,H being strict Group holds
G,H are_isomorphic & G is trivial implies H is trivial
proof let G,H be strict Group;
assume that A1: G,H are_isomorphic and
A2: G is trivial;
A3: ord G = 1 & G is finite by A2,Th12;
then A4: ord H = 1 by A1,Th86;
H is finite by A1,A3,Lm3;
hence thesis by A4,Th12;
end;
Lm5:
for G,H being strict Group holds
G,H are_isomorphic & G is trivial implies H is trivial
proof let G,H be strict Group;
assume that A1: G,H are_isomorphic and
A2: G is trivial;
A3: ord G = 1 & G is finite by A2,Th12;
then A4: ord H = 1 by A1,Th86;
H is finite by A1,A3,Lm3;
hence thesis by A4,Th12;
end;
Lm6:
for G,H being strict Group holds
G,H are_isomorphic & H is trivial implies G is trivial
proof let G,H be strict Group;
assume that A1: G,H are_isomorphic and
A2: H is trivial;
H,G are_isomorphic by A1,Th77;
hence thesis by A2,Lm5;
end;
theorem
for G,H being strict Group holds
G,H are_isomorphic & (G is trivial or H is trivial) implies
G is trivial & H is trivial by Lm5,Lm6;
Lm7:
for H being strict Group, h being Homomorphism of G,H holds
G,H are_isomorphic & G is commutative Group implies H is commutative Group
proof let H be strict Group, h be Homomorphism of G,H;
assume that A1: G,H are_isomorphic and
A2: G is commutative Group;
consider h being Homomorphism of G,H such that
A3: h is_isomorphism by A1,Def15;
A4: h is_epimorphism by A3,Def14;
now
let c,d be Element of H;
consider a such that A5: h.a = c by A4,Th68;
consider b such that A6: h.b = d by A4,Th68;
thus c * d = h.(a * b) by A5,A6,Def7
.= h.(b * a) by A2,Lm2
.= d * c by A5,A6,Def7;
end;
hence thesis by VECTSP_1:def 17;
end;
Lm8:
for G,H being strict Group, h being Homomorphism of G,H holds
G,H are_isomorphic & H is commutative Group implies G is commutative Group
proof let G,H be strict Group, h be Homomorphism of G,H;
assume that A1: G,H are_isomorphic and
A2: H is commutative Group;
H,G are_isomorphic by A1,Th77;
hence thesis by A2,Lm7;
end;
theorem
for G,H being strict Group, h being Homomorphism of G,H holds
G,H are_isomorphic & (G is commutative Group or H is commutative Group)
implies (G is commutative Group & H is commutative Group) by Lm7,Lm8;
Lm9:
G./.Ker g,Image g are_isomorphic & Image g, G./.Ker g are_isomorphic &
ex h being Homomorphism of G./.Ker g,Image g st h is_isomorphism &
g = h * nat_hom Ker g
proof set I = G./.Ker g; set J = Image g;
defpred P[set,set] means for a st $1 = a * Ker g holds $2 = g.a;
A1: for S being Element of I
ex T being Element of J st P[S,T]
proof let S be Element of I;
consider a such that A2: S = a * Ker g & S = Ker g * a by Th26;
g.a in J by Th54;
then reconsider T = g.a as Element of J
by RLVECT_1:def 1;
take T;
let b;
assume S = b * Ker g;
then a" * b in Ker g by A2,GROUP_2:137;
then 1.H = g.(a" * b) by Th50
.= g.(a") * g.b by Def7
.= (g.a)" * g.b by Th41;
then g.b = (g.a)"" by GROUP_1:20;
hence thesis by GROUP_1:19;
end;
consider f being Function of the carrier of I,the carrier of J such that
A3: for S being Element of I holds P[S,f.S]
from FuncExD(A1);
now let S,T be Element of G./.Ker g;
consider a such that A4: S = a * Ker g and S = Ker g * a by Th26;
consider b such that A5: T = b * Ker g and A6: T = Ker g * b by Th26;
f.S = g.a & f.T = g.b by A3,A4,A5;
then A7: f.S * f.T = g.a * g.b by GROUP_2:52
.= g.(a * b) by Def7;
@S = S & @T = T by Def6;
then S * T = (a * Ker g) * (Ker g * b) by A4,A6,Th24
.= (a * Ker g) * Ker g * b by GROUP_3:12
.= a * Ker g * b by Th6
.= a * (Ker g * b) by GROUP_2:128
.= a * (b * Ker g) by GROUP_3:140
.= a * b * Ker g by GROUP_2:127;
hence f.(S * T) = f.S * f.T by A3,A7;
end;
then reconsider f as Homomorphism of G./.Ker g,J by Def7;
the carrier of J c= rng f
proof let x;
assume x in the carrier of J;
then x in Image g by RLVECT_1:def 1;
then consider a such that A8: x = g.a by Th54;
reconsider S = a * Ker g as Element of I by Th27;
f.S = g.a & S in the carrier of I & the carrier of I = dom f
by A3,FUNCT_2:def 1;
hence thesis by A8,FUNCT_1:def 5;
end;
then A9: rng f = the carrier of J by XBOOLE_0:def 10;
A10: f is one-to-one
proof let y1,y2;
assume y1 in dom f & y2 in dom f;
then reconsider S = y1, T = y2 as Element of I
by FUNCT_2:def 1;
consider a such that A11: S = a * Ker g and S = Ker g * a by Th26;
consider b such that A12: T = b * Ker g and T = Ker g * b by Th26;
assume A13: f.y1 = f.y2;
f.S = g.a & f.T = g.b by A3,A11,A12;
then (g.b)" * g.a = 1.H by A13,GROUP_1:def 5;
then 1.H = g.(b") * g.a by Th41
.= g.(b" * a) by Def7;
then b" * a in Ker g by Th50;
hence thesis by A11,A12,GROUP_2:137;
end;
then f is_isomorphism by A9,Th70;
hence G./.Ker g,Image g are_isomorphic by Def15;
hence Image g,G./.Ker g are_isomorphic by Th77;
take f;
A14: dom nat_hom Ker g = the carrier of G & dom g = the carrier of G
by FUNCT_2:def
1;
thus f is_isomorphism by A9,A10,Th70;
A15: now let x;
thus x in dom g implies x in dom nat_hom Ker g & (nat_hom Ker g).x in
dom f
proof assume A16: x in dom g;
hence x in dom nat_hom Ker g by A14;
(nat_hom Ker g).x in rng nat_hom Ker g &
rng nat_hom Ker g c= the carrier of I &
dom f = the carrier of I by A14,A16,FUNCT_1:def 5,FUNCT_2:def 1;
hence (nat_hom Ker g).x in dom f;
end;
assume that A17: x in dom nat_hom Ker g and (nat_hom Ker g).x in dom f
;
thus x in dom g by A14,A17;
end;
now let x;
assume x in dom g;
then reconsider a = x as Element of G by FUNCT_2:def 1
;
(nat_hom Ker g).a = a * Ker g by Def9;
hence g.x = f.((nat_hom Ker g).x) by A3;
end;
hence thesis by A15,FUNCT_1:20;
end;
theorem
G./.Ker g,Image g are_isomorphic & Image g, G./.Ker g are_isomorphic by Lm9;
theorem
ex h being Homomorphism of G./.Ker g,Image g st h is_isomorphism &
g = h * nat_hom Ker g by Lm9;
theorem
for M being strict normal Subgroup of G
for J being strict normal Subgroup of G./.M st
J = N./.(N,M)`*` & M is Subgroup of N holds (G./.M)./.J,G./.N are_isomorphic
proof let M be strict normal Subgroup of G;
let J be strict normal Subgroup of G./.M;
assume that A1: J = N./.(N,M)`*` and A2: M is Subgroup of N;
defpred P[set,set] means for a st $1 = a * M holds $2 = a * N;
A3: for x being Element of G./.M
ex y being Element of G./.N st
P[x,y]
proof let x be Element of G./.M;
consider a such that A4: x = a * M and x = M * a by Th26;
reconsider y = a * N as Element of G./.N by Th27;
take y;
let b;
assume x = b * M;
then a" * b in M by A4,GROUP_2:137;
then a" * b in N by A2,GROUP_2:49;
hence thesis by GROUP_2:137;
end;
consider f being Function of the carrier of G./.M, the carrier of G./.N
such that A5: for x being Element of G./.M holds P[x,f.x]
from FuncExD(A3);
now let x,y be Element of G./.M;
consider a such that A6: x = a * M and x = M * a by Th26;
consider b such that A7: y = b * M and y = M * b by Th26;
A8: f.x = @(f.x) & f.y = @(f.y) by Def6;
A9: f.x = a * N & f.y = b * N by A5,A6,A7;
A10: f.x * f.y = @(f.x) * @(f.y) by Th24
.= a * N * b * N by A8,A9,GROUP_3:10
.= a * (N * b) * N by GROUP_2:128
.= a * (b * N) * N by GROUP_3:140
.= a * ((b * N) * N) by GROUP_3:9
.= a * (b * N) by Th6
.= a * b * N by GROUP_2:127;
A11: @x = x & @y = y by Def6;
x * y = @x * @y by Th24
.= a * M * b * M by A6,A7,A11,GROUP_3:10
.= a * (M * b) * M by GROUP_2:128
.= a * (b * M) * M by GROUP_3:140
.= a * ((b * M) * M) by GROUP_3:9
.= a * (b * M) by Th6
.= a * b * M by GROUP_2:127;
hence f.(x * y) = f.x * f.y by A5,A10;
end;
then reconsider f as Homomorphism of G./.M,G./.N by Def7;
A12: Ker f = J
proof let S be Element of G./.M;
thus S in Ker f implies S in J
proof assume S in Ker f;
then A13: f.S = 1.(G./.N) by Th50
.= carr N by Th29;
consider a such that A14: S = a * M & S = M * a by Th26;
f.S = a * N by A5,A14;
then a in N by A13,GROUP_2:136;
then reconsider q = a as Element of N
by RLVECT_1:def 1;
(N,M)`*` = M by A2,Def1;
then S = q * (N,M)`*` & S = (N,M)`*` * q by A14,Th2;
hence thesis by A1,Th28;
end;
assume S in J;
then consider a being Element of N such that
A15: S = a * (N,M)`*` & S = (N,M)`*` * a by A1,Th28;
reconsider a' = a as Element of G by GROUP_2:51;
(N,M)`*` = M by A2,Def1;
then S = a' * M by A15,Th2;
then f.S = a' * N & a in N by A5,RLVECT_1:def 1;
then f.S = carr N by GROUP_2:136
.= 1.(G./.N) by Th29;
hence thesis by Th50;
end;
the carrier of G./.N c= rng f
proof let x;
assume x in the carrier of G./.N;
then x in G./.N by RLVECT_1:def 1;
then consider a such that A16: x = a * N & x = N * a by Th28;
reconsider S = a * M as Element of G./.M by Th27;
f.S = a * N & S in
the carrier of G./.M & dom f = the carrier of G./.M
by A5,
FUNCT_2:def 1;
hence thesis by A16,FUNCT_1:def 5;
end;
then rng f = the carrier of G./.N by XBOOLE_0:def 10;
then f is_epimorphism by Def13;
then Image f = G./.N by Th67;
hence thesis by A12,Lm9;
end;
theorem
for N being strict normal Subgroup of G holds
(B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic
proof let N be strict normal Subgroup of G;
set f = nat_hom N; set g = f | (the carrier of B);
set I = (B "\/" N)./.(B "\/" N,N)`*`; set J = (B "\/" N,N)`*`;
A1: B is Subgroup of B "\/" N by GROUP_4:78;
A2: dom g = dom f /\ (the carrier of B) & dom f = the carrier of G &
the carrier of B c= the carrier of G by FUNCT_2:def 1,GROUP_2:def 5,
RELAT_1:90;
then A3: dom g = the carrier of B by XBOOLE_1:28;
A4: N is Subgroup of B "\/" N by GROUP_4:78;
then A5: N = (B "\/" N,N)`*` by Def1;
A6: I is Subgroup of G./.N by A4,Th34;
rng g c= the carrier of I
proof let y;
assume y in rng g;
then consider x such that A7: x in
dom g and A8: g.x = y by FUNCT_1:def 5;
reconsider x as Element of B by A2,A7,XBOOLE_1:28;
reconsider x'' = x as Element of B "\/" N
by A1,GROUP_2:51;
reconsider x' = x as Element of G by GROUP_2:51;
A9: g.x = f.x' by A7,FUNCT_1:70
.= x' * N by Def9;
then A10: g.x = N * x' by GROUP_3:140;
x'' * (B "\/" N,N)`*` = x' * N & N * x' = (B "\/" N,N)`*`
* x'' by A5,Th2;
then y in I by A8,A9,A10,Th28;
hence thesis by RLVECT_1:def 1;
end;
then reconsider g as Function of the carrier of B,
the carrier of (B "\/" N)./.
(B "\/" N,N)`*` by A3,FUNCT_2:def 1,RELSET_1:11;
now let a,b be Element of B;
reconsider a' = a, b' = b as Element of G by GROUP_2:51;
A11: f.a' = g.a & f.b' = g.b by FUNCT_1:72;
a * b in the carrier of B & a * b = a' * b' &
a' * b' in the carrier of G by GROUP_2:52;
hence g.(a * b) = f.(a' * b') by FUNCT_1:72
.= f.a' * f.b' by Def7
.= g.a * g.b by A6,A11,GROUP_2:52;
end;
then reconsider g as Homomorphism of B,(B "\/" N)./.(B "\/"
N,N)`*` by Def7;
A12: Ker g = B /\ N
proof let b be Element of B;
reconsider c = b as Element of G by GROUP_2:51;
A13: g.b = f.c by FUNCT_1:72
.= c * N by Def9;
thus b in Ker g implies b in B /\ N
proof assume b in Ker g;
then g.b = 1.I by Th50
.= carr J by Th29
.= the carrier of N by A5,GROUP_2:def 9
.= carr N by GROUP_2:def 9;
then b in B & b in N by A13,GROUP_2:136,RLVECT_1:def 1;
hence thesis by GROUP_2:99;
end;
assume b in B /\ N;
then b in N by GROUP_2:99;
then c * N = carr N by GROUP_2:136
.= the carrier of J by A5,GROUP_2:def 9
.= carr J by GROUP_2:def 9
.= 1.I by Th29;
hence thesis by A13,Th50;
end;
the carrier of I c= rng g
proof let x;
assume x in the carrier of I;
then x in I by RLVECT_1:def 1;
then consider b being Element of B "\/" N such that
A14: x = b * J & x = J * b by Th28;
B * N = N * B & b in B "\/" N by GROUP_5:8,RLVECT_1:def 1;
then consider a1,a2 such that A15: b = a1 * a2 and A16: a1 in B & a2 in
N
by GROUP_5:5;
A17: a1 in the carrier of B & a1 in the carrier of G by A16,RLVECT_1:
def 1;
x = a1 * a2 * N by A5,A14,A15,Th2
.= a1 * (a2 * N) by GROUP_2:127
.= a1 * carr N by A16,GROUP_2:136
.= a1 * N by GROUP_2:def 13
.= f.a1 by Def9
.= g.a1 by A17,FUNCT_1:72;
hence thesis by A3,A17,FUNCT_1:def 5;
end;
then the carrier of I = rng g by XBOOLE_0:def 10;
then g is_epimorphism by Def13;
then Image g = (B "\/" N)./.(B "\/" N,N)`*` by Th67;
hence thesis by A12,Lm9;
end;