:: Homomorphisms and Isomorphisms of Groups. Quotient Group
:: by Wojciech A. Trybulec and Micha{\l} J. Trybulec
::
:: Received October 3, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, FUNCT_1, SUBSET_1, GROUP_1, GROUP_2, PRE_TOPC, RLSUB_1,
NUMBERS, INT_1, STRUCT_0, RELAT_1, TARSKI, NEWTON, XXREAL_1, GROUP_4,
GROUP_5, ALGSTR_0, NATTRA_1, ZFMISC_1, CARD_1, FINSET_1, BINOP_1,
QC_LANG1, CQC_SIM1, REALSET1, MSSUBFAM, FUNCOP_1, ARYTM_3, XXREAL_0,
COMPLEX1, FUNCT_2, WELLORD1, EQREL_1, GROUP_6, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, CARD_1, ORDINAL1,
NUMBERS, XXREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
FUNCOP_1, FINSET_1, BINOP_1, INT_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2,
GROUP_3, NAT_1, GROUP_4, GROUP_5, INT_2;
constructors RELAT_2, PARTFUN1, BINOP_1, FUNCOP_1, FINSUB_1, XXREAL_0, NAT_1,
REAL_1, INT_2, REALSET2, GROUP_4, GROUP_5, RELSET_1, BINOP_2;
registrations FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, XREAL_0, INT_1, STRUCT_0,
GROUP_1, GROUP_2, GROUP_3, ORDINAL1, RELSET_1, FUNCOP_1;
requirements NUMERALS, SUBSET, BOOLE;
definitions XBOOLE_0, FUNCT_1, GROUP_1, GROUP_2, TARSKI, FUNCT_2;
equalities XBOOLE_0, GROUP_2, BINOP_1, REALSET1, GROUP_4, ALGSTR_0, STRUCT_0,
ORDINAL1;
expansions XBOOLE_0, GROUP_1, BINOP_1, FUNCT_2, STRUCT_0;
theorems CARD_1, CARD_2, FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, GROUP_3, GROUP_4,
GROUP_5, TARSKI, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_1, FUNCOP_1, NAT_1,
ABSVALUE, STRUCT_0;
schemes BINOP_1, FUNCT_2, DOMAIN_1, NAT_1, CLASSES1;
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:19;
assume for a,b being Element of A st f.a = f.b holds a = b;
then for a,b being object st a in A & b in A & f.a = f.b holds a = b;
hence thesis by FUNCT_2:19;
end;
definition
let G be Group, A be Subgroup of G;
redefine mode Subgroup of A -> Subgroup of G; :: redefines Subgroup (GROUP_2, definition)
coherence by GROUP_2:56;
end;
registration
let G be Group;
cluster (1).G -> normal;
coherence by GROUP_3:114;
cluster (Omega).G -> normal;
coherence by GROUP_3:114;
end;
reserve n for Element of 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;
set I = X qua Subgroup of G;
assume
A1: x = a;
thus x * X c= a * I
proof
let y be object;
assume y in x * X;
then consider g being Element of A such that
A2: y = x * g & g in X by GROUP_2:103;
reconsider h = g as Element of G by GROUP_2:42;
a * h = x * g by A1,GROUP_2:43;
hence thesis by A2,GROUP_2:103;
end;
thus a * I c= x * X
proof
let y be object;
assume y in a * I;
then consider b such that
A3: y = a * b and
A4: b in X by GROUP_2:103;
reconsider c = b as Element of X by A4;
reconsider c as Element of A by GROUP_2:42;
a * b = x * c by A1,GROUP_2:43;
hence thesis by A3,A4,GROUP_2:103;
end;
thus X * x c= I * a
proof
let y be object;
assume y in X * x;
then consider g being Element of A such that
A5: y = g * x & g in X by GROUP_2:104;
reconsider h = g as Element of G by GROUP_2:42;
h * a = g * x by A1,GROUP_2:43;
hence thesis by A5,GROUP_2:104;
end;
thus I * a c= X * x
proof
let y be object;
assume y in I * a;
then consider b such that
A6: y = b * a and
A7: b in X by GROUP_2:104;
reconsider c = b as Element of X by A7;
reconsider c as Element of A by GROUP_2:42;
b * a = c * x by A1,GROUP_2:43;
hence thesis by A6,A7,GROUP_2:104;
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;
reconsider Z = X /\ Y as Subgroup of G by GROUP_2:56;
the carrier of X /\ Y = (carr X) /\ (carr Y) by GROUP_2:def 10;
then (X qua Subgroup of G) /\ (Y qua Subgroup of G) = Z by GROUP_2:80;
hence thesis;
end;
theorem Th4:
a * b * a" = b |^ a" & a * (b * a") = b |^ a"
proof
thus a * b * a" = a"" * b * a" .= b |^ a" by GROUP_3:def 2;
hence thesis by GROUP_1:def 3;
end;
theorem Th5:
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:45
.= a * A by GROUP_2:76;
hence a * (A * A) = a * A by GROUP_4:45;
thus A * A * a = A * a by GROUP_2:76;
hence thesis by GROUP_4:46;
end;
theorem Th6:
for G being Group, A1 being Subset of G holds
A1 = the set of all [.a,b.] where
a is Element of G, b is Element of G implies G` = gr A1
proof
let G be Group, A1 be Subset of G;
assume
A1: A1 = the set of all [.a,b.] where a is Element of G, b is Element of G;
A1 = commutators G
proof
thus A1 c= commutators G
proof
let x be object;
assume x in A1;
then ex a,b being Element of G st x = [.a,b.] by A1;
hence thesis by GROUP_5:58;
end;
let x be object;
assume x in commutators G;
then ex a,b being Element of G st x = [.a,b.] by GROUP_5:58;
hence thesis by A1;
end;
hence thesis by GROUP_5:72;
end;
theorem Th7:
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
defpred P[set,set] means not contradiction;
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 by GROUP_2:40,GROUP_5:74;
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 DOMAIN_1:sch 9;
assume
A1: for a,b being Element of G holds [.a,b.] in B;
X c= the carrier of B
proof
let x be object;
assume x in X;
then ex a,b being Element of G st x = [.a,b.];
then x in B by A1;
hence thesis;
end;
then gr X is Subgroup of B by GROUP_4:def 4;
hence thesis by Th6;
end;
theorem Th8:
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 N9 = N as Subgroup of B;
now
let n be Element of B;
thus n * N9 c= N9 * n
proof
let x be object;
assume x in n * N9;
then consider a being Element of B such that
A1: x = n * a and
A2: a in N9 by GROUP_2:103;
reconsider a9 = a, n9 = n as Element of G by GROUP_2:42;
x = n9 * a9 by A1,GROUP_2:43;
then
A3: x in n9 * N by A2,GROUP_2:103;
n9 * N c= N * n9 by GROUP_3:118;
then consider a1 such that
A4: x = a1 * n9 and
A5: a1 in N by A3,GROUP_2:104;
a1 in N9 by A5;
then a1 in B by GROUP_2:40;
then reconsider a19 = a1 as Element of B;
x = a19 * n by A4,GROUP_2:43;
hence thesis by A5,GROUP_2:104;
end;
end;
hence thesis by GROUP_3:118;
end;
definition
let G,B;
let M be normal Subgroup of G;
assume
A1: the multMagma of M is Subgroup of B;
func (B,M)`*` -> strict normal Subgroup of B equals
:Def1:
the multMagma of M;
coherence
proof
reconsider x = the multMagma of M as Subgroup of G by A1;
now
let a;
thus a * x = a * M .= M * a by GROUP_3:117
.= x * a;
end;
then x is normal Subgroup of G by GROUP_3:117;
hence thesis by A1,Th8;
end;
correctness;
end;
theorem Th9:
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:88;
now
let b be Element of B;
thus b * A c= A * b
proof
let x be object;
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:103;
reconsider a9 = a, b9 = b as Element of G by GROUP_2:42;
a in N & x = b9 * a9 by A1,A2,GROUP_2:43,82;
then
A3: x in b9 * N by GROUP_2:103;
reconsider x9 = x as Element of B by A1;
A4: b9" = b" by GROUP_2:48;
b9 * N c= N * b9 by GROUP_3:118;
then consider b1 such that
A5: x = b1 * b9 and
A6: b1 in N by A3,GROUP_2:104;
reconsider x99 = x as Element of G by A5;
b1 = x99 * b9" by A5,GROUP_1:14;
then
A7: b1 = x9 * b" by A4,GROUP_2:43;
then reconsider b19 = b1 as Element of B;
b1 in B by A7;
then
A8: b19 in A by A6,GROUP_2:82;
b19 * b = x by A5,GROUP_2:43;
hence thesis by A8,GROUP_2:104;
end;
end;
hence thesis by GROUP_3:118;
end;
hence thesis;
end;
definition
let G,B;
let N be normal Subgroup of G;
redefine func B /\ N -> strict normal Subgroup of B; :: redefines /\ (GROUP_2, definition)
coherence by Th9;
end;
definition
let G;
let N be normal Subgroup of G;
let B;
redefine func N /\ B -> strict normal Subgroup of B; :: redefines /\ (GROUP_2, definition)
coherence by Th9;
end;
definition
let G be non empty 1-sorted;
redefine attr G is trivial means :: redefines trivial (STRUCT_0, redefinition) → trivial (STRUCT_0, definition)
:Def2:
ex x being object st the carrier of G = {x};
compatibility
proof
hereby
set y = the Element of G;
assume G is trivial;
then for x be object holds x in the carrier of G iff x = y;
then the carrier of G = {y} by TARSKI:def 1;
hence ex x being object st the carrier of G = {x};
end;
given x being object such that
A1: the carrier of G = {x};
now
let a,b be Element of G;
thus a = x by A1,TARSKI:def 1
.= b by A1,TARSKI:def 1;
end;
hence thesis;
end;
end;
theorem Th10:
(1).G is trivial
proof
the carrier of (1).G = {1_G} by GROUP_2:def 7;
hence thesis;
end;
registration
let G;
cluster (1).G -> trivial;
coherence by Th10;
end;
registration
cluster strict trivial for Group;
existence
proof
set G = the Group;
take (1).G;
thus thesis;
end;
end;
theorem Th11:
(for G being trivial Group holds card G = 1 & G is finite) &
for G being Group st card G = 1 holds G is trivial
proof
thus for G being trivial Group holds card G = 1 & G is finite
proof
let G be trivial Group;
ex x being object st the carrier of G = {x} by Def2;
hence thesis by CARD_1:30;
end;
let G be Group;
assume card G = 1;
hence ex x being object st the carrier of G = {x} by CARD_2:42;
end;
theorem
for G being strict trivial Group holds (1).G = G
proof
let G be strict trivial Group;
card G = 1 by Th11;
then card G = card (1).G by GROUP_2:69;
hence thesis by GROUP_2:73;
end;
notation
let G,N;
synonym Cosets N for Left_Cosets N;
end;
registration
let G,N;
cluster Cosets N -> non empty;
coherence;
end;
theorem Th13:
for x being object holds
for N being normal Subgroup of G holds x in Cosets N implies
ex a st x = a * N & x = N * a
proof let x be object;
let N be normal Subgroup of G;
assume x in Cosets N;
then consider a such that
A1: x = a * N by GROUP_2:def 15;
x = N * a by A1,GROUP_3:117;
hence thesis by A1;
end;
theorem Th14:
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;
N * a in Right_Cosets N by GROUP_2:def 16;
hence thesis by GROUP_2:def 15,GROUP_3:127;
end;
theorem Th15:
for N being normal Subgroup of G holds x in Cosets N implies
x is Subset of G;
theorem Th16:
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 that
A1: A1 in Cosets N and
A2: A2 in Cosets N;
consider a such that
A3: A1 = a * N and
A1 = N * a by A1,Th13;
consider b such that
A4: A2 = b * N and
A5: A2 = N * b by A2,Th13;
A1 * A2 = a * (N * (b * N)) by A3,A4,GROUP_3:10
.= a * (b * N * N) by A4,A5,GROUP_3:13
.= a * (b * (N * N)) by GROUP_4:45
.= a * (b * N) by GROUP_2:76
.= a * b * N by GROUP_2:105;
hence thesis by GROUP_2:def 15;
end;
definition
let G;
let N be normal Subgroup of G;
func CosOp N -> BinOp of Cosets N means
:Def3:
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 Th15;
reconsider C = A1 * A2 as Element of Cosets N by Th16;
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 BINOP_1:sch 3(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;
o1.(W,V) = A1 * A2 by A2;
hence o1.(x,y) = o2.(x,y) by A3;
end;
hence thesis;
end;
end;
definition
let G;
let N be normal Subgroup of G;
func G./.N -> multMagma equals
multMagma (# Cosets N, CosOp N #);
correctness;
end;
registration
let G;
let N be normal Subgroup of G;
cluster G./.N -> strict non empty;
coherence;
end;
theorem
for N being normal Subgroup of G holds the carrier of G./.N = Cosets N;
theorem
for N being normal Subgroup of G holds the multF of G./.N = CosOp N;
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
S;
coherence by Th15;
end;
theorem
for N being normal Subgroup of G, T1,T2 being Element of G./.N holds
@T1 * @T2 = T1 * T2 by Def3;
theorem
@(T1 * T2) = @T1 * @T2 by Def3;
registration
let G;
let N be normal Subgroup of G;
cluster G./.N -> associative Group-like;
coherence
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
A1: f = a * N and
f = N * a by Th13;
consider c being Element of G such that
A2: h = c * N and
h = N * c by Th13;
thus f * (g * h) = @f * @(g * h) by Def3
.= (a * N) * (@g * @h) by A1,Def3
.= @f * @g * (c * N) by A1,A2,GROUP_2:10
.= @(f * g) * @h by A2,Def3
.= f * g * h by Def3;
end;
reconsider e = carr N as Element of G./.N by GROUP_2:135;
take e;
let h be Element of G./.N;
consider a such that
A3: h = a * N and
A4: h = N * a by Th13;
thus h * e = (a * N) * N by A3,Def3
.= a * (N * N) by GROUP_4:45
.= h by A3,GROUP_2:76;
thus e * h = N * (N * a) by A4,Def3
.= N * N * a by GROUP_4:46
.= h by A4,GROUP_2:76;
reconsider g = a" * N as Element of G./.N by GROUP_2:def 15;
take g;
thus h * g = N * a * (a" * N) by A4,Def3
.= N * a * a" * N by GROUP_3:9
.= N * (a * a") * N by GROUP_2:107
.= N * 1_G * N by GROUP_1:def 5
.= carr N * carr N by GROUP_2:109
.= e by GROUP_2:76;
thus g * h = @g * @h by Def3
.= a" * N * a * N by A3,GROUP_3:9
.= a" * (N * a) * N by GROUP_2:106
.= a" * (a * N) * N by GROUP_3:117
.= a" * a * N * N by GROUP_2:105
.= 1_G * N * N by GROUP_1:def 5
.= 1_G * (N * N) by GROUP_4:45
.= 1_G * carr N by GROUP_2:76
.= e by GROUP_2:37;
end;
end;
theorem
for N being normal Subgroup of G, S being Element of G./.N
ex a st S = a * N & S = N * a by Th13;
theorem
N * a is Element of G./.N & a * N is Element of G./.N &
carr N is Element of G./.N by Th14,GROUP_2:135;
theorem Th23:
for x being object holds
for N being normal Subgroup of G holds x in G./.N iff
ex a st x = a * N & x = N * a by Th13,Th14;
theorem Th24:
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 GROUP_2:135;
now
let h be Element of G./.N;
consider a such that
A1: h = a * N and
A2: h = N * a by Th13;
thus h * e = (a * N) * N by A1,Def3
.= a * (N * N) by GROUP_4:45
.= h by A1,GROUP_2:76;
thus e * h = N * (N * a) by A2,Def3
.= N * N * a by GROUP_4:46
.= h by A2,GROUP_2:76;
end;
hence thesis by GROUP_1:4;
end;
theorem Th25:
for N being normal Subgroup of G, S being Element of G./.N st
S = a * N holds S" = a" * N
proof
let N be normal Subgroup of G, S be Element of G./.N;
reconsider g = a" * N as Element of G./.N by Th14;
assume
A1: S = a * N;
A2: g * S = @g * @S by Def3
.= a" * N * a * N by A1,GROUP_3:9
.= a" * (N * a) * N by GROUP_2:106
.= a" * (a * N) * N by GROUP_3:117
.= a" * a * N * N by GROUP_2:105
.= 1_G * N * N by GROUP_1:def 5
.= 1_G * (N * N) by GROUP_4:45
.= 1_G * carr N by GROUP_2:76
.= carr N by GROUP_2:37;
A3: 1_(G./.N) = carr N by Th24;
S * g = @S * @g by Def3
.= N * a * (a" * N) by A1,GROUP_3:117
.= N * a * a" * N by GROUP_3:9
.= N * (a * a") * N by GROUP_2:107
.= N * 1_G * N by GROUP_1:def 5
.= carr N * carr N by GROUP_2:109
.= carr N by GROUP_2:76;
hence thesis by A2,A3,GROUP_1:def 5;
end;
theorem
for N being normal Subgroup of G holds card(G./.N) = Index N;
theorem
for N being normal Subgroup of G holds Left_Cosets N is finite implies
card(G./.N) = index N
proof
let N be normal Subgroup of G;
assume Left_Cosets N is finite;
then reconsider LC = Left_Cosets N as finite set;
thus card(G./.N) = card LC .= index N by GROUP_2:def 18;
end;
theorem Th28:
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;
set I = B./.(B,M)`*`;
set J = (B,M)`*`;
set g = the multF of I;
set f = the multF of G./.M;
set X = [: the carrier of I,the carrier of I :];
assume
A1: M is Subgroup of B;
A2: the carrier of I c= the carrier of G./.M
proof
let x be object;
assume x in the carrier of I;
then consider a being Element of B such that
A3: x = a * J and
x = J * a by Th13;
reconsider b = a as Element of G by GROUP_2:42;
J = M by A1,Def1;
then a * J = b * M by Th2;
hence thesis by A3,Th14;
end;
A4: now
let x be object;
assume
A5: x in dom g;
then consider y,z being object such that
A6: [y,z] = x by RELAT_1:def 1;
z in the carrier of I by A5,A6,ZFMISC_1:87;
then consider b being Element of B such that
A7: z = b * J and
A8: z = J * b by Th13;
y in the carrier of I by A5,A6,ZFMISC_1:87;
then consider a being Element of B such that
A9: y = a * J and
y = J * a by Th13;
reconsider W1 = y, W2 = z as Element of Cosets J by A9,A7,Th14;
A10: g.x = g.(W1,W2) by A6
.= (a * J) * (J * b) by A9,A8,Def3
.= a * J * J * b by GROUP_3:11
.= a * (J * J) * b by GROUP_4:45
.= a * J * b by GROUP_2:76
.= a * (J * b) by GROUP_2:106
.= a * (b * J) by GROUP_3:117
.= a * b * J by GROUP_2:105;
reconsider a9 = a, b9 = b as Element of G by GROUP_2:42;
A11: J = M by A1,Def1;
then
A12: y = a9 * M by A9,Th2;
z = b9 * M by A7,A11,Th2;
then reconsider V1 = y, V2 = z as Element of Cosets M by A12,Th14;
A13: a9 * b9 = a * b by GROUP_2:43;
A14: z = M * b9 by A8,A11,Th2;
f.x = f.(V1,V2) by A6
.= (a9 * M) * (M * b9) by A12,A14,Def3
.= a9 * M * M * b9 by GROUP_3:11
.= a9 * (M * M) * b9 by GROUP_4:45
.= a9 * M * b9 by GROUP_2:76
.= a9 * (M * b9) by GROUP_2:106
.= a9 * (b9 * M) by GROUP_3:117
.= a9 * b9 * M by GROUP_2:105;
hence g.x = f.x by A10,A11,A13,Th2;
end;
dom g = X & dom f = [: the carrier of G./.M,the carrier of G./.M :] by
FUNCT_2:def 1;
then dom g = dom f /\ X by A2,XBOOLE_1:28,ZFMISC_1:96;
then g = f||the carrier of I by A4,FUNCT_1:46;
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;
then reconsider I = M as normal Subgroup of N;
reconsider J = N./.(N,M)`*` as Subgroup of G./.M by A1,Th28;
now
let S be Element of G./.M;
thus S * J c= J * S
proof
let x be object;
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:103;
consider c being Element of N such that
T = c * I and
A5: T = I * c by A2,A4,Th23;
reconsider d = c as Element of G by GROUP_2:42;
consider a such that
S = a * M and
A6: S = M * a by Th13;
set e = a * (d * a");
c in N & e = d |^ a" by Th4;
then e in N by GROUP_5:3;
then reconsider f = e as Element of N;
A7: M * e = I * f by Th2;
reconsider V = I * f as Element of J by A2,Th14;
A8: V in J;
reconsider V as Element of G./.M by GROUP_2:42;
M * d = I * c by Th2;
then x = M * a * (M * d) by A3,A6,A5,Def3
.= M * a * (M * d * 1_G) by GROUP_2:37
.= M * a * (M * d * (a" * a)) by GROUP_1:def 5
.= M * a * (M * (d * (a" * a))) by GROUP_2:107
.= M * a * M * (d * (a" * a)) by GROUP_3:11
.= M * (a * M) * (d * (a" * a)) by GROUP_3:13
.= M * (M * a) * (d * (a" * a)) by GROUP_3:117
.= M * ((M * a) * (d * (a" * a))) by GROUP_2:98
.= M * (M * (a * (d * (a" * a)))) by GROUP_2:107
.= M * (M * (a * (d * a" * a))) by GROUP_1:def 3
.= M * (M * (a * (d * a") * a)) by GROUP_1:def 3
.= M * (M * e * a) by GROUP_2:107
.= M * (e * M * a) by GROUP_3:117
.= M * (e * (M * a)) by GROUP_2:106
.= M * e * (M * a) by GROUP_3:12
.= V * S by A6,A7,Def3;
hence thesis by A8,GROUP_2:104;
end;
end;
hence thesis by GROUP_3:118;
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 Th14;
A2: [.S,T.] = 1_(G./.N) & 1_(G./.N) = carr N by A1,Th24,GROUP_5:37;
S" = a" * N & T" = b" * N by Th25;
then
A3: S" * T" = (a" * N) * (b" * N) by Def3;
S * T = (a * N) * (b * N) & [.S,T.] = (S" * T") * (S * T)
by Def3,GROUP_5:16;
then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) by A3,Def3;
then carr N = (a" * N) * (b" * N) * (a * (N * (b * N))) by A2,GROUP_3:10
.= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:13
.= (a" * N) * (b" * N) * (a * (b * N * N)) by GROUP_3:117
.= (a" * N) * (b" * N) * (a * (b * N)) by Th5
.= (a" * N) * (b" * N) * (a * b * N) by GROUP_2:105
.= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:10
.= a" * (N * b" * N) * (a * b * N) by GROUP_3:13
.= a" * (b" * N * N) * (a * b * N) by GROUP_3:117
.= a" * (b" * N) * (a * b * N) by Th5
.= (a" * b" * N) * (a * b * N) by GROUP_2:105
.= (a" * b") * (N * (a * b * N)) by GROUP_3:10
.= (a" * b") * (N * (a * b) * N) by GROUP_3:13
.= (a" * b") * ((a * b) * N * N) by GROUP_3:117
.= (a" * b") * ((a * b) * N) by Th5
.= (a" * b") * (a * b) * N by GROUP_2:105
.= [.a,b.] * N by GROUP_5:16;
hence [.a,b.] in N by GROUP_2:113;
end;
hence thesis by Th7;
end;
assume
A4: G` is Subgroup of N;
now
let S,T be Element of G./.N;
A5: [.S,T.] = (S" * T") * (S * T) by GROUP_5:16;
consider b being Element of G such that
A6: T = b * N and
T = N * b by Th13;
A7: T" = b" * N by A6,Th25;
consider a being Element of G such that
A8: S = a * N and
S = N * a by Th13;
S" = a" * N by A8,Th25;
then
A9: S" * T" = (a" * N) * (b" * N) by A7,Def3;
[.a,b.] in N by A4,Th7;
then
A10: carr N = [.a,b.] * N by GROUP_2:113
.= (a" * b") * (a * b) * N by GROUP_5:16
.= (a" * b") * ((a * b) * N) by GROUP_2:105
.= (a" * b") * ((a * b) * N * N) by Th5
.= (a" * b") * (N * (a * b) * N) by GROUP_3:117
.= (a" * b") * (N * (a * b * N)) by GROUP_3:13
.= (a" * b" * N) * (a * b * N) by GROUP_3:10
.= a" * (b" * N) * (a * b * N) by GROUP_2:105
.= a" * (b" * N * N) * (a * b * N) by Th5
.= a" * (N * b" * N) * (a * b * N) by GROUP_3:117
.= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:13
.= (a" * N) * (b" * N) * (a * b * N) by GROUP_3:10
.= (a" * N) * (b" * N) * (a * (b * N)) by GROUP_2:105
.= (a" * N) * (b" * N) * (a * (b * N * N)) by Th5
.= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:117
.= (a" * N) * (b" * N) * (a * (N * (b * N))) by GROUP_3:13
.= (a" * N) * (b" * N) * (a * N * (b * N)) by GROUP_3:10;
S * T = (a * N) * (b * N) by A8,A6,Def3;
then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) by A9,A5,Def3;
hence [.S,T.] = 1_(G./.N) by A10,Th24;
end;
hence thesis by GROUP_5:37;
end;
Lm1:
for G,H being unital non empty multMagma, f being Function of G,H holds
(for a being Element of G holds f.a = 1_H)
implies for a,b being Element of G holds f.(a * b) = f.a * f.b
proof
let G,H be unital non empty multMagma, f be Function of G,H;
assume
A1: for a being Element of G holds f.a = 1_H;
let a,b be Element of G;
thus f.(a * b) = 1_H by A1
.= 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 be non empty multMagma;
let f be Function of G, H;
attr f is multiplicative means
:Def6:
for a, b being Element of G holds f.(a * b) = f.a * f.b;
end;
registration
let G, H be unital non empty multMagma;
cluster multiplicative for Function of G, H;
existence
proof
take f = G --> 1_H;
for a being Element of G holds f.a = 1_H;
hence for a, b being Element of G holds f.(a * b) = f.a * f.b by Lm1;
end;
end;
registration
let A be commutative Group;
cluster inverse_op A -> multiplicative;
coherence
proof
for x,y being Element of A
holds (inverse_op A).(x * y) = ((inverse_op A).x) * ((inverse_op A).y)
proof
let x,y be Element of A;
thus (inverse_op A).(x * y) = (x * y)" by GROUP_1:def 6
.= (y ") * (x ") by GROUP_1:17
.= (x ") * ((inverse_op A).y) by GROUP_1:def 6
.= ((inverse_op A).x) * ((inverse_op A).y) by GROUP_1:def 6;
end;
hence thesis;
end;
end;
definition
let G,H;
mode Homomorphism of G,H is multiplicative Function of G, H;
end;
reserve g,h for Homomorphism of G,H;
reserve h1 for Homomorphism of H,I;
theorem Th31:
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 Def6;
hence thesis by GROUP_1:7;
end;
registration
let G,H;
cluster -> unity-preserving for Homomorphism of G,H;
coherence by Th31;
end;
theorem Th32:
g.(a") = (g.a)"
proof
g.(a") * g.a = g.(a" * a) by Def6
.= g.(1_G) by GROUP_1:def 5
.= 1_H by Th31;
hence thesis by GROUP_1:12;
end;
theorem Th33:
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 Def6
.= g.(b") * g.a * g.b by Def6
.= (g.b)" * g.a * g.b by Th32
.= (g.a) |^ (g.b) by GROUP_3:def 2;
end;
theorem Th34:
g. [.a,b.] = [.g.a,g.b.]
proof
thus g. [.a,b.] = g.(a" * b" * a * b) by GROUP_5:16
.= g.(a" * b" * a) * g.b by Def6
.= g.(a" * b") * g.a * g.b by Def6
.= g.(a") * g.(b") * g.a * g.b by Def6
.= (g.a)" * g.(b") * g.a * g.b by Th32
.= (g.a)" * (g.b)" * g.a * g.b by Th32
.= [.g.a,g.b.] by GROUP_5:16;
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 Th34
.= [.[.g.a1,g.a2.],g.a3.] by Th34
.= [.g.a1,g.a2,g.a3.] by GROUP_5:def 3;
end;
theorem Th36:
g.(a |^ n) = (g.a) |^ n
proof
defpred Q[Nat] means g.(a |^ $1) = (g.a) |^ $1;
A1: for n being Nat st Q[n] holds Q[n + 1]
proof
let n be Nat;
assume
A2: Q[n];
thus g.(a |^ (n + 1)) = g.(a |^ n * a) by GROUP_1:34
.= (g.a) |^ n * g.a by A2,Def6
.= (g.a) |^ (n + 1) by GROUP_1:34;
end;
g.(a |^ 0) = g.(1_G) by GROUP_1:25
.= 1_H by Th31
.= (g.a) |^ 0 by GROUP_1:25;
then
A3: Q[0];
for n being Nat holds Q[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
g.(a |^ i) = (g.a) |^ i
proof
per cases;
suppose
A1: i >= 0;
hence g.(a |^ i) = g.(a |^ |.i.|) by ABSVALUE:def 1
.= (g.a) |^ |.i.| by Th36
.= (g.a) |^ i by A1,ABSVALUE:def 1;
end;
suppose
A2: i < 0;
hence g.(a |^ i) = g.(a |^ |.i.|)" by GROUP_1:30
.= (g.(a |^ |.i.|))" by Th32
.= ((g.a) |^ |.i.|)" by Th36
.= (g.a) |^ i by A2,GROUP_1:30;
end;
end;
theorem Th38:
for G being non empty multMagma holds
id the carrier of G is multiplicative;
registration
let A be non empty multMagma;
cluster id A -> multiplicative;
coherence;
end;
theorem Th39:
for G,H,I being unital non empty multMagma,
h being multiplicative Function of G,H,
h1 being multiplicative Function of H,I holds
h1 * h is multiplicative
proof
let G,H,I be unital non empty multMagma,
h be multiplicative Function of G,H,
h1 be multiplicative Function of H,I;
set f = h1 * h;
let a,b be Element of G;
thus f.(a * b) = h1.(h.(a * b)) by FUNCT_2:15
.= h1.(h.a * h.b) by Def6
.= (h1.(h.a)) * (h1.(h.b)) by Def6
.= f.a * (h1.(h.b)) by FUNCT_2:15
.= f.a * f.b by FUNCT_2:15;
end;
registration
let G,H,I be unital non empty multMagma,
h be multiplicative Function of G,H,
h1 be multiplicative Function of H,I;
cluster h1 * h -> multiplicative for Function of G,I;
coherence by Th39;
end;
definition
let G,H be non empty multMagma;
func 1:(G,H) -> Function of G,H equals
G --> 1_H;
coherence;
end;
registration
let G,H be unital non empty multMagma;
cluster 1:(G,H) -> multiplicative;
coherence
proof
set f = 1:(G,H);
let a,b be Element of G;
for a being Element of G holds f.a = 1_H;
hence f.(a * b) = f.a * f.b by Lm1;
end;
end;
registration
let G1,G2 be Group;
cluster 1:(G1,G2) -> constant;
coherence;
end;
registration
let G1,G2 be Group;
cluster constant for Homomorphism of G1,G2;
existence
proof
take 1:(G1,G2);
thus thesis;
end;
end;
theorem
h1 * 1:(G,H) = 1:(G,I) & 1:(H,I) * h = 1:(G,I)
proof
thus h1 * 1:(G,H) = 1:(G,I)
proof
let a be Element of G;
thus (h1 * 1:(G,H)).a = h1.(1:(G,H).a) by FUNCT_2:15
.= 1_I by Th31
.= 1:(G,I).a;
end;
let a;
thus (1:(H,I) * h).a = 1:(H,I).(h.a) by FUNCT_2:15
.= 1:(G,I).a;
end;
definition
let G;
let N be normal Subgroup of G;
func nat_hom N -> Function of G,G./.N means
:Def8:
for a holds it.a = a * N;
existence
proof
defpred P[object,object] means ex a st $1 = a & $2 = a * N;
A1: for x being object st x in the carrier of G ex y being object st P[x,y]
proof
let x be object;
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
A2: dom f = the carrier of G and
A3: for x being object st x in the carrier of G holds P[x,f.x]
from CLASSES1:sch 1(A1);
rng f c= the carrier of G./.N
proof
let x be object;
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: f.y = x by FUNCT_1:def 3;
consider a such that
y = a and
A6: f.y = a * N by A2,A3,A4;
a * N = N * a by GROUP_3:117;
then x in G./.N by A5,A6,Th23;
hence thesis;
end;
then reconsider f as Function of G, G./.N by A2,FUNCT_2:def 1,RELSET_1:4;
take f;
let a;
ex b st a = b & f.a = b * N by A3;
hence thesis;
end;
uniqueness
proof
let n1,n2 be Function of G,G./.N such that
A7: for a holds n1.a = a * N and
A8: for a holds n2.a = a * N;
now
let a;
n1.a = a * N by A7;
hence n1.a = n2.a by A8;
end;
hence thesis;
end;
end;
registration
let G;
let N be normal Subgroup of G;
cluster nat_hom N -> multiplicative;
coherence
proof
set f = nat_hom N;
let a,b;
A1: f.a = a * N by Def8;
A2: f.b = b * N by Def8;
A3: f.(a*b) = a*b * N by Def8;
thus f.a * f.b = @(f.a) * @(f.b) by Def3
.= (a * N) * b * N by A1,A2,GROUP_3:9
.= a * (N * b) * N by GROUP_2:106
.= a * (b * N) * N by GROUP_3:117
.= a * ((b * N) * N) by GROUP_2:96
.= a * (b * N) by Th5
.= f.(a * b) by A3,GROUP_2:105;
end;
end;
definition
let G,H,g;
func Ker g -> strict Subgroup of G means
:Def9:
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 DOMAIN_1:sch 7;
A1: now
let a,b;
assume a in A & b in A;
then
A2: ( ex a1 st a1 = a & g.a1 = 1_H)& ex b1 st b1 = b & g.b1 = 1_H;
g.(a * b) = g.a * g.b by Def6
.= 1_H by A2,GROUP_1:def 4;
hence a * b in A;
end;
A3: now
let a;
assume a in A;
then ex a1 st a1 = a & g.a1 = 1_H;
then g.(a") = (1_H)" by Th32
.= 1_H by GROUP_1:8;
hence a" in A;
end;
g.(1_G) = 1_H by Th31;
then 1_G in A;
then consider B being strict Subgroup of G such that
A4: the carrier of B = A by A1,A3,GROUP_2:52;
reconsider B as strict Subgroup of G;
take B;
thus thesis by A4;
end;
uniqueness by GROUP_2:59;
end;
registration
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 DOMAIN_1:sch 7;
A1: now
let a,b;
assume a in A & b in A;
then
A2: ( ex a1 st a1 = a & g.a1 = 1_H)& ex b1 st b1 = b & g.b1 = 1_H;
g.(a * b) = g.a * g.b by Def6
.= 1_H by A2,GROUP_1:def 4;
hence a * b in A;
end;
A3: now
let a;
assume a in A;
then ex a1 st a1 = a & g.a1 = 1_H;
then g.(a") = (1_H)" by Th32
.= 1_H by GROUP_1:8;
hence a" in A;
end;
g.(1_G) = 1_H by Th31;
then 1_G in A;
then consider B being strict Subgroup of G such that
A4: the carrier of B = A by A1,A3,GROUP_2:52;
now
let a;
now
let b;
assume b in B |^ a;
then consider c being Element of G such that
A5: b = c |^ a and
A6: c in B by GROUP_3:58;
c in A by A4,A6;
then ex a1 st c = a1 & g.a1 = 1_H;
then g.b = (1_H) |^ (g.a) by A5,Th33
.= 1_H by GROUP_3:17;
then b in A;
hence b in B by A4;
end;
hence B |^ a is Subgroup of B by GROUP_2:58;
end;
then B is normal Subgroup of G by GROUP_3:122;
hence thesis by A4,Def9;
end;
end;
theorem Th41:
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;
then a in {b : h.b = 1_H} by Def9;
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 Def9;
hence thesis;
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;
hence a in Ker 1:(G,H) by Th41;
end;
hence thesis by GROUP_2:62;
end;
theorem Th43:
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
A1: (nat_hom N).a = 1_(G./.N) by Th41;
(nat_hom N).a = a * N & 1_(G./.N) = carr N by Def8,Th24;
hence thesis by A1,GROUP_2:113;
end;
assume a in N;
then
A2: a * N = carr N by GROUP_2:113;
(nat_hom N).a = a * N & 1_(G./.N) = carr N by Def8,Th24;
hence thesis by A2,Th41;
end;
definition
let G,H,g;
func Image g -> strict Subgroup of H means
:Def10:
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: now
let c,d;
assume that
A2: c in S and
A3: d in S;
consider b such that
b in X and
A4: d = g.b by A3,FUNCT_2:65;
consider a such that
a in X and
A5: c = g.a by A2,FUNCT_2:65;
c * d = g.(a * b) by A5,A4,Def6;
hence c * d in S by FUNCT_2:35;
end;
A6: now
let c;
assume c in S;
then consider a such that
a in X and
A7: c = g.a by FUNCT_2:65;
g.(a") = c" by A7,Th32;
hence c" in S by FUNCT_2:35;
end;
dom g = the carrier of G by FUNCT_2:def 1;
then consider D being strict Subgroup of H such that
A8: the carrier of D = S by A1,A6,GROUP_2:52;
take D;
thus thesis by A8;
end;
uniqueness by GROUP_2:59;
end;
theorem Th44:
rng g = the carrier of Image g
proof
the carrier of Image g = g .: (the carrier of G) by Def10
.= g .: (dom g) by FUNCT_2:def 1
.= rng g by RELAT_1:113;
hence thesis;
end;
theorem Th45:
for x being object holds x in Image g iff ex a st x = g.a
proof let x be object;
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;
then x in g .: (the carrier of G) by Def10;
then consider y being object such that
y in dom g and
A1: y in the carrier of G and
A2: g.y = x by FUNCT_1:def 6;
reconsider y as Element of G by A1;
take y;
thus thesis by A2;
end;
given a such that
A3: x = g.a;
the carrier of G = dom g by FUNCT_2:def 1;
then x in g .: (the carrier of G) by A3,FUNCT_1:def 6;
then x in the carrier of Image g by Def10;
hence thesis;
end;
theorem
Image g = gr rng g
proof
rng g = the carrier of Image g & the carrier of Image g = carr Image g
by Th44;
hence thesis by GROUP_4:31;
end;
theorem
Image 1:(G,H) = (1).H
proof
set g = 1:(G,H);
A1: the carrier of Image g c= {1_H}
proof
let x be object;
assume x in the carrier of Image g;
then x in g .: (the carrier of G) by Def10;
then consider y being object such that
y in dom g and
A2: y in the carrier of G and
A3: g.y = x by FUNCT_1:def 6;
reconsider y as Element of G by A2;
g.y = 1_H;
hence thesis by A3,TARSKI:def 1;
end;
1_H in Image g by GROUP_2:46;
then 1_H in the carrier of Image g;
then {1_H} c= the carrier of Image g by ZFMISC_1:31;
then the carrier of Image g = {1_H} by A1;
hence thesis by GROUP_2:def 7;
end;
theorem Th48:
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 and
S = N * a by Th13;
(nat_hom N).a = a * N by Def8;
hence S in Image nat_hom N by A1,Th45;
end;
hence thesis by GROUP_2:62;
end;
theorem Th49:
h is Homomorphism of G,Image h
proof
rng h = the carrier of Image h & dom h = the carrier of G by Th44,
FUNCT_2:def 1;
then reconsider f9 = h as Function of G, Image h by RELSET_1:4;
now
let a,b;
thus f9.a * f9.b = h.a * h.b by GROUP_2:43
.= f9.(a * b) by Def6;
end;
hence thesis by Def6;
end;
theorem Th50:
G is finite implies Image g is finite
proof
assume G is finite;
then g .: (the carrier of G) is finite;
hence thesis by Def10;
end;
registration
let G be finite Group;
let H be Group;
let g be Homomorphism of G,H;
cluster Image g -> finite;
coherence by Th50;
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:42;
h1 in Image g;
then consider a such that
A2: h1 = g.a by Th45;
h2 in Image g;
then consider b such that
A3: h2 = g.b by Th45;
thus h1 * h2 = c * d by GROUP_2:43
.= g.(a * b) by A2,A3,Def6
.= g.(b * a) by A1,Lm2
.= d * c by A2,A3,Def6
.= h2 * h1 by GROUP_2:43;
end;
theorem Th52:
card Image g c= card G
proof
card (g .: (the carrier of G)) c= card (the carrier of G) by CARD_1:67;
hence thesis by Def10;
end;
theorem
for G being finite Group, H being Group, g being Homomorphism of G,H
holds card Image g <= card G
proof let G be finite Group, H be Group, g be Homomorphism of G,H;
Segm card Image g c= Segm card G by Th52;
hence thesis by NAT_1:39;
end;
theorem
h is one-to-one & c in Image h implies h.(h".c) = c
proof
reconsider h9 = h as Function of G,Image h by Th49;
assume that
A1: h is one-to-one and
A2: c in Image h;
A3: rng h9 = the carrier of Image h by Th44;
c in the carrier of Image h by A2;
hence thesis by A1,A3,FUNCT_1:35;
end;
theorem
h is one-to-one implies h" is Homomorphism of Image h,G
proof
assume
A1: h is one-to-one;
reconsider Imh = Image h as Group;
h is Function of G,Imh & rng h = the carrier of Imh by Th44,Th49;
then reconsider h9 = h" as Function of Imh, G by A1,FUNCT_2:25;
now
let a,b be Element of Imh;
reconsider a9 = a, b9 = b as Element of H by GROUP_2:42;
a9 in Imh;
then consider a1 being Element of G such that
A2: h.a1 = a9 by Th45;
b9 in Imh;
then consider b1 being Element of G such that
A3: h.b1 = b9 by Th45;
thus h9.(a * b) = h9.(h.a1 * h.b1) by A2,A3,GROUP_2:43
.= h9.(h.(a1 * b1)) by Def6
.= a1 * b1 by A1,FUNCT_2:26
.= h9.a * b1 by A1,A2,FUNCT_2:26
.= h9.a * h9.b by A1,A3,FUNCT_2:26;
end;
hence thesis by Def6;
end;
theorem Th56:
h is one-to-one iff Ker h = (1).G
proof
thus h is one-to-one implies Ker h = (1).G
proof
assume
A1: h is one-to-one;
now
let x be object;
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;
then x in G by GROUP_2:40;
then reconsider a = x as Element of G;
a in Ker h by A2;
then h.a = 1_H by Th41
.= h.(1_G) by Th31;
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,Th31;
then a in Ker h by Th41;
hence thesis;
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 Def6
.= h.(1_G) by GROUP_1:def 5
.= 1_H by Th31;
then 1_H = h.(b * a") by A6,Def6;
then b * a" in Ker h by Th41;
then
A7: b * a" in the carrier of Ker h;
a = 1_G * a by GROUP_1:def 4
.= b * a" * a by A4,A7,TARSKI:def 1
.= b * (a" * a) by GROUP_1:def 3
.= 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;
hence thesis by Th1;
end;
theorem Th57:
for H being strict Group, h being Homomorphism of G,H holds
h is onto iff Image h = H
proof
let H be strict Group, h be Homomorphism of G,H;
thus h is onto implies Image h = H
proof
assume rng h = the carrier of H;
then the carrier of Image h = the carrier of H by Th44;
hence thesis by GROUP_2:61;
end;
assume
A1: Image h = H;
the carrier of H c= rng h
proof
let x be object;
assume x in the carrier of H;
then x in h .: (the carrier of G) by A1,Def10;
then ex y being object st y in dom h & y in the carrier of G & h.y = x
by FUNCT_1:def 6;
hence thesis by FUNCT_1:def 3;
end;
then rng h = the carrier of H;
hence thesis;
end;
theorem Th58:
for G,H being non empty set, h being Function of G,H holds
h is onto iff
for c being Element of H ex a being Element of G st h.a = c
proof
let G,H be non empty set, h be Function of G,H;
hereby assume
h is onto; then
A1: rng h = H;
let c be Element of H;
ex a being object st a in G & h.a = c by A1,FUNCT_2:11;
hence ex a being Element of G st h.a = c;
end;
assume
A2: for c being Element of H ex a being Element of G st h.a = c;
for y being object st y in H
ex x being object st x in G & y = h.x
proof
let y be object;
assume y in H;
then reconsider y0 = y as Element of H;
ex x being Element of G st h.x = y0 by A2;
hence thesis;
end;
then rng h = H by FUNCT_2:10;
hence h is onto;
end;
theorem Th59:
for N being normal Subgroup of G holds nat_hom N is onto
proof
let N be normal Subgroup of G;
Image nat_hom N = G./.N by Th48;
hence thesis by Th57;
end;
theorem
for G,H being set for h being Function of G,H holds
h is bijective iff rng h = H & h is one-to-one by FUNCT_2:def 3;
theorem
for G being set, H being non empty set for h being Function of G,H holds
h is bijective implies dom h = G & rng h = H by FUNCT_2:def 1,def 3;
theorem Th62:
for H being Group, h being Homomorphism of G,H st
h is bijective holds h" is Homomorphism of H,G
proof
let H be Group, h be Homomorphism of G,H;
assume
A1: h is bijective;
then
A2: h is one-to-one & rng h = the carrier of H by FUNCT_2:def 3;
then reconsider h1 = h" as Function of H,G by FUNCT_2:25;
now
let a,b be Element of H;
set a1 = h1.a, b1 = h1.b;
h.a1 = a & h.b1 = b by A2,FUNCT_1:32;
hence h1.(a * b) = h1.(h.(a1 * b1)) by Def6
.= h1.a * h1.b by A1,FUNCT_2:26;
end;
hence thesis by Def6;
end;
theorem Th63:
for G being set, H being non empty set for h being Function of G,H holds
for g1 being Function of H,G holds
h is bijective & g1 = h" implies g1 is bijective
proof
let G be set,H be non empty set;
let h be Function of G,H, g1 be Function of H,G;
assume
A1: h is bijective & g1 = h";
then dom h = G & rng g1 = dom h by FUNCT_1:33,FUNCT_2:def 1;
hence thesis by A1,FUNCT_2:def 3;
end;
theorem Th64:
for G being set, H,I being non empty set for h being Function of G,H holds
for h1 being Function of H,I holds
h is bijective & h1 is bijective implies h1 * h is bijective
proof
let G be set,H,I be non empty set;
let h be Function of G,H, h1 be Function of H,I;
assume that
A1: h is bijective and
A2: h1 is bijective;
dom h1 = H & rng h = H by A1,FUNCT_2:def 3,def 1;
then rng(h1 * h) = rng h1 by RELAT_1:28
.= I by A2,FUNCT_2:def 3;
hence thesis by A1,A2,FUNCT_2:def 3;
end;
theorem Th65:
for G being Group holds nat_hom (1).G is bijective
proof
let G be Group;
set g = nat_hom (1).G;
Ker g = (1).G by Th43;
then g is one-to-one by Th56;
hence thesis by Th59;
end;
definition
let G,H;
pred G,H are_isomorphic means
:Def11:
ex h st h is bijective;
reflexivity
proof
let G;
reconsider i = id the carrier of G as Homomorphism of G,G by Th38;
i is bijective;
hence thesis;
end;
end;
theorem Th66:
for G,H being Group holds G,H are_isomorphic implies
H,G are_isomorphic
proof
let G,H be Group;
assume G,H are_isomorphic;
then consider h being Homomorphism of G,H such that
A1: h is bijective;
reconsider g = h" as Homomorphism of H,G by A1,Th62;
take g;
thus thesis by A1,Th63;
end;
definition
let G,H be Group;
redefine pred G,H are_isomorphic; :: redefines are_isomorphic (GROUP_6, definition)
symmetry by Th66;
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 bijective by A1;
consider h1 such that
A4: h1 is bijective by A2;
(h1 * g) is bijective by A3,A4,Th64;
hence thesis;
end;
theorem
h is one-to-one implies G,Image h are_isomorphic
proof
reconsider ih = h as Homomorphism of G,Image h by Th49;
assume
A1: h is one-to-one;
take ih;
ih is onto by Th44;
hence thesis by A1;
end;
:: generalized by SK, 14.04.2025
theorem Th69:
for G, H being trivial Group holds G,H are_isomorphic
proof
let G, H be trivial Group;
set h = 1:(G,H);
consider x being object such that
A1: the carrier of G = { x } by ZFMISC_1:131;
reconsider x as Element of G by A1, TARSKI:def 1;
consider y being object such that
A2: the carrier of H = { y } by ZFMISC_1:131;
reconsider y as Element of H by A2, TARSKI:def 1;
A4: 1_H = y by A2, TARSKI:def 1;
now
let z be object;
hereby
assume z in the carrier of H;
then A5: z = y by A2, TARSKI:def 1;
reconsider x as object;
take x;
thus x in dom h;
thus z = ((the carrier of G) --> 1_H).1_G by A4, A5
.= h.x;
end;
given a being object such that
A6: a in dom h & z = h.a;
A7: z in rng h by A6, FUNCT_1:3;
{ 1_H } = rng((the carrier of G) --> 1_H) by FUNCOP_1:8
.= rng h;
then z = 1_H by A7, TARSKI:def 1;
hence z in the carrier of H;
end;
then A8: rng h = the carrier of H by FUNCT_1:def 3;
now
let a,b be object;
assume a in dom h & b in dom h & h.a = h.b;
then a in dom(G --> 1_H) & b in dom(G --> 1_H);
then a = x & b = x by A1, TARSKI:def 1;
hence a = b;
end;
then h is one-to-one by FUNCT_1:def 4;
then h is bijective by A8, FUNCT_2:def 3;
hence thesis;
end;
theorem
(1).G,(1).H are_isomorphic by Th69;
theorem
for G being Group holds G,G./.(1).G are_isomorphic
proof
let G be Group;
nat_hom (1).G is bijective by Th65;
hence thesis;
end;
theorem
for G being Group holds G./.(Omega).G is trivial
proof
let G be Group;
the carrier of G./.(Omega).G = {the carrier of G} by GROUP_2:142;
hence thesis;
end;
theorem Th73:
for G,H being strict Group holds G,H are_isomorphic implies card G = card H
proof
let G,H be strict Group;
assume
A1: G,H are_isomorphic;
then consider h being Homomorphism of G,H such that
A2: h is bijective;
consider g1 being Homomorphism of H,G such that
A3: g1 is bijective by A1,Def11;
Image g1 = G by A3,Th57;
then
A4: card G c= card H by Th52;
Image h = H by A2,Th57;
hence thesis by A4,Th52;
end;
theorem Th74:
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 bijective by A1;
rng h = the carrier of H by A3,FUNCT_2:def 3;
hence thesis by A2;
end;
theorem
for G,H being strict Group holds G,H are_isomorphic implies card G = card H
by Th73;
theorem
for G being strict trivial Group, H being strict Group holds
G,H are_isomorphic implies H is trivial
proof
let G be strict trivial Group, H be strict Group;
assume
A1: G,H are_isomorphic;
then reconsider H as finite Group by Th74;
card G = 1 by Th11;
then card H = 1 by A1,Th73;
hence thesis by Th11;
end;
theorem
for H being Group st G,H are_isomorphic & G is commutative
holds H is commutative
proof
let H be Group;
assume that
A1: G,H are_isomorphic and
A2: G is commutative;
consider h being Homomorphism of G,H such that
A3: h is bijective by A1;
now
let c,d be Element of H;
consider a such that
A4: h.a = c by A3,Th58;
consider b such that
A5: h.b = d by A3,Th58;
thus c * d = h.(a * b) by A4,A5,Def6
.= h.(b * a) by A2
.= d * c by A4,A5,Def6;
end;
hence thesis;
end;
Lm3: G./.Ker g,Image g are_isomorphic & ex h being Homomorphism of G./.Ker g,
Image g st h is bijective & 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: dom nat_hom Ker g = the carrier of G by FUNCT_2:def 1;
A2: 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
A3: S = a * Ker g and
S = Ker g * a by Th13;
g.a in J by Th45;
then reconsider T = g.a as Element of J;
take T;
let b;
assume S = b * Ker g;
then a" * b in Ker g by A3,GROUP_2:114;
then 1_H = g.(a" * b) by Th41
.= g.(a") * g.b by Def6
.= (g.a)" * g.b by Th32;
then g.b = (g.a)"" by GROUP_1:12;
hence thesis;
end;
consider f being Function of I,J such that
A4: for S being Element of I holds P[S,f.S] from FUNCT_2:sch 3(A2);
now
let S,T be Element of G./.Ker g;
consider a such that
A5: S = a * Ker g and
S = Ker g * a by Th13;
consider b such that
A6: T = b * Ker g and
A7: T = Ker g * b by Th13;
A8: f.T = g.b by A4,A6;
f.S = g.a by A4,A5;
then
A9: f.S * f.T = g.a * g.b by A8,GROUP_2:43
.= g.(a * b) by Def6;
S * T = (a * Ker g) * (Ker g * b) by A5,A7,Def3
.= (a * Ker g) * Ker g * b by GROUP_3:11
.= a * Ker g * b by Th5
.= a * (Ker g * b) by GROUP_2:106
.= a * (b * Ker g) by GROUP_3:117
.= a * b * Ker g by GROUP_2:105;
hence f.(S * T) = f.S * f.T by A4,A9;
end;
then reconsider f as Homomorphism of G./.Ker g,J by Def6;
A10: f is one-to-one
proof
let y1,y2 be object;
assume y1 in dom f & y2 in dom f;
then reconsider S = y1, T = y2 as Element of I;
assume
A11: f.y1 = f.y2;
consider a such that
A12: S = a * Ker g and
S = Ker g * a by Th13;
consider b such that
A13: T = b * Ker g and
T = Ker g * b by Th13;
A14: f.T = g.b by A4,A13;
f.S = g.a by A4,A12;
then (g.b)" * g.a = 1_H by A11,A14,GROUP_1:def 5;
then 1_H = g.(b") * g.a by Th32
.= g.(b" * a) by Def6;
then b" * a in Ker g by Th41;
hence thesis by A12,A13,GROUP_2:114;
end;
A15: dom g = the carrier of G by FUNCT_2:def 1;
A16: now
let x be object;
thus x in dom g implies x in dom nat_hom Ker g & (nat_hom Ker g).x in dom f
proof
assume
A17: x in dom g;
hence x in dom nat_hom Ker g by A1;
A18: dom f = the carrier of I by FUNCT_2:def 1;
(nat_hom Ker g).x in rng nat_hom Ker g by A1,A17,FUNCT_1:def 3;
hence thesis by A18;
end;
assume that
A19: x in dom nat_hom Ker g and
(nat_hom Ker g).x in dom f;
thus x in dom g by A15,A19;
end;
the carrier of J c= rng f
proof
let x be object;
assume x in the carrier of J;
then x in Image g;
then consider a such that
A20: x = g.a by Th45;
reconsider S = a * Ker g as Element of I by Th14;
f.S = g.a & the carrier of I = dom f by A4,FUNCT_2:def 1;
hence thesis by A20,FUNCT_1:def 3;
end;
then
A21: rng f = the carrier of J;
then f is bijective by A10,FUNCT_2:def 3;
hence G./.Ker g,Image g are_isomorphic;
take f;
thus f is bijective by A21,A10,FUNCT_2:def 3;
now
let x be object;
assume x in dom g;
then reconsider a = x as Element of G;
(nat_hom Ker g).a = a * Ker g by Def8;
hence g.x = f.((nat_hom Ker g).x) by A4;
end;
hence thesis by A16,FUNCT_1:10;
end;
theorem
G./.Ker g, Image g are_isomorphic by Lm3;
::$N First isomorphism theorem for groups
theorem
ex h being Homomorphism of G./.Ker g,Image g st
h is bijective & g = h * nat_hom Ker g by Lm3;
::$N Third isomorphism theorem for groups
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 Th13;
reconsider y = a * N as Element of G./.N by Th14;
take y;
let b;
assume x = b * M;
then a" * b in M by A4,GROUP_2:114;
then a" * b in N by A2,GROUP_2:40;
hence thesis by GROUP_2:114;
end;
consider f being Function of G./.M, G./.N such that
A5: for x being Element of G./.M holds P[x,f.x] from FUNCT_2:sch 3(A3);
now
let x,y be Element of G./.M;
consider a such that
A6: x = a * M and
x = M * a by Th13;
consider b such that
A7: y = b * M and
y = M * b by Th13;
A8: x * y = @x * @y by Def3
.= a * M * b * M by A6,A7,GROUP_3:9
.= a * (M * b) * M by GROUP_2:106
.= a * (b * M) * M by GROUP_3:117
.= a * ((b * M) * M) by GROUP_2:96
.= a * (b * M) by Th5
.= a * b * M by GROUP_2:105;
A9: f.y = b * N by A5,A7;
A10: f.x = a * N by A5,A6;
f.x * f.y = @(f.x) * @(f.y) by Def3
.= a * N * b * N by A10,A9,GROUP_3:9
.= a * (N * b) * N by GROUP_2:106
.= a * (b * N) * N by GROUP_3:117
.= a * ((b * N) * N) by GROUP_2:96
.= a * (b * N) by Th5
.= a * b * N by GROUP_2:105;
hence f.(x * y) = f.x * f.y by A5,A8;
end;
then reconsider f as Homomorphism of G./.M,G./.N by Def6;
A11: 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
A12: f.S = 1_(G./.N) by Th41
.= carr N by Th24;
consider a such that
A13: S = a * M and
A14: S = M * a by Th13;
f.S = a * N by A5,A13;
then a in N by A12,GROUP_2:113;
then reconsider q = a as Element of N;
(N,M)`*` = M by A2,Def1;
then S = q * (N,M)`*` & S = (N,M)`*` * q by A13,A14,Th2;
hence thesis by A1,Th23;
end;
assume S in J;
then consider a being Element of N such that
A15: S = a * (N,M)`*` and
S = (N,M)`*` * a by A1,Th23;
reconsider a9 = a as Element of G by GROUP_2:42;
(N,M)`*` = M by A2,Def1;
then S = a9 * M by A15,Th2;
then
A16: f.S = a9 * N by A5;
a in N;
then f.S = carr N by A16,GROUP_2:113
.= 1_(G./.N) by Th24;
hence thesis by Th41;
end;
the carrier of G./.N c= rng f
proof
let x be object;
assume x in the carrier of G./.N;
then x in G./.N;
then consider a such that
A17: x = a * N and
x = N * a by Th23;
reconsider S = a * M as Element of G./.M by Th14;
f.S = a * N & dom f = the carrier of G./.M by A5,FUNCT_2:def 1;
hence thesis by A17,FUNCT_1:def 3;
end;
then rng f = the carrier of G./.N;
then f is onto;
then Image f = G./.N by Th57;
hence thesis by A11,Lm3;
end;
::$N Second isomorphism theorem for groups
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: the carrier of B c= the carrier of G by GROUP_2:def 5;
A2: dom g = dom f /\ (the carrier of B) & dom f = the carrier of G by
FUNCT_2:def 1,RELAT_1:61;
then
A3: dom g = the carrier of B by A1,XBOOLE_1:28;
A4: N is Subgroup of B "\/" N by GROUP_4:60;
then
A5: N = (B "\/" N,N)`*` by Def1;
A6: B is Subgroup of B "\/" N by GROUP_4:60;
rng g c= the carrier of I
proof
let y be object;
assume y in rng g;
then consider x being object such that
A7: x in dom g and
A8: g.x = y by FUNCT_1:def 3;
reconsider x as Element of B by A2,A1,A7,XBOOLE_1:28;
reconsider x9 = x as Element of G by GROUP_2:42;
reconsider x99 = x as Element of B "\/" N by A6,GROUP_2:42;
A9: x99 * (B "\/" N,N)`*` = x9 * N & N * x9 = (B "\/" N,N)`*` * x99 by A5,Th2;
A10: g.x = f.x9 by A7,FUNCT_1:47
.= x9 * N by Def8;
then g.x = N * x9 by GROUP_3:117;
then y in I by A8,A10,A9,Th23;
hence thesis;
end;
then reconsider g as Function of B, (B "\/" N)./.(B "\/" N,N)`*` by A3,
FUNCT_2:def 1,RELSET_1:4;
A11: I is Subgroup of G./.N by A4,Th28;
now
let a,b be Element of B;
reconsider a9 = a, b9 = b as Element of G by GROUP_2:42;
A12: f.a9 = g.a & f.b9 = g.b by FUNCT_1:49;
a * b = a9 * b9 by GROUP_2:43;
hence g.(a * b) = f.(a9 * b9) by FUNCT_1:49
.= f.a9 * f.b9 by Def6
.= g.a * g.b by A11,A12,GROUP_2:43;
end;
then reconsider g as Homomorphism of B,(B "\/" N)./.(B "\/" N,N)`*` by Def6;
A13: Ker g = B /\ N
proof
let b be Element of B;
reconsider c = b as Element of G by GROUP_2:42;
A14: g.b = f.c by FUNCT_1:49
.= c * N by Def8;
thus b in Ker g implies b in B /\ N
proof
assume b in Ker g;
then g.b = 1_I by Th41
.= carr J by Th24
.= carr N by A4,Def1;
then b in B & b in N by A14,GROUP_2:113;
hence thesis by GROUP_2:82;
end;
assume b in B /\ N;
then b in N by GROUP_2:82;
then c * N = carr J by A5,GROUP_2:113
.= 1_I by Th24;
hence thesis by A14,Th41;
end;
the carrier of I c= rng g
proof
let x be object;
assume x in the carrier of I;
then x in I;
then consider b being Element of B "\/" N such that
A15: x = b * J and
x = J * b by Th23;
B * N = N * B & b in B "\/" N by GROUP_5:8;
then consider a1,a2 such that
A16: b = a1 * a2 and
A17: a1 in B and
A18: a2 in N by GROUP_5:5;
A19: a1 in the carrier of B by A17;
x = a1 * a2 * N by A5,A15,A16,Th2
.= a1 * (a2 * N) by GROUP_2:105
.= a1 * N by A18,GROUP_2:113
.= f.a1 by Def8
.= g.a1 by A19,FUNCT_1:49;
hence thesis by A3,A19,FUNCT_1:def 3;
end;
then the carrier of I = rng g;
then g is onto;
then Image g = (B "\/" N)./.(B "\/" N,N)`*` by Th57;
hence thesis by A13,Lm3;
end;