Metamath Proof Explorer


Theorem eqgfval

Description: Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses eqgval.x X=BaseG
eqgval.n N=invgG
eqgval.p +˙=+G
eqgval.r R=G~QGS
Assertion eqgfval GVSXR=xy|xyXNx+˙yS

Proof

Step Hyp Ref Expression
1 eqgval.x X=BaseG
2 eqgval.n N=invgG
3 eqgval.p +˙=+G
4 eqgval.r R=G~QGS
5 elex GVGV
6 1 fvexi XV
7 6 ssex SXSV
8 simpl g=Gs=Sg=G
9 8 fveq2d g=Gs=SBaseg=BaseG
10 9 1 eqtr4di g=Gs=SBaseg=X
11 10 sseq2d g=Gs=SxyBasegxyX
12 8 fveq2d g=Gs=S+g=+G
13 12 3 eqtr4di g=Gs=S+g=+˙
14 8 fveq2d g=Gs=Sinvgg=invgG
15 14 2 eqtr4di g=Gs=Sinvgg=N
16 15 fveq1d g=Gs=Sinvggx=Nx
17 eqidd g=Gs=Sy=y
18 13 16 17 oveq123d g=Gs=Sinvggx+gy=Nx+˙y
19 simpr g=Gs=Ss=S
20 18 19 eleq12d g=Gs=Sinvggx+gysNx+˙yS
21 11 20 anbi12d g=Gs=SxyBaseginvggx+gysxyXNx+˙yS
22 21 opabbidv g=Gs=Sxy|xyBaseginvggx+gys=xy|xyXNx+˙yS
23 df-eqg ~QG=gV,sVxy|xyBaseginvggx+gys
24 6 6 xpex X×XV
25 simpl xyXNx+˙ySxyX
26 vex xV
27 vex yV
28 26 27 prss xXyXxyX
29 25 28 sylibr xyXNx+˙ySxXyX
30 29 ssopab2i xy|xyXNx+˙ySxy|xXyX
31 df-xp X×X=xy|xXyX
32 30 31 sseqtrri xy|xyXNx+˙ySX×X
33 24 32 ssexi xy|xyXNx+˙ySV
34 22 23 33 ovmpoa GVSVG~QGS=xy|xyXNx+˙yS
35 4 34 eqtrid GVSVR=xy|xyXNx+˙yS
36 5 7 35 syl2an GVSXR=xy|xyXNx+˙yS