:: On Rough Subgroup of a Group
:: by Xiquan Liang and Dailu Li
::
:: Received August 7, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GROUP_1, XBOOLE_0, SUBSET_1, GROUP_2, PRE_TOPC, RELAT_1, TARSKI,
STRUCT_0;
notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2,
GROUP_3, GROUP_4;
constructors REALSET2, GROUP_4;
registrations XBOOLE_0, STRUCT_0, GROUP_1, GROUP_2, GROUP_3;
requirements SUBSET, BOOLE;
definitions XBOOLE_0, TARSKI;
equalities GROUP_2, GROUP_4;
expansions TARSKI;
theorems GROUP_1, GROUP_8, GROUP_2, GROUP_3, XBOOLE_0, XBOOLE_1, GROUP_4,
STRUCT_0;
begin :: Preliminaries
reserve G for Group;
reserve A,B for non empty Subset of G;
reserve N,H,H1,H2 for Subgroup of G;
reserve x,a,b for Element of G;
theorem Th1:
for N be normal Subgroup of G,x1,x2 be Element of G holds
(x1 * N) * (x2 * N) = (x1 * x2) * N
proof
let N be normal Subgroup of G,x1,x2 be Element of G;
(x1 * N) * (x2 * N) = x1 * N * x2 * N by GROUP_2:10
.= x1 * (N * x2) * N by GROUP_2:29
.= x1 * (x2 * N) * N by GROUP_3:117
.= (x1 * x2) * N * N by GROUP_2:105
.= (x1 * x2) * (N * N) by GROUP_2:29;
hence thesis by GROUP_2:76;
end;
theorem Th2:
for G being Group,N being Subgroup of G, x, y being Element of G
st y in x * N holds x * N = y * N
proof
let G be Group,N be Subgroup of G,x,y be Element of G;
assume
A1:y in x * N;
y in y * N by GROUP_2:108;
then x * N meets y * N by A1,XBOOLE_0:3;
hence thesis by GROUP_2:115;
end;
theorem Th3:
for N being Subgroup of G,H being Subgroup of G,
x being Element of G st x * N meets carr(H)
ex y being Element of G st y in x * N & y in H
proof
let N be Subgroup of G,H being Subgroup of G, x being Element of G;
assume x * N meets carr(H);
then consider y be object such that
A1: y in x * N & y in carr(H) by XBOOLE_0:3;
reconsider y as Element of G by A1;
y in H by A1,STRUCT_0:def 5;
hence thesis by A1;
end;
theorem Th4:
for x,y being Element of G, N be normal Subgroup of G
st y in N holds x * y * x" in N
proof
let x,y be Element of G, N be normal Subgroup of G;
assume y in N;
then x * y in x * N by GROUP_2:103;
then x * y in N * x by GROUP_3:117;
then consider y1 be Element of G such that
A1: x * y = y1 * x & y1 in N by GROUP_2:104;
x * y * x" = y1 * (x * x") by A1,GROUP_1:def 3
.= y1 * 1_G by GROUP_1:def 5
.= y1 by GROUP_1:def 4;
hence thesis by A1;
end;
theorem Th5:
for N be Subgroup of G
st for x,y being Element of G st y in N holds x * y * x" in N
holds N is normal
proof
let N be Subgroup of G such that
A1:for x,y being Element of G st y in N holds x * y * x" in N;
for x be Element of G holds x * N c= N * x
proof
let x be Element of G;
let z be object;
assume
A2:z in x * N;
then reconsider z as Element of G;
consider z1 be Element of G such that
A3: z = x * z1 & z1 in N by A2,GROUP_2:103;
A4: x * z1 * x" in N by A1,A3;
(x * z1 * x") * x = z by A3,GROUP_3:1;
hence thesis by A4,GROUP_2:104;
end;
hence thesis by GROUP_3:118;
end;
theorem Th6:
x in H1 * H2 iff ex a,b st x = a * b & a in H1 & b in H2
proof
thus x in H1 * H2 implies ex a,b st x = a * b & a in H1 & b in H2
proof
assume x in H1 * H2;
then consider a,b such that
A1: x = a * b & a in carr(H1) & b in carr(H2);
a in H1 & b in H2 by A1,STRUCT_0:def 5;
hence thesis by A1;
end;
given a,b such that
A2: x = a * b & a in H1 & b in H2;
a in carr(H1) & b in carr(H2) by A2,STRUCT_0:def 5;
hence thesis by A2;
end;
theorem Th7:
for G being Group, N1,N2 being strict normal Subgroup of G
ex M being strict Subgroup of G st the carrier of M = N1 * N2
proof
let G be Group, N1,N2 be strict normal Subgroup of G;
A1:1_G in N1 * N2
proof
A2: 1_G in N1 & 1_G in N2 by GROUP_2:46;
1_G * 1_G = 1_G by GROUP_1:def 4;
hence thesis by A2,Th6;
end;
A3:for x,y being Element of G holds x in N1 * N2 & y in N1 * N2
implies x * y in N1 * N2
proof
let x,y be Element of G;
assume that
A4: x in N1 * N2 and
A5: y in N1 * N2;
consider a,b be Element of G such that
A6: x = a * b & a in N1 & b in N2 by A4,Th6;
consider c,d be Element of G such that
A7: y = c * d & c in N1 & d in N2 by A5,Th6;
A8: x * y = ((a * b) * c) * d by A6,A7,GROUP_1:def 3
.= a * (b * c) * d by GROUP_1:def 3;
b * c in N2 * N1 by A6,A7,Th6;
then b * c in N1 * N2 by GROUP_3:125;
then consider b9,c9 be Element of G such that
A9: b * c = b9 * c9 & b9 in N1 & c9 in N2 by Th6;
A10: x * y = ((a * b9) * c9) * d by A8,A9,GROUP_1:def 3
.= (a * b9) * (c9 * d) by GROUP_1:def 3;
A11: a * b9 in N1 by A6,A9,GROUP_2:50;
c9* d in N2 by A7,A9,GROUP_2:50;
hence thesis by A10,A11,Th6;
end;
for x being Element of G holds x in N1 * N2 implies x" in N1 * N2
proof
let x be Element of G;
assume x in N1 * N2;
then consider a,b be Element of G such that
A12: x = a * b & a in N1 & b in N2 by Th6;
A13: x" = b" * a" by A12,GROUP_1:17;
b" in N2 & a" in N1 by A12,GROUP_2:51;
then
x" in N2 * N1 by A13,Th6;
hence thesis by GROUP_3:125;
end;
hence thesis by A1,A3,GROUP_2:52;
end;
theorem Th8:
for G being Group, N1,N2 being strict normal Subgroup of G
ex M being strict normal Subgroup of G st the carrier of M = N1 * N2
proof
let G be Group, N1,N2 be strict normal Subgroup of G;
consider M being strict Subgroup of G such that
A1:the carrier of M = N1 * N2 by Th7;
for x,y be Element of G st y in M holds x * y * x" in M
proof
let x,y be Element of G;
assume y in M;
then y in the carrier of M by STRUCT_0:def 5;
then consider a,b be Element of G such that
A2: y = a * b & a in N1 & b in N2 by A1,Th6;
A3: x * y * x" =((x * a) * b) * x" by A2,GROUP_1:def 3
.=(x * a) * (b * x") by GROUP_1:def 3
.=(x * a) * 1_G * (b * x") by GROUP_1:def 4
.=(x * a) * (x" * x) * (b * x") by GROUP_1:def 5
.=(x * a) * x" * x * (b * x") by GROUP_1:def 3
.=((x * a) * x") * (x * (b * x")) by GROUP_1:def 3
.=(x * a * x") * (x * b * x") by GROUP_1:def 3;
x * a * x" in N1 & x * b * x" in N2 by A2,Th4;
then x * y * x" in N1 * N2 by A3,Th6;
hence thesis by A1,STRUCT_0:def 5;
end;
then M is normal Subgroup of G by Th5;
hence thesis by A1;
end;
theorem Th9:
for G being Group, N,N1,N2 being Subgroup of G st
the carrier of N = N1 * N2 holds N1 is Subgroup of N & N2 is Subgroup of N
proof
let G be Group, N,N1,N2 be Subgroup of G;
assume
A1:the carrier of N = N1 * N2;
for x be Element of G st x in N1 holds x in N
proof
let x be Element of G;
assume
A2: x in N1;
A3: 1_ G in N2 by GROUP_2:46;
x = x * 1_ G by GROUP_1:def 4;
then x in N1 * N2 by A2,A3,Th6;
hence thesis by A1,STRUCT_0:def 5;
end;
hence N1 is Subgroup of N by GROUP_2:58;
for y be Element of G st y in N2 holds y in N
proof
let y be Element of G;
assume
A4: y in N2;
A5: 1_ G in N1 by GROUP_2:46;
y = 1_ G * y by GROUP_1:def 4;
then y in N1 * N2 by A4,A5,Th6;
hence thesis by A1,STRUCT_0:def 5;
end;
hence N2 is Subgroup of N by GROUP_2:58;
end;
theorem Th10:
for N,N1,N2 be normal Subgroup of G,a,b be Element of G st
the carrier of N = N1 * N2 holds (a * N1) * (b * N2) = (a * b) * N
proof
let N,N1,N2 be normal Subgroup of G;
let a,b be Element of G;
assume
A1: the carrier of N = N1 * N2;
(a * N1) * (b * N2) = a * N1 * b * N2 by GROUP_2:10
.= a * (N1 * b) * N2 by GROUP_2:29
.= a * (b * N1) * N2 by GROUP_3:117
.= (a * b) * N1 * N2 by GROUP_2:105
.= (a * b) * (N1 * N2) by GROUP_4:45;
hence thesis by A1;
end;
theorem
for N being normal Subgroup of G for x holds x * N * x" c= carr(N)
proof
let N be normal Subgroup of G;
let x;
x * N c= N * x by GROUP_3:118; then
A1: x * N * x" c= N * x * x" by GROUP_3:5;
N * x * x" = N * (x * x") by GROUP_2:107
.= N * 1_G by GROUP_1:def 5;
hence thesis by A1,GROUP_2:109;
end;
definition
let G be Group, A be Subset of G;
let N be Subgroup of G;
func N ` A -> Subset of G equals
{x where x is Element of G: x * N c= A};
correctness
proof
{x where x is Element of G : x * N c= A} c= the carrier of G
proof
let y be object;
assume y in {x where x is Element of G: x * N c= A};
then ex x being Element of G st y = x & x * N c= A;
hence thesis;
end;
hence thesis;
end;
func N ~ A -> Subset of G equals
{x where x is Element of G : x * N meets A};
correctness
proof
{x where x is Element of G : x * N meets A} c= the carrier of G
proof
let y be object;
assume y in {x where x is Element of G : x * N meets A};
then ex x being Element of G st y = x & x * N meets A;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th12:
for x being Element of G st x in N ` A holds x * N c= A
proof
let x be Element of G;
assume x in N ` A;
then ex x1 being Element of G st x1 = x & x1 * N c= A;
hence thesis;
end;
theorem
for x being Element of G st x * N c= A holds x in N ` A;
theorem Th14:
for x being Element of G st x in N ~ A holds x * N meets A
proof
let x be Element of G;
assume x in N ~ A;
then ex x1 being Element of G st x = x1 & x1 * N meets A;
hence thesis;
end;
theorem
for x being Element of G st x * N meets A holds x in N ~ A;
theorem Th16:
N ` A c= A
proof
let x be object;
assume x in N ` A;
then consider y being Element of G such that
A1: y = x & y * N c= A;
y in y * N by GROUP_2:108;
hence thesis by A1;
end;
theorem Th17:
A c= N ~ A
proof
let x be object;
assume
A1: x in A;
then reconsider x9 = x as Element of G;
x9 in x9 * N by GROUP_2:108;
then x9 * N meets A by A1,XBOOLE_0:3;
hence thesis;
end;
theorem Th18:
N ` A c= N ~ A
proof
A1: N ` A c= A by Th16;
A c= N ~ A by Th17;
hence thesis by A1;
end;
theorem
N ~ (A \/ B) = N ~ A \/ N ~ B
proof
thus N ~ (A \/ B) c= N ~ A \/ N ~ B
proof
let x be object;
assume
A1: x in N ~ (A \/ B);
then reconsider x as Element of G;
x * N meets (A \/ B) by A1,Th14;
then x * N meets A or x * N meets B by XBOOLE_1:70;
then x in N ~ A or x in N ~ B;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume
A2:x in N ~ A \/ N ~ B;
then reconsider x as Element of G;
x in N ~ A or x in N ~ B by A2,XBOOLE_0:def 3;
then
x * N meets A or x * N meets B by Th14;
then x * N meets (A \/ B) by XBOOLE_1:70;
hence thesis;
end;
theorem
N ` (A /\ B) = N ` A /\ N ` B
proof
thus N ` (A /\ B) c= N ` A /\ N ` B
proof
let x be object;
assume
A1: x in N ` (A /\ B);
then reconsider x as Element of G;
consider x1 being Element of G such that
A2: x1 = x & x1 * N c= A /\ B by A1;
x * N c= A & x * N c= B by A2,XBOOLE_1:18;
then x in N ` A & x in N ` B;
hence thesis by XBOOLE_0:def 4;
end;
let x be object;
assume
A3: x in N ` A /\ N ` B;
then reconsider x as Element of G;
x in N ` A & x in N ` B by A3,XBOOLE_0:def 4;
then x * N c= A & x * N c= B by Th12;
then x * N c= A /\ B by XBOOLE_1:19;
hence thesis;
end;
theorem
A c= B implies N ` A c= N ` B
proof
assume
A1: A c= B;
let x be object;
assume
A2: x in N ` A;
then reconsider x as Element of G;
x * N c= A by A2,Th12;
then x * N c= B by A1;
hence thesis;
end;
theorem
A c= B implies N ~ A c= N ~ B
proof
assume
A1: A c= B;
let x be object;
assume
A2: x in N ~ A;
then reconsider x as Element of G;
x * N meets A by A2,Th14;
then x * N meets B by A1,XBOOLE_1:63;
hence thesis;
end;
theorem
N ` A \/ N ` B c= N ` (A \/ B)
proof
let x be object;
assume
A1: x in N ` A \/ N ` B;
then reconsider x as Element of G;
per cases by A1,XBOOLE_0:def 3;
suppose x in N ` A;
then x * N c= A \/ B by Th12,XBOOLE_1:10;
hence thesis;
end;
suppose x in N ` B;
then x * N c= A \/ B by Th12,XBOOLE_1:10;
hence thesis;
end;
end;
theorem
N ~ (A \/ B)= N ~ A \/ N ~ B
proof
thus N ~ (A \/ B) c= N ~ A \/ N ~ B
proof
let x be object;
assume
A1: x in N ~ (A \/ B);
then reconsider x as Element of G;
x * N meets (A \/ B) by A1,Th14;
then x * N meets A or x * N meets B by XBOOLE_1:70;
then x in N ~ A or x in N ~ B;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume
A2: x in N ~ A \/ N ~ B;
then reconsider x as Element of G;
x in N ~ A or x in N ~ B by A2,XBOOLE_0:def 3;
then x * N meets A or x * N meets B by Th14;
then x * N meets (A \/ B) by XBOOLE_1:70;
hence thesis;
end;
theorem Th25:
N is Subgroup of H implies H ` A c= N ` A
proof
assume
A1: N is Subgroup of H;
let x be object;
assume
A2: x in H ` A;
then reconsider x as Element of G;
A3: x * N c= x * H by A1,GROUP_3:6;
x * H c= A by A2,Th12;
then x * N c= A by A3;
hence thesis;
end;
theorem Th26:
N is Subgroup of H implies N ~ A c= H ~ A
proof
assume
A1: N is Subgroup of H;
let x be object;
assume
A2: x in N ~ A;
then reconsider x as Element of G;
x * N meets A by A2,Th14;
then x * H meets A by A1,GROUP_3:6,XBOOLE_1:63;
hence thesis;
end;
theorem
for G be Group, A,B be non empty Subset of G, N be normal Subgroup of G
holds N ` A * N ` B c= N ` (A * B)
proof
let G be Group, A,B be non empty Subset of G,
N be normal Subgroup of G;
let x be object;
assume
A1: x in N ` A * N ` B;
then reconsider x as Element of G;
consider x1, x2 be Element of G such that
A2: x = x1 * x2 & x1 in N ` A & x2 in N ` B by A1;
x1 * N c= A & x2 * N c= B by A2,Th12;
then (x1 * N) * (x2 * N) c= A * B by GROUP_3:4;
then (x1 * x2) * N c= A * B by Th1;
hence thesis by A2;
end;
theorem Th28:
for x being Element of G st x in N ~ (A * B) holds x * N meets A * B
proof
let x be Element of G;
assume x in N ~ (A * B);
then consider x1 being Element of G such that
A1: x = x1 & x1 * N meets A * B;
thus thesis by A1;
end;
theorem
for G be Group, A,B be non empty Subset of G, N be normal Subgroup of G
holds N ~ A * N ~ B = N ~ (A * B)
proof
let G be Group, A,B be non empty Subset of G,
N be normal Subgroup of G;
thus N ~ A * N ~ B c= N ~ (A * B)
proof
let x be object;
assume
A1: x in N ~ A * N ~ B;
then reconsider x as Element of G;
consider x1, x2 be Element of G such that
A2: x = x1 * x2 & x1 in N ~ A & x2 in N ~ B by A1;
A3: x1 * N meets A by A2,Th14;
A4: x2 * N meets B by A2,Th14;
consider x19 be object such that
A5: x19 in x1 * N & x19 in A by A3,XBOOLE_0:3;
consider x29 be object such that
A6: x29 in x2 * N & x29 in B by A4,XBOOLE_0:3;
reconsider x19 as Element of G by A5;
reconsider x29 as Element of G by A6;
A7: x19 * x29 in A * B by A5,A6;
x19 * x29 in (x1 * N) * (x2 * N) by A5,A6;
then (x1 * N) * (x2 * N) meets A * B by A7,XBOOLE_0:3;
then (x1 * x2) * N meets A * B by Th1;
hence thesis by A2;
end;
let x be object;
assume
A8: x in N ~ (A * B);
then reconsider x as Element of G;
x * N meets A * B by A8,Th28;
then consider x1 be object such that
A9: x1 in x * N & x1 in A * B by XBOOLE_0:3;
reconsider x1 as Element of G by A9;
consider y1, y2 be Element of G such that
A10: x1 = y1 * y2 & y1 in A & y2 in B by A9;
x * N = (y1 * y2) * N by A9,A10,Th2
.= (y1 * N) * (y2 * N) by Th1;
then x in (y1 * N) * (y2 * N) by GROUP_2:108;
then consider g1, g2 be Element of G such that
A11: x = g1 * g2 & g1 in y1 * N & g2 in y2 * N;
y1 * N = g1 * N & y2 * N = g2 * N by A11,Th2;
then y1 in g1 * N & y2 in g2 * N by GROUP_2:108;
then g1 * N meets A & g2 * N meets B by A10,XBOOLE_0:3;
then g1 in N ~ A & g2 in N ~ B;
hence thesis by A11;
end;
theorem Th30:
for x being Element of G st x in N ~ (N ` (N ~ A))
holds x * N meets N ` (N ~ A)
proof
let x be Element of G;
assume x in N ~ (N ` (N ~ A));
then ex x1 being Element of G st x = x1 & x1 * N meets N ` (N ~ A);
hence thesis;
end;
theorem Th31:
for x being Element of G st x in N ` (N ~ A) holds x * N c= N ~ A
proof
let x be Element of G;
assume x in N ` (N ~ A);
then ex x1 being Element of G st x1 = x & x1 * N c= N ~ A;
hence thesis;
end;
theorem Th32:
for x being Element of G st x in N ~ (N ~ A) holds x * N meets N ~ A
proof
let x be Element of G;
assume x in N ~ (N ~ A);
then ex x1 being Element of G st x = x1 & x1 * N meets N ~ A;
hence thesis;
end;
theorem Th33:
for x being Element of G st x in N ~ (N ` A) holds x * N meets N ` A
proof
let x be Element of G;
assume x in N ~ (N ` A);
then ex x1 being Element of G st x = x1 & x1 * N meets N ` A;
hence thesis;
end;
theorem Th34:
N ` (N ` A) = N ` A
proof
thus N ` (N ` A) c= N ` A
proof
let x be object;
assume x in N ` (N ` A);
then consider y being Element of G such that
A1: y = x & y * N c= N ` A;
y in y * N by GROUP_2:108;
hence thesis by A1;
end;
let x be object;
assume
A2: x in N ` A;
then reconsider x9 = x as Element of G;
A3: x9 * N c= A by A2,Th12;
x9 * N c= N ` A
proof
let y be object;
assume
A4: y in x9 * N;
then reconsider y9 = y as Element of G;
x9 * N = y9 * N by A4,Th2;
hence thesis by A3;
end;
hence thesis;
end;
theorem Th35:
N ~ A = N ~ (N ~ A)
proof
thus N ~ A c= N ~ (N ~ A)
proof
let x be object;
assume
A1: x in N ~ A;
then reconsider x as Element of G;
x in x * N by GROUP_2:108;
then x * N meets N ~ A by A1,XBOOLE_0:3;
hence thesis;
end;
let x be object;
assume
A2:x in N ~ (N ~ A);
then reconsider x9 = x as Element of G;
x9 * N meets N ~ A by A2,Th32;
then consider y be object such that
A3:y in x9 * N & y in N ~ A by XBOOLE_0:3;
reconsider y9 = y as Element of G by A3;
A4:y9 * N meets A by A3,Th14;
y9 * N = x9 * N by A3,Th2;
hence thesis by A4;
end;
theorem
N ` (N ` A) c= N ~ (N ~ A)
proof
N ` A c= N ~ A by Th18;
then N ` (N ` A) c= N ~ A by Th34;
hence thesis by Th35;
end;
theorem
N ~ (N ` A) c= A
proof
let x be object;
assume
A1:x in N ~ (N ` A);
then reconsider x9 = x as Element of G;
x9 * N meets N ` A by A1,Th33;
then consider y being object such that
A2:y in x9 * N & y in N ` A by XBOOLE_0:3;
reconsider y9 = y as Element of G by A2;
y9 * N c= A by A2,Th12; then
A3:x9 * N c= A by A2,Th2;
x9 in x9 * N by GROUP_2:108;
hence thesis by A3;
end;
theorem
N ` (N ~ (N ` A)) = N ` A
proof
thus N ` (N ~ (N ` A)) c= N ` A
proof
let x be object;
assume x in N ` (N ~ (N ` A));
then consider x1 being Element of G such that
A1: x1 = x & x1 * N c= N ~ (N ` A);
x1 in x1 * N by GROUP_2:108;
then x1 * N meets N ` A by A1,Th33;
then consider y be object such that
A2: y in x1 * N & y in N ` A by XBOOLE_0:3;
reconsider y as Element of G by A2;
y * N c= A by A2,Th12;
then x1 * N c= A by A2,Th2;
hence thesis by A1;
end;
let x be object;
assume
A3: x in N ` A;
then reconsider x as Element of G;
x * N c= N ~ (N ` A)
proof
let y be object;
assume
A4: y in x * N;
then reconsider y as Element of G;
y * N = x * N by A4,Th2;
then x in y * N by GROUP_2:108;
then y * N meets N ` A by A3,XBOOLE_0:3;
hence thesis;
end;
hence thesis;
end;
theorem Th39:
A c= N ` (N ~ A) implies N ~ A c= N ~ (N `(N ~ A))
proof
assume
A1: A c= N ` (N ~ A);
let x be object;
assume
A2: x in N ~ A;
then reconsider x as Element of G;
x * N meets A by A2,Th14;
then x * N meets N ` (N ~ A) by A1,XBOOLE_1:63;
hence thesis;
end;
theorem
N ~ (N `(N ~ A)) = N ~ A
proof
thus N ~ (N `(N ~ A)) c= N ~ A
proof
let x be object;
assume
A1: x in N ~ (N ` (N ~ A));
then reconsider x as Element of G;
x * N meets N ` (N ~ A) by A1,Th30;
then consider y being object such that
A2: y in x * N & y in N ` (N ~ A) by XBOOLE_0:3;
reconsider y as Element of G by A2;
y * N c= N ~ A by A2,Th31;
then
A3: x * N c= N ~ A by A2,Th2;
x in x * N by GROUP_2:108;
hence thesis by A3;
end;
thus N ~ A c= N ~ (N `(N ~ A))
proof
A c= N ` (N ~ A)
proof
let x be object;
assume
A4: x in A;
then reconsider x as Element of G;
x * N c= N ~ A
proof
let y be object;
assume
A5: y in x * N;
then reconsider y as Element of G;
y * N = x * N by A5,Th2;
then x in y * N by GROUP_2:108;
then y * N meets A by A4,XBOOLE_0:3;
hence thesis;
end;
hence thesis;
end;
hence thesis by Th39;
end;
end;
theorem Th41:
for x being Element of G st x in N ` (N ` A) holds x * N c= N ` A
proof
let x be Element of G;
assume x in N ` (N ` A);
then ex x1 being Element of G st x1 = x & x1 * N c= N ` A;
hence thesis;
end;
theorem
N `(N ` A) = N ~ (N ` A)
proof
thus N `(N ` A) c= N ~ (N ` A)
proof
let x be object;
assume
A1: x in N `(N ` A);
then reconsider x as Element of G;
A2: x * N c= N ` A by A1,Th41;
x in x * N by GROUP_2:108;
then x * N meets N ` A by A2,XBOOLE_0:3;
hence thesis;
end;
let x be object;
assume
A3:x in N ~ (N ` A);
then reconsider x as Element of G;
x * N meets N ` A by A3,Th33;
then consider z being object such that
A4:z in x * N & z in N ` A by XBOOLE_0:3;
reconsider z as Element of G by A4;
z * N c= A by A4,Th12;
then
A5: x * N c= A by A4,Th2;
x * N c= N ` A
proof
let y be object;
assume
A6: y in x * N;
then reconsider y as Element of G;
x * N = y * N by A6,Th2;
hence thesis by A5;
end;
hence thesis;
end;
theorem
N ~ (N ~ A) = N `(N ~ A)
proof
thus N ~ (N ~ A) c= N `(N ~ A)
proof
let x be object;
assume
A1: x in N ~ (N ~ A);
then reconsider x as Element of G;
x * N meets N ~ A by A1,Th32;
then consider z being object such that
A2: z in x * N & z in N ~ A by XBOOLE_0:3;
reconsider z as Element of G by A2;
z * N meets A by A2,Th14;
then
A3: x * N meets A by A2,Th2;
x * N c= N ~ A
proof
let y be object;
assume
A4: y in x * N;
then reconsider y as Element of G;
x * N = y * N by A4,Th2;
hence thesis by A3;
end;
hence thesis;
end;
let x be object;
assume
A5: x in N ` (N ~ A);
then reconsider x as Element of G;
A6: x * N c= N ~ A by A5,Th31;
x in x * N by GROUP_2:108;
then x * N meets N ~ A by A6,XBOOLE_0:3;
hence thesis;
end;
theorem
for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N ~ A c= N1 ~ A /\ N2 ~ A
proof
let N, N1,N2 be Subgroup of G;
assume N = N1 /\ N2; then
A1:N is Subgroup of N1 & N is Subgroup of N2 by GROUP_2:88;
let x be object;
assume
A2: x in N ~ A;
N ~ A c= N1 ~ A & N ~ A c= N2 ~ A by A1,Th26;
hence thesis by A2,XBOOLE_0:def 4;
end;
theorem
for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N1 ` A /\ N2 ` A c= N ` A
proof
let N,N1,N2 be Subgroup of G;
assume N = N1 /\ N2; then
A1:N is Subgroup of N1 & N is Subgroup of N2 by GROUP_2:88;
let x be object;
assume x in N1 ` A /\ N2 ` A; then
A2: x in N1 ` A & x in N2 ` A by XBOOLE_0:def 4;
N1 ` A c= N ` A & N2 ` A c= N ` A by A1,Th25;
hence thesis by A2;
end;
theorem
for N1,N2 be strict normal Subgroup of G
ex N being strict normal Subgroup of G
st the carrier of N = N1 * N2 & N ` A c= N1 ` A /\ N2 ` A
proof
let N1,N2 be strict normal Subgroup of G;
consider N be strict normal Subgroup of G such that
A1:the carrier of N = N1 * N2 by Th8;
N1 is Subgroup of N & N2 is Subgroup of N by A1,Th9; then
A2: N ` A c= N1 ` A & N ` A c= N2 ` A by Th25;
N ` A c= N1 ` A /\ N2 ` A
by A2,XBOOLE_0:def 4;
hence thesis by A1;
end;
theorem
for N1,N2 be strict normal Subgroup of G ex N being strict normal
Subgroup of G st the carrier of N = N1 * N2 & N1 ~ A \/ N2 ~ A c= N ~ A
proof
let N1,N2 be strict normal Subgroup of G;
consider N be strict normal Subgroup of G such that
A1:the carrier of N = N1 * N2 by Th8;
N1 is Subgroup of N & N2 is Subgroup of N by A1,Th9; then
A2: N1 ~ A c= N ~ A & N2 ~ A c= N ~ A by Th26;
N1 ~ A \/ N2 ~ A c= N ~ A
proof
let x be object;
assume x in N1 ~ A \/ N2 ~ A;
then x in N1 ~ A or x in N2 ~ A by XBOOLE_0:def 3;
hence thesis by A2;
end;
hence thesis by A1;
end;
theorem
for N1,N2 be strict normal Subgroup of G
ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 &
N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1)
proof
let N1,N2 be strict normal Subgroup of G;
consider N be strict normal Subgroup of G such that
A1:the carrier of N = N1 * N2 by Th8;
N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1)
proof
let x be object;
assume
A2: x in N ~ A;
then reconsider x as Element of G;
x * N meets A by A2,Th14;
then consider x1 be object such that
A3: x1 in x * N & x1 in A by XBOOLE_0:3;
reconsider x1 as Element of G by A3;
consider y be Element of G such that
A4: x1 = x * y & y in N by A3,GROUP_2:103;
A5: y in N1 * N2 by A1,A4,STRUCT_0:def 5;
then consider a,b be Element of G such that
A6: y = a * b & a in N1 & b in N2 by Th6;
A7: x1 = x * a * b by A4,A6,GROUP_1:def 3;
a in carr(N1) by A6,STRUCT_0:def 5;
then
A8: x * a * b in x * N1 * b by GROUP_8:15;
x * N1 * b = x * (N1 * b) by GROUP_2:106
.= x * (b * N1) by GROUP_3:117
.= (x * b) * N1 by GROUP_2:105;
then (x * b) * N1 meets A by A3,A7,A8,XBOOLE_0:3;
then
A9: x * b in N1 ~ A;
A10:(x * b) * b" = x * (b * b") by GROUP_1:def 3
.= x * 1_G by GROUP_1:def 5
.= x by GROUP_1:def 4;
b" in N2 by A6,GROUP_2:51;
then
A11:x in (N1 ~ A) * N2 by A9,A10,GROUP_2:94;
y in N2 * N1 by A5,GROUP_3:125;
then consider a,b be Element of G such that
A12: y = a * b & a in N2 & b in N1 by Th6;
A13: x1 = x * a * b by A4,A12,GROUP_1:def 3;
a in carr(N2) by A12,STRUCT_0:def 5;
then
A14: x * a * b in x * N2 * b by GROUP_8:15;
x * N2 * b = x * (N2 * b) by GROUP_2:106
.= x * (b * N2) by GROUP_3:117
.= (x * b) * N2 by GROUP_2:105;
then (x * b) * N2 meets A by A3,A13,A14,XBOOLE_0:3;
then
A15: x * b in N2 ~ A;
A16:(x * b) * b" = x * (b * b") by GROUP_1:def 3
.= x * 1_G by GROUP_1:def 5
.= x by GROUP_1:def 4;
b" in N1 by A12,GROUP_2:51;
then x in (N2 ~ A) * N1 by A15,A16,GROUP_2:94;
hence thesis by A11,XBOOLE_0:def 4;
end;
hence thesis by A1;
end;
reserve N1,N2 for Subgroup of G;
definition
let G be Group, H, N be Subgroup of G;
func N ` H -> Subset of G equals
{x where x is Element of G: x * N c= carr(H)};
coherence
proof
{x where x is Element of G : x * N c= carr(H)} c= the carrier of G
proof
let y be object;
assume y in {x where x is Element of G : x * N c= carr(H)};
then ex x being Element of G st y = x & x * N c= carr(H);
hence thesis;
end;
hence thesis;
end;
func N ~ H -> Subset of G equals
{x where x is Element of G : x * N meets carr(H)};
coherence
proof
{x where x is Element of G : x * N meets carr(H)} c= the carrier of G
proof
let y be object;
assume y in {x where x is Element of G : x * N meets carr(H)};
then ex x being Element of G st y = x & x * N meets carr(H);
hence thesis;
end;
hence thesis;
end;
end;
theorem Th49:
for x being Element of G st x in N ` H holds x * N c= carr(H)
proof
let x be Element of G;
assume x in N ` H;
then ex x1 being Element of G st x1 = x & x1 * N c= carr(H);
hence thesis;
end;
theorem
for x being Element of G st x * N c= carr(H) holds x in N ` H;
theorem Th51:
for x being Element of G st x in N ~ H holds x * N meets carr(H)
proof
let x be Element of G;
assume x in N ~ H;
then ex x1 being Element of G st x = x1 & x1 * N meets carr(H);
hence thesis;
end;
theorem
for x being Element of G st x * N meets carr(H) holds x in N ~ H;
theorem Th53:
N ` H c= carr(H)
proof
let x be object;
assume x in N ` H;
then consider y1 being Element of G such that
A1: y1 = x & y1 * N c= carr(H);
y1 in y1 * N by GROUP_2:108;
hence thesis by A1;
end;
theorem Th54:
carr(H) c= N ~ H
proof
let x be object;
assume x in carr(H);
then reconsider x as Element of H;
reconsider x as Element of G by GROUP_2:42;
x in x * N by GROUP_2:108;
then x * N meets carr(H) by XBOOLE_0:3;
hence thesis;
end;
theorem Th55:
N ` H c= N ~ H
proof
A1: N ` H c= carr(H) by Th53;
carr(H) c= N ~ H by Th54;
hence thesis by A1;
end;
theorem Th56:
H1 is Subgroup of H2 implies N ~ H1 c= N ~ H2
proof
assume H1 is Subgroup of H2; then
A1: carr(H1) c= carr(H2) by GROUP_2:def 5;
let x be object;
assume
A2: x in N ~ H1;
then reconsider x as Element of G;
x * N meets carr(H1) by A2,Th51;
then x * N meets carr(H2) by A1,XBOOLE_1:63;
hence thesis;
end;
theorem Th57:
N1 is Subgroup of N2 implies N1 ~ H c= N2 ~ H
proof
assume
A1:N1 is Subgroup of N2;
let x be object;
assume
A2: x in N1 ~ H;
then reconsider x as Element of G;
x * N1 meets carr(H) by A2,Th51;
then x * N2 meets carr(H) by A1,GROUP_3:6,XBOOLE_1:63;
hence thesis;
end;
theorem
N1 is Subgroup of N2 implies N1 ~ N1 c= N2 ~ N2
proof
assume
A1: N1 is Subgroup of N2; then
A2: N2 ~ N1 c= N2 ~ N2 by Th56;
N1 ~ N1 c= N2 ~ N1 by A1,Th57;
hence thesis by A2;
end;
theorem Th59:
H1 is Subgroup of H2 implies N ` H1 c= N ` H2
proof
assume H1 is Subgroup of H2; then
A1: carr(H1) c= carr(H2) by GROUP_2:def 5;
let x be object;
assume
A2: x in N ` H1;
then reconsider x as Element of G;
x * N c= carr(H1) by A2,Th49;
then x * N c= carr(H2) by A1;
hence thesis;
end;
theorem Th60:
N1 is Subgroup of N2 implies N2 ` H c= N1 ` H
proof
assume
A1: N1 is Subgroup of N2;
let x be object;
assume
A2: x in N2 ` H;
then reconsider x as Element of G;
A3: x * N1 c= x * N2 by A1,GROUP_3:6;
x * N2 c= carr(H) by A2,Th49;
then x * N1 c= carr(H) by A3;
hence thesis;
end;
theorem
N1 is Subgroup of N2 implies N2 ` N1 c= N1 ` N2
proof
assume
A1: N1 is Subgroup of N2; then
A2: N2 ` N1 c= N2 ` N2 by Th59;
N2 ` N2 c= N1 ` N2 by A1,Th60;
hence thesis by A2;
end;
theorem
for N be normal Subgroup of G holds N ` H1 * N ` H2 c= N ` (H1 * H2)
proof
let N be normal Subgroup of G;
let x be object;
assume
A1: x in N ` H1 * N ` H2;
then reconsider x as Element of G;
consider x1, x2 be Element of G such that
A2: x = x1 * x2 & x1 in N ` H1 & x2 in N ` H2 by A1;
x1 * N c= carr(H1) & x2 * N c= carr(H2) by A2,Th49;
then (x1 * N) * (x2 * N) c= carr(H1) * carr(H2) by GROUP_3:4;
then (x1 * x2) * N c= carr(H1) * carr(H2) by Th1;
hence thesis by A2;
end;
theorem
for N be normal Subgroup of G holds N ~ H1 * N ~ H2 = N ~ (H1 * H2)
proof
let N be normal Subgroup of G;
thus N ~ H1 * N ~ H2 c= N ~ (H1 * H2)
proof
let x be object;
assume
A1: x in N ~ H1 * N ~ H2;
then reconsider x as Element of G;
consider x1, x2 be Element of G such that
A2: x = x1 * x2 & x1 in N ~ H1 & x2 in N ~ H2 by A1;
A3: x1 * N meets carr(H1) by A2,Th51;
A4: x2 * N meets carr(H2) by A2,Th51;
consider x19 be object such that
A5: x19 in x1 * N & x19 in carr(H1) by A3,XBOOLE_0:3;
consider x29 be object such that
A6: x29 in x2 * N & x29 in carr(H2) by A4,XBOOLE_0:3;
reconsider x19 as Element of G by A5;
reconsider x29 as Element of G by A6;
A7: x19 * x29 in carr(H1) * carr(H2) by A5,A6;
x19 * x29 in (x1 * N) * (x2 * N) by A5,A6;
then (x1 * N) * (x2 * N) meets carr(H1) * carr(H2) by A7,XBOOLE_0:3;
then (x1 * x2) * N meets carr(H1) * carr(H2) by Th1;
hence thesis by A2;
end;
let x be object;
assume
A8: x in N ~ (H1 * H2);
then reconsider x as Element of G;
x * N meets carr(H1) * carr(H2) by A8,Th28;
then consider x1 be object such that
A9: x1 in x * N & x1 in carr(H1) * carr(H2) by XBOOLE_0:3;
reconsider x1 as Element of G by A9;
consider y1, y2 be Element of G such that
A10: x1 = y1 * y2 & y1 in carr(H1) & y2 in carr(H2) by A9;
x * N = (y1 * y2) * N by A9,A10,Th2
.= (y1 * N) * (y2 * N) by Th1;
then x in (y1 * N) * (y2 * N) by GROUP_2:108;
then consider g1, g2 be Element of G such that
A11: x = g1 * g2 & g1 in y1 * N & g2 in y2 * N;
y1 * N = g1 * N & y2 * N = g2 * N by A11,Th2;
then y1 in g1 * N & y2 in g2 * N by GROUP_2:108;
then g1 * N meets carr(H1) & g2 * N meets carr(H2) by A10,XBOOLE_0:3;
then g1 in N ~ H1 & g2 in N ~ H2;
hence thesis by A11;
end;
theorem
for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N ~ H c= N1 ~ H /\ N2 ~ H
proof
let N,N1,N2 be Subgroup of G;
assume N = N1 /\ N2; then
A1:N is Subgroup of N1 & N is Subgroup of N2 by GROUP_2:88;
let x be object;
assume
A2: x in N ~ H;
N ~ H c= N1 ~ H & N ~ H c= N2 ~ H by A1,Th57;
hence thesis by A2,XBOOLE_0:def 4;
end;
theorem
for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N1 ` H /\ N2 ` H c= N ` H
proof
let N,N1,N2 be Subgroup of G;
assume N = N1 /\ N2; then
A1:N is Subgroup of N1 & N is Subgroup of N2 by GROUP_2:88;
let x be object;
assume x in N1 ` H /\ N2 ` H; then
A2: x in N1 ` H & x in N2 ` H by XBOOLE_0:def 4;
N1 ` H c= N ` H & N2 ` H c= N ` H by A1,Th60;
hence thesis by A2;
end;
theorem
for N1,N2 be strict normal Subgroup of G holds ex N being strict normal
Subgroup of G st the carrier of N = N1 * N2 & N ` H c= N1 ` H /\ N2 ` H
proof
let N1,N2 be strict normal Subgroup of G;
consider N be strict normal Subgroup of G such that
A1:the carrier of N = N1 * N2 by Th8;
N1 is Subgroup of N & N2 is Subgroup of N by A1,Th9; then
A2: N ` H c= N1 ` H & N ` H c= N2 ` H by Th60;
N ` H c= N1 ` H /\ N2 ` H
by A2,XBOOLE_0:def 4;
hence thesis by A1;
end;
theorem
for N1,N2 be strict normal Subgroup of G ex N being strict normal
Subgroup of G st the carrier of N = N1 * N2 & N1 ~ H \/ N2 ~ H c= N ~ H
proof
let N1,N2 be strict normal Subgroup of G;
consider N be strict normal Subgroup of G such that
A1:the carrier of N = N1 * N2 by Th8;
N1 is Subgroup of N & N2 is Subgroup of N by A1,Th9; then
A2: N1 ~ H c= N ~ H & N2 ~ H c= N ~ H by Th57;
N1 ~ H \/ N2 ~ H c= N ~ H
proof
let x be object;
assume x in N1 ~ H \/ N2 ~ H;
then x in N1 ~ H or x in N2 ~ H by XBOOLE_0:def 3;
hence thesis by A2;
end;
hence thesis by A1;
end;
theorem
for N1,N2 be strict normal Subgroup of G
ex N being strict normal Subgroup of G st
the carrier of N = N1 * N2 & N1 ` H * N2 ` H c= N ` H
proof
let N1,N2 be strict normal Subgroup of G;
consider N be strict normal Subgroup of G such that
A1:the carrier of N = N1 * N2 by Th8;
N1 ` H * N2 ` H c= N ` H
proof
let x be object;
assume
A2: x in N1 ` H * N2 ` H;
then reconsider x as Element of G;
consider a,b be Element of G such that
A3: x = a * b & a in N1 ` H & b in N2 ` H by A2;
a * N1 c= carr(H) & b * N2 c= carr(H) by A3,Th49;
then (a * N1) * (b * N2) c= carr(H) * carr(H) by GROUP_3:4; then
A4: (a * N1) * (b * N2) c= carr(H) by GROUP_2:76;
(a * N1) * (b * N2) = (a * b) * N by A1,Th10;
hence thesis by A3,A4;
end;
hence thesis by A1;
end;
theorem
for N1,N2 be strict normal Subgroup of G
ex N being strict normal Subgroup of G st
the carrier of N = N1 * N2 & N1 ~ H * N2 ~ H c= N ~ H
proof
let N1,N2 be strict normal Subgroup of G;
consider N be strict normal Subgroup of G such that
A1:the carrier of N = N1 * N2 by Th8;
N1 ~ H * N2 ~ H c= N ~ H
proof
let x be object;
assume
A2: x in N1 ~ H * N2 ~ H;
then reconsider x as Element of G;
consider a,b be Element of G such that
A3: x = a * b & a in N1 ~ H & b in N2 ~ H by A2;
A4: a * N1 meets carr(H) by A3,Th51;
A5: b * N2 meets carr(H) by A3,Th51;
consider x1 be object such that
A6: x1 in a * N1 & x1 in carr(H) by A4,XBOOLE_0:3;
consider x2 be object such that
A7: x2 in b * N2 & x2 in carr(H) by A5,XBOOLE_0:3;
reconsider x1 as Element of G by A6;
reconsider x2 as Element of G by A7;
A8: x1 * x2 in carr(H) * carr(H) by A6,A7;
A9: x1 * x2 in (a * N1) * (b * N2) by A6,A7;
carr(H) * carr(H) = carr(H) by GROUP_2:76; then
A10:(a * N1) * (b * N2) meets carr(H) by A8,A9,XBOOLE_0:3;
(a * N1) * (b * N2) = (a * b) * N by A1,Th10;
hence thesis by A3,A10;
end;
hence thesis by A1;
end;
theorem
for N1,N2 be strict normal Subgroup of G
ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 &
N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1)
proof
let N1,N2 be strict normal Subgroup of G;
consider N be strict normal Subgroup of G such that
A1:the carrier of N = N1 * N2 by Th8;
N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1)
proof
let x be object;
assume
A2: x in N ~ H;
then reconsider x as Element of G;
x * N meets carr(H) by A2,Th51;
then consider x1 be object such that
A3: x1 in x * N & x1 in carr(H) by XBOOLE_0:3;
reconsider x1 as Element of G by A3;
consider y be Element of G such that
A4: x1 = x * y & y in N by A3,GROUP_2:103;
A5: y in N1 * N2 by A1,A4,STRUCT_0:def 5;
then consider a,b be Element of G such that
A6: y = a * b & a in N1 & b in N2 by Th6;
A7: x1 = x * a * b by A4,A6,GROUP_1:def 3;
a in carr(N1) by A6,STRUCT_0:def 5; then
A8: x * a * b in x * N1 * b by GROUP_8:15;
x * N1 * b = x * (N1 * b) by GROUP_2:106
.= x * (b * N1) by GROUP_3:117
.= (x * b) * N1 by GROUP_2:105;
then (x * b) * N1 meets carr(H) by A3,A7,A8,XBOOLE_0:3;
then
A9: x * b in N1 ~ H;
A10:(x * b) * b" = x * (b * b") by GROUP_1:def 3
.= x * 1_G by GROUP_1:def 5
.= x by GROUP_1:def 4;
b" in N2 by A6,GROUP_2:51; then
A11:x in (N1 ~ H) * N2 by A9,A10,GROUP_2:94;
y in N2 * N1 by A5,GROUP_3:125;
then consider a,b be Element of G such that
A12: y = a * b & a in N2 & b in N1 by Th6;
A13: x1 = x * a * b by A4,A12,GROUP_1:def 3;
a in carr(N2) by A12,STRUCT_0:def 5; then
A14: x * a * b in x * N2 * b by GROUP_8:15;
x * N2 * b = x * (N2 * b) by GROUP_2:106
.= x * (b * N2) by GROUP_3:117
.= (x * b) * N2 by GROUP_2:105;
then (x * b) * N2 meets carr(H) by A3,A13,A14,XBOOLE_0:3;
then
A15: x * b in N2 ~ H;
A16:(x * b) * b" = x * (b * b") by GROUP_1:def 3
.= x * 1_G by GROUP_1:def 5
.= x by GROUP_1:def 4;
b" in N1 by A12,GROUP_2:51;
then x in (N2 ~ H) * N1 by A15,A16,GROUP_2:94;
hence thesis by A11,XBOOLE_0:def 4;
end;
hence thesis by A1;
end;
theorem Th71:
for H being Subgroup of G, N being normal Subgroup of G
ex M being strict Subgroup of G st the carrier of M = N ~ H
proof
let H be Subgroup of G, N be normal Subgroup of G;
A1:1_G in N ~ H
proof
1_G in H by GROUP_2:46; then
A2: 1_G in carr(H) by STRUCT_0:def 5;
1_G in 1_G * N by GROUP_2:108;
then 1_G * N meets carr(H) by A2,XBOOLE_0:3;
hence thesis;
end;
A3:for x,y being Element of G holds x in N ~ H & y in N ~ H
implies x * y in N ~ H
proof
let x,y be Element of G;
assume that
A4: x in N ~ H and
A5: y in N ~ H;
consider a be Element of G such that
A6: a in x * N & a in H by A4,Th51,Th3;
consider b be Element of G such that
A7: b in y * N & b in H by A5,Th51,Th3;
(x * N) * (y * N) = (x * y) * N & (a * N) * (b * N) = (a * b) * N by Th1;
then
A8: a * b in (x * y) * N by A6,A7;
a * b in H by A6,A7,GROUP_2:50;
then a * b in carr(H) by STRUCT_0:def 5;
then (x * y) * N meets carr(H) by A8,XBOOLE_0:3;
hence thesis;
end;
for x being Element of G holds x in N ~ H implies x" in N ~ H
proof
let x be Element of G;
assume x in N ~ H;
then consider a be Element of G such that
A9:a in x * N & a in H by Th3,Th51;
consider a1 be Element of G such that
A10:a = x * a1 & a1 in N by A9,GROUP_2:103;
A11:a1" in N by A10,GROUP_2:51;
a" = a1" * x" by A10,GROUP_1:17;
then a" in N * x" by A11,GROUP_2:104; then
A12:a" in x" * N by GROUP_3:117;
a" in H by A9,GROUP_2:51;
then a" in carr(H) by STRUCT_0:def 5;
then x" * N meets carr(H) by A12,XBOOLE_0:3;
hence thesis;
end;
hence thesis by A1,A3,GROUP_2:52;
end;
theorem Th72:
for H being Subgroup of G, N being normal Subgroup of G st N is Subgroup of H
ex M being strict Subgroup of G st the carrier of M = N ` H
proof
let H be Subgroup of G, N be normal Subgroup of G;
assume
A1: N is Subgroup of H;
A2: 1_G in N ` H
proof
1_G in N by GROUP_2:46; then
A3: 1_G * N = carr(N) by GROUP_2:113;
carr(N) c= carr(H) by A1,GROUP_2:def 5;
hence thesis by A3;
end;
A4:for x,y being Element of G holds x in N ` H & y in N ` H
implies x * y in N ` H
proof
let x,y be Element of G;
assume x in N ` H & y in N ` H;
then x * N c= carr(H) & y * N c= carr(H) by Th49; then
A5: (x * N) * (y * N) c= carr(H) * carr(H) by GROUP_3:4;
A6: (x * N) * (y * N) = (x * y) * N by Th1;
carr(H) * carr(H) = carr(H) by GROUP_2:76;
hence thesis by A5,A6;
end;
for x being Element of G holds x in N ` H implies x" in N ` H
proof
let x be Element of G;
assume x in N ` H; then
A7: x * N c= carr(H) by Th49;
x in x * N by GROUP_2:108;
then x in H by A7,STRUCT_0:def 5; then
x" in H by GROUP_2:51;
then A8: x" * H = carr(H) by GROUP_2:113;
x" * N c= x" * H by A1,GROUP_3:6;
hence thesis by A8;
end;
hence thesis by A2,A4,GROUP_2:52;
end;
theorem Th73:
for H,N be normal Subgroup of G
ex M being strict normal Subgroup of G st the carrier of M = N ~ H
proof
let H,N be normal Subgroup of G;
consider M being strict Subgroup of G such that
A1: the carrier of M = N ~ H by Th71;
for x be Element of G holds x * M c= M * x
proof
let x be Element of G;
let y be object;
assume
A2: y in x * M;
then reconsider y as Element of G;
consider z be Element of G such that
A3: y = x * z & z in M by A2,GROUP_2:103;
z in the carrier of M by A3,STRUCT_0:def 5;
then consider z9 be Element of G such that
A4: z9 in z * N & z9 in H by Th3,A1,Th51;
x * z9 * x" in H by A4,Th4;
then
A5: x * z9 * x" in carr(H) by STRUCT_0:def 5;
A6: x * z9 * x" in x * (z * N) * x" by A4,GROUP_8:15;
x * (z * N) * x" = x * ((z * N) * x") by GROUP_2:33
.= x * (z * (N * x")) by GROUP_2:33
.= x * (z * (x" * N)) by GROUP_3:117
.= x * (z * x" * N) by GROUP_2:32
.= x * (z * x") * N by GROUP_2:32
.= (x * z * x") * N by GROUP_1:def 3;
then (x * z * x") * N meets carr(H) by A5,A6,XBOOLE_0:3;
then x * z * x" in N ~ H;
then
A7: x * z * x" in M by A1,STRUCT_0:def 5;
(x * z * x") * x = y by A3,GROUP_3:1;
hence thesis by A7,GROUP_2:104;
end;
then M is normal Subgroup of G by GROUP_3:118;
hence thesis by A1;
end;
theorem Th74:
for H,N being normal Subgroup of G st N is Subgroup of H
ex M being strict normal Subgroup of G st the carrier of M = N ` H
proof
let H,N be normal Subgroup of G;
assume
A1: N is Subgroup of H;
then consider M being strict Subgroup of G such that
A2: the carrier of M = N ` H by Th72;
for x be Element of G holds x * M c= M * x
proof
let x be Element of G;
let y be object;
assume
A3: y in x * M;
then reconsider y as Element of G;
consider z be Element of G such that
A4: y = x * z & z in M by A3,GROUP_2:103;
z in the carrier of M by A4,STRUCT_0:def 5;
then
A5: z * N c= carr(H) by A2,Th49;
z in z * N by GROUP_2:108;
then z in H by A5,STRUCT_0:def 5;
then x * z * x" in H by Th4;
then
A6: (x * z * x") * H = carr(H) by GROUP_2:113;
(x * z * x") * N c= (x * z * x") * H by A1,GROUP_3:6;
then x * z * x" in N ` H by A6; then
A7: x * z * x" in M by A2,STRUCT_0:def 5;
(x * z * x") * x = y by A4,GROUP_3:1;
hence thesis by A7,GROUP_2:104;
end;
then M is normal Subgroup of G by GROUP_3:118;
hence thesis by A2;
end;
theorem Th75:
for N,N1 be normal Subgroup of G st N1 is Subgroup of N
ex N2,N3 being strict normal Subgroup of G st
the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N &
N2 ` N c= N3 ` N
proof
let N,N1 be normal Subgroup of G;
assume
A1:N1 is Subgroup of N;
consider N2 be strict normal Subgroup of G such that
A2:the carrier of N2 = N1 ~ N by Th73;
consider N3 be strict normal Subgroup of G such that
A3:the carrier of N3 = N1 ` N by A1,Th74;
N3 is Subgroup of N2 by A2,A3,Th55,GROUP_2:57;
then N2 ` N c= N3 ` N by Th60;
hence thesis by A2,A3;
end;
theorem Th76:
for N,N1 be normal Subgroup of G st N1 is Subgroup of N
ex N2,N3 being strict normal Subgroup of G st
the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N &
N3 ~ N c= N2 ~ N
proof
let N,N1 be normal Subgroup of G;
assume
A1:N1 is Subgroup of N;
consider N2 be strict normal Subgroup of G such that
A2:the carrier of N2 = N1 ~ N by Th73;
consider N3 be strict normal Subgroup of G such that
A3:the carrier of N3 = N1 ` N by A1,Th74;
N3 is Subgroup of N2 by A2,A3,Th55,GROUP_2:57;
then N3 ~ N c= N2 ~ N by Th57;
hence thesis by A2,A3;
end;
theorem
for N,N1 be normal Subgroup of G st N1 is Subgroup of N
ex N2,N3 being strict normal Subgroup of G
st the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N &
N2 ` N c= N3 ~ N
proof
let N,N1 be normal Subgroup of G;
assume N1 is Subgroup of N;
then consider N2,N3 be strict normal Subgroup of G such that
A1:the carrier of N2 = N1 ~ N and
A2:the carrier of N3 = N1 ` N and
A3: N2 ` N c= N3 ` N by Th75;
N3 ` N c= N3 ~ N by Th55;
hence thesis by A1,A2,A3,XBOOLE_1:1;
end;
theorem
for N,N1 be normal Subgroup of G st N1 is Subgroup of N
ex N2,N3 being strict normal Subgroup of G st
the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N &
N3 ` N c= N2 ~ N
proof
let N,N1 be normal Subgroup of G;
assume N1 is Subgroup of N;
then consider N2,N3 be strict normal Subgroup of G such that
A1:the carrier of N2 = N1 ~ N and
A2:the carrier of N3 = N1 ` N and
A3: N3 ~ N c= N2 ~ N by Th76;
N3 ` N c= N3 ~ N by Th55;
hence thesis by A1,A2,A3,XBOOLE_1:1;
end;
theorem
for N,N1,N2 be normal Subgroup of G st N1 is Subgroup of N2
ex N3,N4 being strict normal Subgroup of G st
the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 &
N3 ~ N1 c= N4 ~ N1
proof
let N,N1,N2 be normal Subgroup of G;
assume
A1:N1 is Subgroup of N2;
consider N3 be strict normal Subgroup of G such that
A2:the carrier of N3 = N ~ N1 by Th73;
consider N4 be strict normal Subgroup of G such that
A3:the carrier of N4 = N ~ N2 by Th73;
N3 is Subgroup of N4 by A1,A2,A3,Th56,GROUP_2:57;
then N3 ~ N1 c= N4 ~ N1 by Th57;
hence thesis by A2,A3;
end;
theorem
for N,N1 be normal Subgroup of G ex N2 being strict normal Subgroup of G st
the carrier of N2 = N ` N & N ` N1 c= N2 ` N1
proof
let N,N1 be normal Subgroup of G;
N is Subgroup of N by GROUP_2:54;
then consider N2 be strict normal Subgroup of G such that
A1:the carrier of N2 = N ` N by Th74;
N2 is Subgroup of N by A1,Th53,GROUP_2:57;
then N ` N1 c= N2 ` N1 by Th60;
hence thesis by A1;
end;
theorem
for N,N1 be normal Subgroup of G ex N2 being strict normal Subgroup of G st
the carrier of N2 = N ~ N & N ~ N1 c= N2 ~ N1
proof
let N,N1 be normal Subgroup of G;
consider N2 be strict normal Subgroup of G such that
A1:the carrier of N2 = N ~ N by Th73;
N is Subgroup of N2 by A1,Th54,GROUP_2:57;
then N ~ N1 c= N2 ~ N1 by Th57;
hence thesis by A1;
end;