let G be finite Group; :: thesis: for H being Subgroup of G holds card G = (card H) * (index H)
let H be Subgroup of G; :: thesis: card G = (card H) * (index H)
reconsider C = Left_Cosets H as finite set ;
set B = the carrier of G;
A1:
( union (Left_Cosets H) = the carrier of G & card G = card the carrier of G )
by Th167;
now let X be
set ;
:: thesis: ( X in C implies ex B being finite set st
( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) ) )assume A2:
X in C
;
:: thesis: ex B being finite set st
( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )then reconsider x =
X as
Subset of
G ;
consider a being
Element of
G such that A3:
x = a * H
by A2, Def15;
x is
finite
;
then reconsider B =
X as
finite set ;
take B =
B;
:: thesis: ( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )thus
B = X
;
:: thesis: ( card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )
ex
B,
C being
finite set st
(
B = a * H &
C = H * a &
card H = card B &
card H = card C )
by Th156;
hence
card B = card H
by A3;
:: thesis: for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y )let Y be
set ;
:: thesis: ( Y in C & X <> Y implies ( X,Y are_equipotent & X misses Y ) )assume that A4:
Y in C
and A5:
X <> Y
;
:: thesis: ( X,Y are_equipotent & X misses Y )reconsider y =
Y as
Subset of
G by A4;
consider b being
Element of
G such that A6:
y = b * H
by A4, Def15;
thus
X,
Y are_equipotent
by A3, A6, Th151;
:: thesis: X misses Ythus
X misses Y
by A3, A5, A6, Th138;
:: thesis: verum end;
then
ex D being finite set st
( D = union C & card D = (card H) * (card C) )
by Lm5;
hence
card G = (card H) * (index H)
by A1, Def18; :: thesis: verum