let G be Group; for B, A being Subgroup of G
for D being Subgroup of A st D = A /\ B & G is finite holds
index (G,B) >= index (A,D)
let B, A be Subgroup of G; for D being Subgroup of A st D = A /\ B & G is finite holds
index (G,B) >= index (A,D)
let D be Subgroup of A; ( D = A /\ B & G is finite implies index (G,B) >= index (A,D) )
assume that
A1:
D = A /\ B
and
A2:
G is finite
; index (G,B) >= index (A,D)
reconsider LCB = Left_Cosets B as non empty finite set by A2;
reconsider LCD = Left_Cosets D as non empty finite set by A2;
A3:
now for x, y being Element of G
for x9, y9 being Element of A st x9 = x & y9 = y holds
( x * B = y * B iff x9 * D = y9 * D )end;
defpred S1[ set , set ] means ex a being Element of G ex a9 being Element of A st
( a = a9 & $2 = a * B & $1 = a9 * D );
A8:
for x being Element of LCD ex y being Element of LCB st S1[x,y]
consider F being Function of LCD,LCB such that
A10:
for a being Element of LCD holds S1[a,F . a]
from FUNCT_2:sch 3(A8);
A11:
dom F = LCD
by FUNCT_2:def 1;
A12:
rng F c= LCB
by RELAT_1:def 19;
A13:
index D = card LCD
by GROUP_2:def 18;
A14:
index B = card LCB
by GROUP_2:def 18;
F is one-to-one
then
Segm (index D) c= Segm (index B)
by A11, A12, A13, A14, CARD_1:10;
hence
index (G,B) >= index (A,D)
by NAT_1:39; verum