let G be Group; :: thesis: 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; :: thesis: 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; :: thesis: ( D = A /\ B & G is finite implies index (G,B) >= index (A,D) )

assume that

A1: D = A /\ B and

A2: G is finite ; :: thesis: 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;

_{1}[ 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 S_{1}[x,y]

A10: for a being Element of LCD holds S_{1}[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

hence index (G,B) >= index (A,D) by NAT_1:39; :: thesis: verum

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; :: thesis: 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; :: thesis: ( D = A /\ B & G is finite implies index (G,B) >= index (A,D) )

assume that

A1: D = A /\ B and

A2: G is finite ; :: thesis: 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 :: thesis: 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 )

defpred Sfor x9, y9 being Element of A st x9 = x & y9 = y holds

( x * B = y * B iff x9 * D = y9 * D )

let x, y be Element of G; :: thesis: for x9, y9 being Element of A st x9 = x & y9 = y holds

( x * B = y * B iff x9 * D = y9 * D )

let x9, y9 be Element of A; :: thesis: ( x9 = x & y9 = y implies ( x * B = y * B iff x9 * D = y9 * D ) )

assume that

A4: x9 = x and

A5: y9 = y ; :: thesis: ( x * B = y * B iff x9 * D = y9 * D )

A6: y9 " = y " by A5, GROUP_2:48;

A7: (y9 ") * x9 in A ;

( x * B = y * B iff (y ") * x in B ) by GROUP_2:114;

then ( x * B = y * B iff (y9 ") * x9 in B ) by A4, A6, GROUP_2:43;

then ( x * B = y * B iff (y9 ") * x9 in D ) by A1, A7, GROUP_2:82;

hence ( x * B = y * B iff x9 * D = y9 * D ) by GROUP_2:114; :: thesis: verum

end;( x * B = y * B iff x9 * D = y9 * D )

let x9, y9 be Element of A; :: thesis: ( x9 = x & y9 = y implies ( x * B = y * B iff x9 * D = y9 * D ) )

assume that

A4: x9 = x and

A5: y9 = y ; :: thesis: ( x * B = y * B iff x9 * D = y9 * D )

A6: y9 " = y " by A5, GROUP_2:48;

A7: (y9 ") * x9 in A ;

( x * B = y * B iff (y ") * x in B ) by GROUP_2:114;

then ( x * B = y * B iff (y9 ") * x9 in B ) by A4, A6, GROUP_2:43;

then ( x * B = y * B iff (y9 ") * x9 in D ) by A1, A7, GROUP_2:82;

hence ( x * B = y * B iff x9 * D = y9 * D ) by GROUP_2:114; :: thesis: verum

( a = a9 & $2 = a * B & $1 = a9 * D );

A8: for x being Element of LCD ex y being Element of LCB st S

proof

consider F being Function of LCD,LCB such that
let x be Element of LCD; :: thesis: ex y being Element of LCB st S_{1}[x,y]

x in LCD ;

then consider a9 being Element of A such that

A9: x = a9 * D by GROUP_2:def 15;

reconsider a = a9 as Element of G by GROUP_2:42;

reconsider y = a * B as Element of LCB by GROUP_2:def 15;

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

take a ; :: thesis: ex a9 being Element of A st

( a = a9 & y = a * B & x = a9 * D )

take a9 ; :: thesis: ( a = a9 & y = a * B & x = a9 * D )

thus ( a = a9 & y = a * B & x = a9 * D ) by A9; :: thesis: verum

end;x in LCD ;

then consider a9 being Element of A such that

A9: x = a9 * D by GROUP_2:def 15;

reconsider a = a9 as Element of G by GROUP_2:42;

reconsider y = a * B as Element of LCB by GROUP_2:def 15;

take y ; :: thesis: S

take a ; :: thesis: ex a9 being Element of A st

( a = a9 & y = a * B & x = a9 * D )

take a9 ; :: thesis: ( a = a9 & y = a * B & x = a9 * D )

thus ( a = a9 & y = a * B & x = a9 * D ) by A9; :: thesis: verum

A10: for a being Element of LCD holds S

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

proof

then
Segm (index D) c= Segm (index B)
by A11, A12, A13, A14, CARD_1:10;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 )

assume that

A15: x1 in dom F and

A16: x2 in dom F ; :: thesis: ( not F . x1 = F . x2 or x1 = x2 )

reconsider z1 = x1, z2 = x2 as Element of LCD by A15, A16, FUNCT_2:def 1;

A17: ex a being Element of G ex a9 being Element of A st

( a = a9 & F . z1 = a * B & z1 = a9 * D ) by A10;

ex b being Element of G ex b9 being Element of A st

( b = b9 & F . z2 = b * B & z2 = b9 * D ) by A10;

hence ( not F . x1 = F . x2 or x1 = x2 ) by A3, A17; :: thesis: verum

end;assume that

A15: x1 in dom F and

A16: x2 in dom F ; :: thesis: ( not F . x1 = F . x2 or x1 = x2 )

reconsider z1 = x1, z2 = x2 as Element of LCD by A15, A16, FUNCT_2:def 1;

A17: ex a being Element of G ex a9 being Element of A st

( a = a9 & F . z1 = a * B & z1 = a9 * D ) by A10;

ex b being Element of G ex b9 being Element of A st

( b = b9 & F . z2 = b * B & z2 = b9 * D ) by A10;

hence ( not F . x1 = F . x2 or x1 = x2 ) by A3, A17; :: thesis: verum

hence index (G,B) >= index (A,D) by NAT_1:39; :: thesis: verum