let G be Group; :: thesis: for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent

let H be Subgroup of G; :: thesis: Left_Cosets H, Right_Cosets H are_equipotent

defpred S_{1}[ object , object ] means ex g being Element of G st

( $1 = g * H & $2 = H * (g ") );

A1: for x being object st x in Left_Cosets H holds

ex y being object st S_{1}[x,y]

A3: dom f = Left_Cosets H and

A4: for x being object st x in Left_Cosets H holds

S_{1}[x,f . x]
from CLASSES1:sch 1(A1);

A5: rng f = Right_Cosets H

let H be Subgroup of G; :: thesis: Left_Cosets H, Right_Cosets H are_equipotent

defpred S

( $1 = g * H & $2 = H * (g ") );

A1: for x being object st x in Left_Cosets H holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in Left_Cosets H implies ex y being object st S_{1}[x,y] )

assume x in Left_Cosets H ; :: thesis: ex y being object st S_{1}[x,y]

then consider g being Element of G such that

A2: x = g * H by Def15;

reconsider y = H * (g ") as set ;

take y ; :: thesis: S_{1}[x,y]

take g ; :: thesis: ( x = g * H & y = H * (g ") )

thus ( x = g * H & y = H * (g ") ) by A2; :: thesis: verum

end;assume x in Left_Cosets H ; :: thesis: ex y being object st S

then consider g being Element of G such that

A2: x = g * H by Def15;

reconsider y = H * (g ") as set ;

take y ; :: thesis: S

take g ; :: thesis: ( x = g * H & y = H * (g ") )

thus ( x = g * H & y = H * (g ") ) by A2; :: thesis: verum

A3: dom f = Left_Cosets H and

A4: for x being object st x in Left_Cosets H holds

S

A5: rng f = Right_Cosets H

proof

f is one-to-one
thus
rng f c= Right_Cosets H
:: according to XBOOLE_0:def 10 :: thesis: Right_Cosets H c= rng f

assume A8: x in Right_Cosets H ; :: thesis: x in rng f

then reconsider A = x as Subset of G ;

consider g being Element of G such that

A9: A = H * g by A8, Def16;

A10: (g ") * H in Left_Cosets H by Def15;

then A11: f . ((g ") * H) in rng f by A3, FUNCT_1:def 3;

consider a being Element of G such that

A12: (g ") * H = a * H and

A13: f . ((g ") * H) = H * (a ") by A4, A10;

(a ") * (g ") in H by A12, Th114;

hence x in rng f by A9, A11, A13, Th120; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Right_Cosets H or x in rng f )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Right_Cosets H )

assume x in rng f ; :: thesis: x in Right_Cosets H

then consider y being object such that

A6: y in dom f and

A7: f . y = x by FUNCT_1:def 3;

ex g being Element of G st

( y = g * H & f . y = H * (g ") ) by A3, A4, A6;

hence x in Right_Cosets H by A7, Def16; :: thesis: verum

end;assume x in rng f ; :: thesis: x in Right_Cosets H

then consider y being object such that

A6: y in dom f and

A7: f . y = x by FUNCT_1:def 3;

ex g being Element of G st

( y = g * H & f . y = H * (g ") ) by A3, A4, A6;

hence x in Right_Cosets H by A7, Def16; :: thesis: verum

assume A8: x in Right_Cosets H ; :: thesis: x in rng f

then reconsider A = x as Subset of G ;

consider g being Element of G such that

A9: A = H * g by A8, Def16;

A10: (g ") * H in Left_Cosets H by Def15;

then A11: f . ((g ") * H) in rng f by A3, FUNCT_1:def 3;

consider a being Element of G such that

A12: (g ") * H = a * H and

A13: f . ((g ") * H) = H * (a ") by A4, A10;

(a ") * (g ") in H by A12, Th114;

hence x in rng f by A9, A11, A13, Th120; :: thesis: verum

proof

hence
Left_Cosets H, Right_Cosets H are_equipotent
by A3, A5, WELLORD2:def 4; :: thesis: verum
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )

assume that

A14: x in dom f and

A15: y in dom f and

A16: f . x = f . y ; :: thesis: x = y

consider b being Element of G such that

A17: y = b * H and

A18: f . y = H * (b ") by A3, A4, A15;

consider a being Element of G such that

A19: x = a * H and

A20: f . x = H * (a ") by A3, A4, A14;

(b ") * ((a ") ") in H by A16, A20, A18, Th120;

hence x = y by A19, A17, Th114; :: thesis: verum

end;assume that

A14: x in dom f and

A15: y in dom f and

A16: f . x = f . y ; :: thesis: x = y

consider b being Element of G such that

A17: y = b * H and

A18: f . y = H * (b ") by A3, A4, A15;

consider a being Element of G such that

A19: x = a * H and

A20: f . x = H * (a ") by A3, A4, A14;

(b ") * ((a ") ") in H by A16, A20, A18, Th120;

hence x = y by A19, A17, Th114; :: thesis: verum