:: On Rough Subgroup of a Group
:: by Xiquan Liang and Dailu Li
::
:: Received August 7, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

theorem Th1: :: GROUP_11:1
for G being Group
for N being normal Subgroup of G
for x1, x2 being Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N
proofend;

theorem Th2: :: GROUP_11:2
for G being Group
for N being Subgroup of G
for x, y being Element of G st y in x * N holds
x * N = y * N
proofend;

theorem Th3: :: GROUP_11:3
for G being Group
for N, H being Subgroup of G
for x being Element of G st x * N meets carr H holds
ex y being Element of G st
( y in x * N & y in H )
proofend;

theorem Th4: :: GROUP_11:4
for G being Group
for x, y being Element of G
for N being normal Subgroup of G st y in N holds
(x * y) * (x ") in N
proofend;

theorem Th5: :: GROUP_11:5
for G being Group
for N being 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
proofend;

theorem Th6: :: GROUP_11:6
for G being Group
for H1, H2 being Subgroup of G
for x being Element of G holds
( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
proofend;

theorem Th7: :: GROUP_11:7
for G being Group
for N1, N2 being strict normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N1 * N2
proofend;

theorem Th8: :: GROUP_11:8
for G being Group
for N1, N2 being strict normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N1 * N2
proofend;

theorem Th9: :: GROUP_11:9
for G being Group
for 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 )
proofend;

theorem Th10: :: GROUP_11:10
for G being Group
for N, N1, N2 being normal Subgroup of G
for a, b being Element of G st the carrier of N = N1 * N2 holds
(a * N1) * (b * N2) = (a * b) * N
proofend;

theorem :: GROUP_11:11
for G being Group
for N being normal Subgroup of G
for x being Element of G holds (x * N) * (x ") c= carr N
proofend;

definition
let G be Group;
let A be Subset of G;
let N be Subgroup of G;
funcN ` A ->  Subset of G equals :: GROUP_11:def 1
 {  x where x is Element of G : x * N c= A  }  ;
correctness
coherence
{  x where x is Element of G : x * N c= A  }  is Subset of G;
proofend;
funcN ~ A ->  Subset of G equals :: GROUP_11:def 2
 {  x where x is Element of G : x * N meets A  }  ;
correctness
coherence
{  x where x is Element of G : x * N meets A  }  is Subset of G;
proofend;
end;

:: deftheorem  defines ` GROUP_11:def_1_:_
 for G being Group
for A being Subset of G
for N being Subgroup of G holds N ` A =  {  x where x is Element of G : x * N c= A  }  ;

:: deftheorem  defines ~ GROUP_11:def_2_:_
 for G being Group
for A being Subset of G
for N being Subgroup of G holds N ~ A =  {  x where x is Element of G : x * N meets A  }  ;

theorem Th12: :: GROUP_11:12
for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ` A holds
x * N c= A
proofend;

theorem :: GROUP_11:13
for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x * N c= A holds
x in N ` A ;

theorem Th14: :: GROUP_11:14
for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ~ A holds
x * N meets A
proofend;

theorem :: GROUP_11:15
for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x * N meets A holds
x in N ~ A ;

theorem Th16: :: GROUP_11:16
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ` A c= A
proofend;

theorem Th17: :: GROUP_11:17
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds A c= N ~ A
proofend;

theorem Th18: :: GROUP_11:18
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ` A c= N ~ A
proofend;

theorem :: GROUP_11:19
for G being Group
for A, B being non empty Subset of G
for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)
proofend;

theorem :: GROUP_11:20
for G being Group
for A, B being non empty Subset of G
for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B)
proofend;

theorem :: GROUP_11:21
for G being Group
for A, B being non empty Subset of G
for N being Subgroup of G st A c= B holds
N ` A c= N ` B
proofend;

theorem :: GROUP_11:22
for G being Group
for A, B being non empty Subset of G
for N being Subgroup of G st A c= B holds
N ~ A c= N ~ B
proofend;

theorem :: GROUP_11:23
for G being Group
for A, B being non empty Subset of G
for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B)
proofend;

theorem :: GROUP_11:24
for G being Group
for A, B being non empty Subset of G
for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)
proofend;

theorem Th25: :: GROUP_11:25
for G being Group
for A being non empty Subset of G
for N, H being Subgroup of G st N is Subgroup of H holds
H ` A c= N ` A
proofend;

theorem Th26: :: GROUP_11:26
for G being Group
for A being non empty Subset of G
for N, H being Subgroup of G st N is Subgroup of H holds
N ~ A c= H ~ A
proofend;

theorem :: GROUP_11:27
for G being Group
for A, B being non empty Subset of G
for N being normal Subgroup of G holds (N ` A) * (N ` B) c= N ` (A * B)
proofend;

theorem Th28: :: GROUP_11:28
for G being Group
for A, B being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ~ (A * B) holds
x * N meets A * B
proofend;

theorem :: GROUP_11:29
for G being Group
for A, B being non empty Subset of G
for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B)
proofend;

theorem Th30: :: GROUP_11:30
for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ~ (N ` (N ~ A)) holds
x * N meets N ` (N ~ A)
proofend;

theorem Th31: :: GROUP_11:31
for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ` (N ~ A) holds
x * N c= N ~ A
proofend;

theorem Th32: :: GROUP_11:32
for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ~ (N ~ A) holds
x * N meets N ~ A
proofend;

theorem Th33: :: GROUP_11:33
for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ~ (N ` A) holds
x * N meets N ` A
proofend;

theorem Th34: :: GROUP_11:34
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ` (N ` A) = N ` A
proofend;

theorem Th35: :: GROUP_11:35
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ~ A = N ~ (N ~ A)
proofend;

theorem :: GROUP_11:36
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A)
proofend;

theorem :: GROUP_11:37
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ~ (N ` A) c= A
proofend;

theorem :: GROUP_11:38
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ` (N ~ (N ` A)) = N ` A
proofend;

theorem Th39: :: GROUP_11:39
for G being Group
for A being non empty Subset of G
for N being Subgroup of G st A c= N ` (N ~ A) holds
N ~ A c= N ~ (N ` (N ~ A))
proofend;

theorem :: GROUP_11:40
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ~ (N ` (N ~ A)) = N ~ A
proofend;

theorem Th41: :: GROUP_11:41
for G being Group
for A being non empty Subset of G
for N being Subgroup of G
for x being Element of G st x in N ` (N ` A) holds
x * N c= N ` A
proofend;

theorem :: GROUP_11:42
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ` (N ` A) = N ~ (N ` A)
proofend;

theorem :: GROUP_11:43
for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ~ (N ~ A) = N ` (N ~ A)
proofend;

theorem :: GROUP_11:44
for G being Group
for A being non empty Subset of G
for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds
N ~ A c= (N1 ~ A) /\ (N2 ~ A)
proofend;

theorem :: GROUP_11:45
for G being Group
for A being non empty Subset of G
for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds
(N1 ` A) /\ (N2 ` A) c= N ` A
proofend;

theorem :: GROUP_11:46
for G being Group
for A being non empty Subset of G
for N1, N2 being 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) )
proofend;

theorem :: GROUP_11:47
for G being Group
for A being non empty Subset of G
for N1, N2 being 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 )
proofend;

theorem :: GROUP_11:48
for G being Group
for A being non empty Subset of G
for N1, N2 being 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) )
proofend;

definition
let G be Group;
let H, N be Subgroup of G;
funcN ` H ->  Subset of G equals :: GROUP_11:def 3
 {  x where x is Element of G : x * N c= carr H  }  ;
coherence
  {  x where x is Element of G : x * N c= carr H  }  is Subset of G
proofend;
funcN ~ H ->  Subset of G equals :: GROUP_11:def 4
 {  x where x is Element of G : x * N meets carr H  }  ;
coherence
  {  x where x is Element of G : x * N meets carr H  }  is Subset of G
proofend;
end;

:: deftheorem  defines ` GROUP_11:def_3_:_
 for G being Group
for H, N being Subgroup of G holds N ` H =  {  x where x is Element of G : x * N c= carr H  }  ;

:: deftheorem  defines ~ GROUP_11:def_4_:_
 for G being Group
for H, N being Subgroup of G holds N ~ H =  {  x where x is Element of G : x * N meets carr H  }  ;

theorem Th49: :: GROUP_11:49
for G being Group
for N, H being Subgroup of G
for x being Element of G st x in N ` H holds
x * N c= carr H
proofend;

theorem :: GROUP_11:50
for G being Group
for N, H being Subgroup of G
for x being Element of G st x * N c= carr H holds
x in N ` H ;

theorem Th51: :: GROUP_11:51
for G being Group
for N, H being Subgroup of G
for x being Element of G st x in N ~ H holds
x * N meets carr H
proofend;

theorem :: GROUP_11:52
for G being Group
for N, H being Subgroup of G
for x being Element of G st x * N meets carr H holds
x in N ~ H ;

theorem Th53: :: GROUP_11:53
for G being Group
for N, H being Subgroup of G holds N ` H c= carr H
proofend;

theorem Th54: :: GROUP_11:54
for G being Group
for H, N being Subgroup of G holds carr H c= N ~ H
proofend;

theorem Th55: :: GROUP_11:55
for G being Group
for N, H being Subgroup of G holds N ` H c= N ~ H
proofend;

theorem Th56: :: GROUP_11:56
for G being Group
for H1, H2, N being Subgroup of G st H1 is Subgroup of H2 holds
N ~ H1 c= N ~ H2
proofend;

theorem Th57: :: GROUP_11:57
for G being Group
for H, N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds
N1 ~ H c= N2 ~ H
proofend;

theorem :: GROUP_11:58
for G being Group
for N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds
N1 ~ N1 c= N2 ~ N2
proofend;

theorem Th59: :: GROUP_11:59
for G being Group
for H1, H2, N being Subgroup of G st H1 is Subgroup of H2 holds
N ` H1 c= N ` H2
proofend;

theorem Th60: :: GROUP_11:60
for G being Group
for H, N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds
N2 ` H c= N1 ` H
proofend;

theorem :: GROUP_11:61
for G being Group
for N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds
N2 ` N1 c= N1 ` N2
proofend;

theorem :: GROUP_11:62
for G being Group
for H1, H2 being Subgroup of G
for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2)
proofend;

theorem :: GROUP_11:63
for G being Group
for H1, H2 being Subgroup of G
for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)
proofend;

theorem :: GROUP_11:64
for G being Group
for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds
N ~ H c= (N1 ~ H) /\ (N2 ~ H)
proofend;

theorem :: GROUP_11:65
for G being Group
for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds
(N1 ` H) /\ (N2 ` H) c= N ` H
proofend;

theorem :: GROUP_11:66
for G being Group
for H being Subgroup of G
for N1, N2 being 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 ` H) )
proofend;

theorem :: GROUP_11:67
for G being Group
for H being Subgroup of G
for N1, N2 being 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 )
proofend;

theorem :: GROUP_11:68
for G being Group
for H being Subgroup of G
for N1, N2 being 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 )
proofend;

theorem :: GROUP_11:69
for G being Group
for H being Subgroup of G
for N1, N2 being 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 )
proofend;

theorem :: GROUP_11:70
for G being Group
for H being Subgroup of G
for N1, N2 being 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) )
proofend;

theorem Th71: :: GROUP_11:71
for G being Group
for H being Subgroup of G
for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H
proofend;

theorem Th72: :: GROUP_11:72
for G being Group
for H being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of H holds
ex M being strict Subgroup of G st the carrier of M = N ` H
proofend;

theorem Th73: :: GROUP_11:73
for G being Group
for H, N being normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N ~ H
proofend;

theorem Th74: :: GROUP_11:74
for G being Group
for H, N being normal Subgroup of G st N is Subgroup of H holds
ex M being strict normal Subgroup of G st the carrier of M = N ` H
proofend;

theorem Th75: :: GROUP_11:75
for G being Group
for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds
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 )
proofend;

theorem Th76: :: GROUP_11:76
for G being Group
for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds
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 )
proofend;

theorem :: GROUP_11:77
for G being Group
for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds
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 )
proofend;

theorem :: GROUP_11:78
for G being Group
for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds
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 )
proofend;

theorem :: GROUP_11:79
for G being Group
for N, N1, N2 being normal Subgroup of G st N1 is Subgroup of N2 holds
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 )
proofend;

theorem :: GROUP_11:80
for G being Group
for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st
( the carrier of N2 = N ` N & N ` N1 c= N2 ` N1 )
proofend;

theorem :: GROUP_11:81
for G being Group
for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st
( the carrier of N2 = N ~ N & N ~ N1 c= N2 ~ N1 )
proofend;