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;
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 )
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 ;
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 ;
then ( x * B = y * B iff (y9 ") * x9 in D ) by ;
hence ( x * B = y * B iff x9 * D = y9 * D ) by GROUP_2:114; :: thesis: verum
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]
proof
let x be Element of LCD; :: thesis: ex y being Element of LCB st S1[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: S1[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;
consider F being Function of LCD,LCB such that
A10: for a being Element of LCD holds S1[a,F . a] from 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
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 ;
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 ; :: thesis: verum
end;
then Segm () c= Segm () by ;
hence index (G,B) >= index (A,D) by NAT_1:39; :: thesis: verum
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "http://mizar.uwb.edu.pl/version/current/html/proofs/group_8/19", "fetch_time": 1571380489000000000, "content_mime_type": "text/plain", "warc_filename": "crawl-data/CC-MAIN-2019-43/segments/1570986677964.40/warc/CC-MAIN-20191018055014-20191018082514-00309.warc.gz", "warc_record_offset": 138533247, "warc_record_length": 3581, "token_count": 1159, "char_count": 2965, "score": 3.65625, "int_score": 4, "crawl": "CC-MAIN-2019-43", "snapshot_type": "latest", "language": "en", "language_score": 0.8707126975059509, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00020-of-00064.parquet"}