let G be addGroup; :: thesis: for a being Element of G
for H being Subgroup of G holds Index H = Index (H * a)
let a be Element of G; :: thesis: for H being Subgroup of G holds Index H = Index (H * a)
let H be Subgroup of G; :: thesis: Index H = Index (H * a)
defpred S₁[ object , object ] means ex b being Element of G st
( $1 = b + H & $2 = (b * a) + (H * a) );
A1: for x being object st x in Left_Cosets H holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in Left_Cosets H implies ex y being object st S₁[x,y] )
assume x in Left_Cosets H ; :: thesis: ex y being object st S₁[x,y]
then consider b being Element of G such that
A2: x = b + H by Def15;
reconsider y = (b * a) + (H * a) as set ;
take y ; :: thesis: S₁[x,y]
take b ; :: thesis: ( x = b + H & y = (b * a) + (H * a) )
thus ( x = b + H & y = (b * a) + (H * a) ) by A2; :: thesis: verum

end;

consider f being Function such that
A3: dom f = Left_Cosets H and
A4: for x being object st x in Left_Cosets H holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
A5: for x, y1, y2 being set st x in Left_Cosets H & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

set A = carr H;
let x, y1, y2 be set ; :: thesis: ( x in Left_Cosets H & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume x in Left_Cosets H ; :: thesis: ( not S₁[x,y1] or not S₁[x,y2] or y1 = y2 )
given b being Element of G such that A6: x = b + H and
A7: y1 = (b * a) + (H * a) ; :: thesis: ( not S₁[x,y2] or y1 = y2 )
given c being Element of G such that A8: x = c + H and
A9: y2 = (c * a) + (H * a) ; :: thesis: y1 = y2
thus y1 = (((- a) + b) + a) + (((- a) + H) + a) by A7, ThB59
.= ((((- a) + b) + a) + ((- a) + (carr H))) + a by ThA33
.= (((- a) + b) + (a + ((- a) + (carr H)))) + a by Th32
.= (((- a) + b) + ((a + (- a)) + (carr H))) + a by Th32
.= (((- a) + b) + ((0_ G) + (carr H))) + a by Def5
.= (((- a) + b) + (carr H)) + a by Th37
.= ((- a) + (c + H)) + a by A6, A8, Th32
.= (((- a) + c) + (carr H)) + a by Th32
.= (((- a) + c) + ((0_ G) + (carr H))) + a by Th37
.= (((- a) + c) + ((a + (- a)) + (carr H))) + a by Def5
.= (((- a) + c) + (a + ((- a) + (carr H)))) + a by Th32
.= ((((- a) + c) + a) + ((- a) + (carr H))) + a by Th32
.= (((- a) + c) + a) + (((- a) + H) + a) by ThA33
.= y2 by A9, ThB59 ; :: thesis: verum

end;

A10: rng f = Left_Cosets (H * a)

proof

thus rng f c= Left_Cosets (H * a) :: according to XBOOLE_0:def 10 :: thesis: Left_Cosets (H * a) c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Left_Cosets (H * a) )
assume x in rng f ; :: thesis: x in Left_Cosets (H * a)
then consider y being object such that
A11: ( y in dom f & f . y = x ) by FUNCT_1:def 3;
ex b being Element of G st
( y = b + H & x = (b * a) + (H * a) ) by A3, A4, A11;
hence x in Left_Cosets (H * a) by Def15; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Left_Cosets (H * a) or x in rng f )
assume x in Left_Cosets (H * a) ; :: thesis: x in rng f
then consider b being Element of G such that
A12: x = b + (H * a) by Def15;
set c = b * (- a);
A13: x = ((b * (- a)) * a) + (H * a) by A12, ThB25;
A14: (b * (- a)) + H in Left_Cosets H by Def15;
then consider d being Element of G such that
A15: (b * (- a)) + H = d + H and
A16: f . ((b * (- a)) + H) = (d * a) + (H * a) by A4;
((b * (- a)) * a) + (H * a) = (d * a) + (H * a) by A5, A14, A15;
hence x in rng f by A3, A13, A14, A16, FUNCT_1:def 3; :: thesis: verum

end;

f is one-to-one

proof

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
A17: x in dom f and
A18: y in dom f and
A19: f . x = f . y ; :: thesis: x = y
consider c being Element of G such that
A20: y = c + H and
A21: f . y = (c * a) + (H * a) by A3, A4, A18;
consider b being Element of G such that
A22: x = b + H and
A23: f . x = (b * a) + (H * a) by A3, A4, A17;
A24: (- (c * a)) + (b * a) = ((- c) * a) + (b * a) by Th26
.= ((- c) + b) * a by Th23 ;
consider d being Element of G such that
A25: ((- c) + b) * a = d * a and
A26: d in H by A24, Th58, A19, A23, A21, Th114;
(- c) + b = d by A25, ThB16;
hence x = y by A22, A20, A26, Th114; :: thesis: verum

end;

hence Index H = Index (H * a) by A3, A10, WELLORD2:def 4, CARD_1:5; :: thesis: verum