:: On Rough Subgroup of a Group
:: by Xiquan Liang and Dailu Li
::
:: Received August 7, 2009
:: Copyright (c) 2009-2011 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

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 H, N 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 H1, H2, N 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 H1, H2, N 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;