:: On Rough Subgroup of a Group
:: by Xiquan Liang and Dailu Li
::
:: Received August 7, 2009
:: Copyright (c) 2009-2021 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;
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 :: GROUP_11:1
for N be normal Subgroup of G,x1,x2 be Element of G holds
(x1 * N) * (x2 * N) = (x1 * x2) * N;
theorem :: GROUP_11:2
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;
theorem :: GROUP_11:3
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;
theorem :: GROUP_11:4
for x,y being Element of G, N be normal Subgroup of G
st y in N holds x * y * x" in N;
theorem :: GROUP_11:5
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;
theorem :: GROUP_11:6
x in H1 * H2 iff ex a,b st x = a * b & a in H1 & b in H2;
theorem :: GROUP_11:7
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;
theorem :: GROUP_11:8
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;
theorem :: GROUP_11:9
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;
theorem :: GROUP_11:10
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;
theorem :: GROUP_11:11
for N being normal Subgroup of G for x holds x * N * x" c= carr(N);
definition
let G be Group, A be Subset of G;
let N be Subgroup of G;
func N ` A -> Subset of G equals
:: GROUP_11:def 1
{x where x is Element of G: x * N c= A};
func N ~ A -> Subset of G equals
:: GROUP_11:def 2
{x where x is Element of G : x * N meets A};
end;
theorem :: GROUP_11:12
for x being Element of G st x in N ` A holds x * N c= A;
theorem :: GROUP_11:13
for x being Element of G st x * N c= A holds x in N ` A;
theorem :: GROUP_11:14
for x being Element of G st x in N ~ A holds x * N meets A;
theorem :: GROUP_11:15
for x being Element of G st x * N meets A holds x in N ~ A;
theorem :: GROUP_11:16
N ` A c= A;
theorem :: GROUP_11:17
A c= N ~ A;
theorem :: GROUP_11:18
N ` A c= N ~ A;
theorem :: GROUP_11:19
N ~ (A \/ B) = N ~ A \/ N ~ B;
theorem :: GROUP_11:20
N ` (A /\ B) = N ` A /\ N ` B;
theorem :: GROUP_11:21
A c= B implies N ` A c= N ` B;
theorem :: GROUP_11:22
A c= B implies N ~ A c= N ~ B;
theorem :: GROUP_11:23
N ` A \/ N ` B c= N ` (A \/ B);
theorem :: GROUP_11:24
N ~ (A \/ B)= N ~ A \/ N ~ B;
theorem :: GROUP_11:25
N is Subgroup of H implies H ` A c= N ` A;
theorem :: GROUP_11:26
N is Subgroup of H implies N ~ A c= H ~ A;
theorem :: GROUP_11:27
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);
theorem :: GROUP_11:28
for x being Element of G st x in N ~ (A * B) holds x * N meets A * B;
theorem :: GROUP_11:29
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);
theorem :: GROUP_11:30
for x being Element of G st x in N ~ (N ` (N ~ A))
holds x * N meets N ` (N ~ A);
theorem :: GROUP_11:31
for x being Element of G st x in N ` (N ~ A) holds x * N c= N ~ A;
theorem :: GROUP_11:32
for x being Element of G st x in N ~ (N ~ A) holds x * N meets N ~ A;
theorem :: GROUP_11:33
for x being Element of G st x in N ~ (N ` A) holds x * N meets N ` A;
theorem :: GROUP_11:34
N ` (N ` A) = N ` A;
theorem :: GROUP_11:35
N ~ A = N ~ (N ~ A);
theorem :: GROUP_11:36
N ` (N ` A) c= N ~ (N ~ A);
theorem :: GROUP_11:37
N ~ (N ` A) c= A;
theorem :: GROUP_11:38
N ` (N ~ (N ` A)) = N ` A;
theorem :: GROUP_11:39
A c= N ` (N ~ A) implies N ~ A c= N ~ (N `(N ~ A));
theorem :: GROUP_11:40
N ~ (N `(N ~ A)) = N ~ A;
theorem :: GROUP_11:41
for x being Element of G st x in N ` (N ` A) holds x * N c= N ` A;
theorem :: GROUP_11:42
N `(N ` A) = N ~ (N ` A);
theorem :: GROUP_11:43
N ~ (N ~ A) = N `(N ~ A);
theorem :: GROUP_11:44
for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N ~ A c= N1 ~ A /\ N2 ~ A;
theorem :: GROUP_11:45
for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N1 ` A /\ N2 ` A c= N ` A;
theorem :: GROUP_11:46
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;
theorem :: GROUP_11:47
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;
theorem :: GROUP_11:48
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);
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
:: GROUP_11:def 3
{x where x is Element of G: x * N c= carr(H)};
func N ~ H -> Subset of G equals
:: GROUP_11:def 4
{x where x is Element of G : x * N meets carr(H)};
end;
theorem :: GROUP_11:49
for x being Element of G st x in N ` H holds x * N c= carr(H);
theorem :: GROUP_11:50
for x being Element of G st x * N c= carr(H) holds x in N ` H;
theorem :: GROUP_11:51
for x being Element of G st x in N ~ H holds x * N meets carr(H);
theorem :: GROUP_11:52
for x being Element of G st x * N meets carr(H) holds x in N ~ H;
theorem :: GROUP_11:53
N ` H c= carr(H);
theorem :: GROUP_11:54
carr(H) c= N ~ H;
theorem :: GROUP_11:55
N ` H c= N ~ H;
theorem :: GROUP_11:56
H1 is Subgroup of H2 implies N ~ H1 c= N ~ H2;
theorem :: GROUP_11:57
N1 is Subgroup of N2 implies N1 ~ H c= N2 ~ H;
theorem :: GROUP_11:58
N1 is Subgroup of N2 implies N1 ~ N1 c= N2 ~ N2;
theorem :: GROUP_11:59
H1 is Subgroup of H2 implies N ` H1 c= N ` H2;
theorem :: GROUP_11:60
N1 is Subgroup of N2 implies N2 ` H c= N1 ` H;
theorem :: GROUP_11:61
N1 is Subgroup of N2 implies N2 ` N1 c= N1 ` N2;
theorem :: GROUP_11:62
for N be normal Subgroup of G holds N ` H1 * N ` H2 c= N ` (H1 * H2);
theorem :: GROUP_11:63
for N be normal Subgroup of G holds N ~ H1 * N ~ H2 = N ~ (H1 * H2);
theorem :: GROUP_11:64
for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N ~ H c= N1 ~ H /\ N2 ~ H;
theorem :: GROUP_11:65
for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N1 ` H /\ N2 ` H c= N ` H;
theorem :: GROUP_11:66
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;
theorem :: GROUP_11:67
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;
theorem :: GROUP_11:68
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;
theorem :: GROUP_11:69
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;
theorem :: GROUP_11:70
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);
theorem :: GROUP_11:71
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;
theorem :: GROUP_11:72
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;
theorem :: GROUP_11:73
for H,N be normal Subgroup of G
ex M being strict normal Subgroup of G st the carrier of M = N ~ H;
theorem :: GROUP_11:74
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;
theorem :: GROUP_11:75
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;
theorem :: GROUP_11:76
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;
theorem :: GROUP_11:77
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;
theorem :: GROUP_11:78
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;
theorem :: GROUP_11:79
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;
theorem :: GROUP_11:80
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;
theorem :: GROUP_11:81
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;