:: On Rough Subgroup of a Group
:: by Xiquan Liang and Dailu Li
::
:: Copyright (c) 2009-2021 Association of Mizar Users

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
proof end;

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
proof end;

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 )
proof end;

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
proof end;

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
proof end;

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 ) )
proof end;

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
proof end;

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
proof end;

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 )
proof end;

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
proof end;

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
proof end;

definition
let G be Group;
let 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 } ;
correctness
coherence
{ x where x is Element of G : x * N c= A } is Subset of G
;
proof end;
func N ~ 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
;
proof end;
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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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
proof end;

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)
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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
proof end;

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))
proof end;

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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) )
proof end;

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 )
proof end;

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) )
proof end;

definition
let G be Group;
let 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 } ;
coherence
{ x where x is Element of G : x * N c= carr H } is Subset of G
proof end;
func N ~ 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
proof end;
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
proof end;

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
proof end;

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
proof end;

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

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

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

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
proof end;

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
proof end;

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

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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) )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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) )
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;