let G be Group; :: 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₁[ set , set ] means ex b being Element of G st
( $1 = b * H & $2 = (b |^ a) * (H |^ a) );
A1: for x, y1, y2 being set st x in Left_Cosets H & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis: ( x in Left_Cosets H & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
set A = carr H;
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 A2: ( x = b * H & y1 = (b |^ a) * (H |^ a) ) ; :: thesis: ( not S₁[x,y2] or y1 = y2 )
given c being Element of G such that A3: ( x = c * H & y2 = (c |^ a) * (H |^ a) ) ; :: thesis: y1 = y2
thus y1 = (((a " ) * b) * a) * (((a " ) * H) * a) by A2, Th71
.= ((((a " ) * b) * a) * ((a " ) * (carr H))) * a by GROUP_2:39
.= (((a " ) * b) * (a * ((a " ) * (carr H)))) * a by GROUP_2:38
.= (((a " ) * b) * ((a * (a " )) * (carr H))) * a by GROUP_2:38
.= (((a " ) * b) * ((1_ G) * (carr H))) * a by GROUP_1:def 6
.= (((a " ) * b) * (carr H)) * a by GROUP_2:43
.= ((a " ) * (c * H)) * a by A2, A3, GROUP_2:38
.= (((a " ) * c) * (carr H)) * a by GROUP_2:38
.= (((a " ) * c) * ((1_ G) * (carr H))) * a by GROUP_2:43
.= (((a " ) * c) * ((a * (a " )) * (carr H))) * a by GROUP_1:def 6
.= (((a " ) * c) * (a * ((a " ) * (carr H)))) * a by GROUP_2:38
.= ((((a " ) * c) * a) * ((a " ) * (carr H))) * a by GROUP_2:38
.= (((a " ) * c) * a) * (((a " ) * H) * a) by GROUP_2:39
.= y2 by A3, Th71 ; :: thesis: verum

end;

A4: for x being set st x in Left_Cosets H holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in Left_Cosets H implies ex y being set st S₁[x,y] )
assume x in Left_Cosets H ; :: thesis: ex y being set st S₁[x,y]
then consider b being Element of G such that
A5: x = b * H by GROUP_2:def 15;
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 A5; :: thesis: verum

end;

consider f being Function such that
A6: dom f = Left_Cosets H and
A7: for x being set st x in Left_Cosets H holds
S₁[x,f . x] from CLASSES1:sch 1(A4);
A8: 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 set ; :: 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 set such that
A9: ( y in dom f & f . y = x ) by FUNCT_1:def 5;
ex b being Element of G st
( y = b * H & x = (b |^ a) * (H |^ a) ) by A6, A7, A9;
hence x in Left_Cosets (H |^ a) by GROUP_2:def 15; :: thesis: verum

end;

let x be set ; :: 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
A10: x = b * (H |^ a) by GROUP_2:def 15;
set c = b |^ (a " );
A11: x = ((b |^ (a " )) |^ a) * (H |^ a) by A10, Th30;
A12: (b |^ (a " )) * H in Left_Cosets H by GROUP_2:def 15;
then consider d being Element of G such that
A13: ( (b |^ (a " )) * H = d * H & f . ((b |^ (a " )) * H) = (d |^ a) * (H |^ a) ) by A7;
((b |^ (a " )) |^ a) * (H |^ a) = (d |^ a) * (H |^ a) by A1, A12, A13;
hence x in rng f by A6, A11, A12, A13, FUNCT_1:def 5; :: thesis: verum

end;

f is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: 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: x = b * H and
A18: f . x = (b |^ a) * (H |^ a) by A6, A7, A14;
consider c being Element of G such that
A19: y = c * H and
A20: f . y = (c |^ a) * (H |^ a) by A6, A7, A15;
A21: ((c |^ a) " ) * (b |^ a) in H |^ a by A16, A18, A20, GROUP_2:137;
((c |^ a) " ) * (b |^ a) = ((c " ) |^ a) * (b |^ a) by Th32
.= ((c " ) * b) |^ a by Th28 ;
then consider d being Element of G such that
A22: ( ((c " ) * b) |^ a = d |^ a & d in H ) by A21, Th70;
(c " ) * b = d by A22, Th21;
hence x = y by A17, A19, A22, GROUP_2:137; :: thesis: verum

end;

then Left_Cosets H, Left_Cosets (H |^ a) are_equipotent by A6, A8, WELLORD2:def 4;
hence Index H = Index (H |^ a) by CARD_1:21; :: thesis: verum